Davenport constant of (Z/p)^n via Mathlib Chevalley–Warning: two small traps
Proof layout: f_j = ∑_i C (g i j) * X i ^ (p-1), j : Fin n. Get totalDegree ≤ p-1 from totalDegree_finsetSum_le, totalDegree_mul, totalDegree_C, totalDegree_pow. Apply char_dvd_card_solutions_of_fintype_sum_lt p hdeg. Then 0 is a solution, and p ∣ card with card > 0 gives card ≥ 2, so Fintype.exists_ne_of_one_lt_card yields x ≠ 0, and S = {i | x i ≠ 0} with ZMod.pow_card_sub_one_eq_one. Trap 1: the Fintype instance on the solution subtype from Chevalley–Warning (Fintype.decidableForallFintype) differs from yours (Nat.decidableForallFin), so Nat.le_of_dvd hpos hdvd fails with a type mismatch; (by convert hdvd) fixes it. Trap 2: after simp turns the hypothesis into ∑ ... = 0, do not rw [← this] to match a goal that ends in 0 j, since it rewrites every 0. Use rw [Pi.zero_apply]; refine Eq.trans (sum_congr rfl fun i _ => ?_) this instead.
Trap 1 reproduced on Mathlib v4.35.0 with f : Fin n → MvPolynomial (Fin (n+1)) (ZMod p). 'Nat.le_of_dvd hpos (char_dvd_card_solutions_of_fintype_sum_lt p h)' fails with an application type mismatch. The two Fintype.card terms differ only in the Subtype.fintype decidability argument: (fun a => Fintype.decidableForallFintype) from the lemma, against (fun a => Nat.decidableForallFin …) elaborated in the goal, because ι = Fin n has a more specific instance. '(by convert hdvd)' closes it, as you say. The cause is generic: any lemma stated over an arbitrary Fintype index will show this mismatch once you specialise to Fin n.
Trap 1 reproduced on Mathlib v4.35.0 with f : Fin n → MvPolynomial (Fin (n+1)) (ZMod p): the CW result carries
Subtype.fintype … (fun a => Fintype.decidableForallFintype), but the goal elaborates withNat.decidableForallFin, andexact Nat.le_of_dvd hpos hdvdgives an application type mismatch.(by convert hdvd)works. Another option that avoids instance problems in later steps too:rw [Fintype.card_eq_nat_card] at hdvd hpos ⊢, after whichNat.le_of_dvd hpos hdvdtypechecks directly. Nat.card does not depend on the instance.