-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
this : ∀ (i : ι) (σ : ι →₀ ℕ) (_ : σ ∈ F.support), p ∣ (σ : (a : ι) → ℕ) i
σ' : (σ : ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ (σ : ι →₀ ℕ) (hσ : σ ∈ F.support), σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), (↑σ : ι →₀ ℕ) = p • σ' (↑σ : ι →₀ ℕ)
replace :
  ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
    LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p
⊢ False
have replace₁ : ∀
  (H :
    ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K) (hv : LinearIndependent k v),
      LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (x : ι) ↦ v x ^ p),
  False
Tactic: classical
  replace H (ι : Type u_3) (_ : Fintype ι) (v : ι → K) (hv : LinearIndependent k v) :
      LinearIndependent k (v · ^ p) := by
    simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, linearIndepOn_range_iff
      hv.injective] using H (Finset.univ.image v) (by simpa using hv.linearIndepOn_id)
  have := mt (H F.support inferInstance (fun s ↦ aeval a (monomial (σ' s) (1 : k)))) (by
    simp_rw [← map_pow, monomial_pow, ← hσ'', one_pow, not_linearIndependent_iff]
    refine ⟨.univ, (F.coeff ·), ?_, by simpa [MvPolynomial.eq_zero_iff] using hF0⟩
    simp only [← map_smul, ← map_sum, Finset.univ_eq_attach, smul_eq_mul, mul_one]
    rw [F.support.sum_attach (fun i ↦ monomial i (F.coeff i)), support_sum_monomial_coeff, hFa])
  simp only [LinearIndependent, injective_iff_map_eq_zero, not_forall] at this
  obtain ⟨F', hF', hF'0⟩ := this
  let F'' : MvPolynomial ι k := F'.mapDomain fun s ↦ σ' s.1
  have hF''0 : F'' ≠ 0 := ne_of_ne_of_eq ((Finsupp.mapDomain_injective fun s t h ↦ Subtype.ext
    (Finsupp.ext fun i ↦ by rw [hσ' _ s.2, hσ' _ t.2, h])).ne_iff.mpr hF'0) (by simp)
  have hF'' : aeval a F'' = 0 := by
    have : (aeval a).toLinearMap ∘ₗ (Finsupp.lmapDomain k k fun s : F.support ↦ σ' s) =
        (Finsupp.linearCombination k fun s : F.support ↦ aeval a (monomial (σ' s) (1 : k))) := by
      ext v; simp [AddMonoidAlgebra, monomial]
    simp only [← hF', F'', ← this]; rfl
  suffices hpm : p * F''.totalDegree ≤ F.totalDegree by
    have hF''0' : F''.totalDegree ≠ 0 := by
      contrapose hF''0
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
    replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
    exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)
  rw [totalDegree, Finset.mul_sup₀, Finset.sup_le_iff]
  intro σ hσ
  obtain ⟨σ, hσ₂, rfl⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hσ)
  refine le_trans ?_ (Finset.le_sup σ.2)
  conv_rhs => rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]