awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF'' : coeff 0 F'' = 0
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0 : F''.totalDegree = 0
rw :
  Eq (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 F'') : MvPolynomial ι k) (0 : MvPolynomial ι k)
rw₁ : Eq (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) 0) 0
⊢ F'' = 0
have rw₂ : Eq (α := MvPolynomial ι k) 0 0
Tactic: rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
hpm : p * F''.totalDegree ≤ F.totalDegree
⊢ False
have hF''0' : F''.totalDegree ≠ 0
Tactic: 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]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
hpm : p * F''.totalDegree ≤ F.totalDegree
hF''0' : F''.totalDegree ≠ 0
⊢ False
have this₁ : p * F''.totalDegree ≤ 1 * F''.totalDegree
Tactic: replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
Cleared hypotheses: this
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
⊢ False
have suffices : p * F''.totalDegree ≤ F.totalDegree
Tactic: 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)
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
⊢ p * F''.totalDegree ≤ F.totalDegree
have rw : ∀ b ∈ F''.support, (p * b.sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree
Tactic: rw [totalDegree, Finset.mul_sup₀, Finset.sup_le_iff]
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ι →₀ ℕ
hσ : σ ∈ F''.support
⊢ (p * σ.sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree
have obtain : ∀ (σ : ↥F.support) (hσ₂ : σ ∈ F'.support) (hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support),
  (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree
Tactic: obtain ⟨σ, hσ₂, rfl⟩ := Finset.mem_image.mp (Finsupp.mapDomain_support hσ)
Cleared hypotheses: σ, hσ
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
⊢ (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ F.totalDegree
have refine : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
Tactic: refine le_trans ?_ (Finset.le_sup σ.2)
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
| (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
have rw : p * (σ' (↑σ : ι →₀ ℕ)).sum fun (i : ι) (a : ℕ) ↦ a
Tactic: rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
⊢ (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
have conv_rhs : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
Tactic: conv_rhs => rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]
-- 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
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 • σ' (↑σ : ι →₀ ℕ)
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
F' : Finsupp.{u_3, u_1} (↥F.support) k
hF' :
  Eq.{u_2 + 1} (α := K)
    ((Finsupp.linearCombination k fun (s : ↥F.support) ↦
            (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1) :
          (a : ↥F.support →₀ k) → K)
        F' :
      K)
    (0 : K)
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F'
hF''0 : F'' ≠ 0
hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
σ : ↥F.support
hσ₂ : σ ∈ F'.support
hσ : σ' (↑σ : ι →₀ ℕ) ∈ F''.support
conv_rhs : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
⊢ (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ (↑σ : ι →₀ ℕ).sum fun (x : ι) (e : ℕ) ↦ e
have conv_rhs₁ : (p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e) ≤ p * (σ' (↑σ : ι →₀ ℕ)).sum fun (x : ι) (e : ℕ) ↦ e
Tactic: conv_rhs => rw [hσ' _ σ.2, Finsupp.sum_smul_index (fun _ ↦ rfl), ← Finsupp.mul_sum]
-- 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 • σ' (↑σ : ι →₀ ℕ)
⊢ False
have 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
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]
-- 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
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
⊢ ∃ F ∈ S,
    ∀ (G : MvPolynomial ι k),
      G ≠ 0 →
        Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) G : K) (0 : K) → F.totalDegree ≤ G.totalDegree
have suffices : S.Nonempty
Tactic: suffices S.Nonempty from
      ⟨totalDegree.argminOn S this, totalDegree.argminOn_mem ..,
        fun _ h₁ h₂ ↦ totalDegree.argminOn_le S ⟨h₁, h₂⟩⟩
-- 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
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
⊢ S.Nonempty
have suffices : ¬AlgebraicIndependent k a
Tactic: suffices ¬ AlgebraicIndependent k a by simpa [S, algebraicIndependent_iff, and_comm] using this
-- 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
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
⊢ False
have refine : IsAlgebraic (↥(Algebra.adjoin k (a '' {n}ᶜ))) (a n)
Tactic: refine h.transcendental_adjoin (i := n) (s := {n}ᶜ) (by simp) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
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
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
h : AlgebraicIndependent k a
⊢ IsAlgebraic (↥(Algebra.adjoin k (a '' {n}ᶜ))) (a n)
have this : a '' {n}ᶜ = Set.range fun (x : { i : ι // i ≠ n }) ↦ a (↑x : ι)
Tactic: have : a '' {n}ᶜ = Set.range (ι := {i // i ≠ n}) (a ·) := by aesop