awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ∀ (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
this :
  ¬LinearIndependent.{u_3, u_1, u_2} k (M := K) fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1)
⊢ False
have this₁ : ∃ (x : Finsupp.{u_3, u_1} (↥F.support) k) (_ :
  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)
        x :
      K)
    (0 : K)),
  ¬x = 0
Tactic: simp only [LinearIndependent, injective_iff_map_eq_zero, not_forall] at this
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_1 : ∀ (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
this :
  ∃ (x : Finsupp.{u_3, u_1} (↥F.support) k) (_ :
    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)
          x :
        K)
      (0 : K)),
    ¬x = 0
⊢ False
have obtain : ∀ (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), False
Tactic: obtain ⟨F', hF', hF'0⟩ := this
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'
s t : ↥F.support
h : σ' (↑s : ι →₀ ℕ) = σ' (↑t : ι →₀ ℕ)
i : ι
⊢ Eq (α := ℕ) (((↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) (((↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
have rw : Eq (α := ℕ) ((p • σ' (↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) (((↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
Tactic: rw [hσ' _ s.2, hσ' _ t.2, 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'
s t : ↥F.support
h : σ' (↑s : ι →₀ ℕ) = σ' (↑t : ι →₀ ℕ)
i : ι
rw : Eq (α := ℕ) ((p • σ' (↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) (((↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) (((↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) (((↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
have rw₁ : Eq (α := ℕ) ((p • σ' (↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) ((p • σ' (↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
Tactic: rw [hσ' _ s.2, hσ' _ t.2, 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'
s t : ↥F.support
h : σ' (↑s : ι →₀ ℕ) = σ' (↑t : ι →₀ ℕ)
i : ι
rw : Eq (α := ℕ) ((p • σ' (↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) (((↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
rw₁ : Eq (α := ℕ) ((p • σ' (↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) ((p • σ' (↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) (((↑s : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) (((↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
have rw₂ : Eq (α := ℕ) ((p • σ' (↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ) ((p • σ' (↑t : ι →₀ ℕ) : (a : ι) → ℕ) i : ℕ)
Tactic: rw [hσ' _ s.2, hσ' _ t.2, h]
-- 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'
⊢ False
have hF''0 : F'' ≠ 0
Tactic: 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)
-- 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
⊢ Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
    (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
    (Finsupp.linearCombination k fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))
have h : ∀ (v : ↥F.support),
  Eq.{u_2 + 1} (α := K)
    (((AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) ∘ₗ
            Finsupp.lsingle v :
          (a : k) → K)
        1 :
      K)
    (((Finsupp.linearCombination k fun (s : ↥F.support) ↦
              (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1)) ∘ₗ
            Finsupp.lsingle v :
          (a : k) → K)
        1 :
      K)
Tactic: ext v
-- 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
⊢ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
have this₁ : Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
  (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
  (Finsupp.linearCombination k fun (s : ↥F.support) ↦
    (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))
Tactic: 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]
-- 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_1 : ∀ (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
this :
  Eq (α := Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K)
    (AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ))
    (Finsupp.linearCombination k fun (s : ↥F.support) ↦
      (aeval a : (a : MvPolynomial ι k) → K) ((monomial (σ' (↑s : ι →₀ ℕ)) : (a : k) → MvPolynomial ι k) 1))
⊢ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
have simp : Eq.{u_2 + 1} (α := K)
  ((aeval a : (a : MvPolynomial ι k) → K) (Finsupp.mapDomain (fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ)) F') : K)
  (((AlgHom.toLinearMap (aeval a) ∘ₗ Finsupp.lmapDomain k k fun (s : ↥F.support) ↦ σ' (↑s : ι →₀ ℕ) :
          Finsupp.{u_3, u_1} (↥F.support) k →ₗ[k] K) :
        (a : ↥F.support →₀ k) → K)
      F' :
    K)
Tactic: simp only [← hF', F'', ← this]
-- 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
⊢ False
have hF'' : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F'' : K) (0 : K)
Tactic: 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
-- 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)
hpm : p * F''.totalDegree ≤ F.totalDegree
⊢ F''.totalDegree ≠ 0
have contrapose : ∀ (hF''0 : F''.totalDegree = 0), F'' = 0
Tactic: contrapose hF''0
Cleared hypotheses: hF''0
-- 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'' : 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
⊢ F'' = 0
have hF''₁ : coeff 0 F'' = 0
Tactic: rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
Cleared hypotheses: hF'', hpm, hF''0
-- 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
⊢ F'' = 0
have rw : Eq (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 F'') : MvPolynomial ι k) (0 : MvPolynomial ι k)
Tactic: rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
-- 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)
⊢ F'' = 0
have rw₁ : Eq (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) 0) 0
Tactic: rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]