awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
hF : ExpChar F q
inst_3 : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F (A := E) ((iterateFrobenius E q n : (a : E) → E) a : E)
hdeg :
  Polynomial.natDegree (minpoly F a) ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
hdeg₁ :
  finrank.{u, v} F ↥F⟮a⟯ ≤ Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
hdeg₂ :
  finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
hdeg₃ : finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤ finrank.{u, v} F ↥F⟮((iterateFrobenius E q n : (a : E) → E) a : E)⟯
⊢ Polynomial.natDegree (Polynomial.map (iterateFrobenius F q n) (minpoly F a)) ≤
    Polynomial.natDegree (minpoly F (B := E) ((iterateFrobenius E q n : (a : E) → E) a : E))
have hdeg₄ : finrank.{u, v} F ↥F⟮a ^ q ^ n⟯ ≤ finrank.{u, v} F ↥F⟮a ^ q ^ n⟯
Tactic: rw [(minpoly F a).natDegree_map_eq_of_injective (iterateFrobenius F q n).injective,
      ← IntermediateField.adjoin.finrank hai,
      IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable F E hsep q n,
      ← IntermediateField.adjoin.finrank hapi, iterateFrobenius_def]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
⊢ PerfectField F
have this : ExpChar E p
Tactic: haveI := expChar_of_injective_algebraMap (algebraMap F E).injective p
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x
have obtain : ∀ (y : E) (h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)),
  ∃ (a : F), (frobenius F p : (a : F) → F) a = x
Tactic: obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
⊢ (algebraMap F E : (a : F) → E) x = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
have rw : (frobenius E p : (a : E) → E) y = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
Tactic: rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
rw : (frobenius E p : (a : E) → E) y = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
⊢ (algebraMap F E : (a : F) → E) x = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
have rw₁ : (frobenius E p : (a : E) → E) y = y ^ ringExpChar F
Tactic: rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
rw : (frobenius E p : (a : E) → E) y = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
rw₁ : (frobenius E p : (a : E) → E) y = y ^ ringExpChar F
⊢ (algebraMap F E : (a : F) → E) x = y ^ HPow.hPow (β := ℕ) (ringExpChar F) 1
have rw₂ : y ^ p = y ^ ringExpChar F
Tactic: rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x
have this₁ : Membership.mem (γ := IntermediateField F E) (perfectClosure F E) y
Tactic: have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
x : F
y : E
h : Eq (α := E) ((frobenius E p : (a : E) → E) y : E) ((algebraMap F E : (a : F) → E) x : E)
this : Membership.mem (γ := IntermediateField F E) (perfectClosure F E) y
⊢ ∃ (a : F), (frobenius F p : (a : F) → F) a = x
have obtain : ∀ (z : F)
  (h :
    Eq (α := E) ((frobenius E p : (a : E) → E) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E) : E)
      ((algebraMap F E : (a : F) → E) x : E))
  (this :
    Membership.mem (α := E) (γ := IntermediateField F E) (perfectClosure F E)
      ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)),
  ∃ (a : F), (frobenius F p : (a : F) → F) a = x
Tactic: obtain ⟨z, rfl⟩ := eq ▸ this
Cleared hypotheses: y, h, this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h_1 : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this_1 : ExpChar E p
x z : F
h :
  Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    ((algebraMap F E : (a : F) → E) x : E)
this :
  Membership.mem (α := E) (γ := IntermediateField F E) (perfectClosure F E)
    ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)
⊢ Eq (α := E) ((frobenius E p : (a : E) → E) ((algebraMap F E : (a : F) → E) z : E) : E)
    (((algebraMap F E : F →+* E) : (a : F) → E) x : E)
have rw : Eq.{v + 1} (α := E) ((algebraMap F E : (a : F) → E) x : E) (((algebraMap F E : F →+* E) : (a : F) → E) x : E)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.PerfectClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
h : PerfectField E
eq : Eq (α := IntermediateField F E) (perfectClosure F E) ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
⊢ PerfectField F
have this₁ : PerfectRing F p
Tactic: haveI := PerfectRing.ofSurjective F p fun x ↦ by
    obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)
    have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
    obtain ⟨z, rfl⟩ := eq ▸ this
    simp only [Algebra.ofId] at h
    exact ⟨z, (algebraMap F E).injective (by rw [RingHom.map_frobenius]; rw [h])⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
⊢ LinearIndependent E v
have obtain : ∀ (q : ℕ), ExpChar F q → LinearIndependent E v
Tactic: obtain ⟨q, _⟩ := ExpChar.exists F
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
⊢ LinearIndependent E v
have this : ExpChar K q
Tactic: haveI := expChar_of_injective_algebraMap (algebraMap F K).injective q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this : ExpChar K q
⊢ LinearIndependent E v
have refine : ∀ (l : ι →₀ E) (hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)) (i : ι),
  Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
Tactic: refine linearIndependent_iff.mpr fun l hl ↦ Finsupp.ext fun i ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i : ι
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
have choose : ∀ (f : (i : ι) → ℕ)
  (hf :
    ∀ (i : ι),
      Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
        (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))),
  Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
Tactic: choose f hf using fun i ↦ (isPurelyInseparable_iff_pow_mem F q).1 ‹_› (l i)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
have this₁ : q ^ n ≠ 0
Tactic: have := (expChar_pow_pos F q n).ne'
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
have pos : ∀ (hs : i ∈ l.support),
  Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
Tactic: by_cases hs : i ∈ l.support
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
pos :
  ∀ (hs : i ∈ l.support),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
have neg : ∀ (hs : i ∉ l.support),
  Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
Tactic: by_cases hs : i ∈ l.support
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
have h₁ : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i) ^ q ^ (n - f i)
Tactic: convert! pow_mem (hf i) (q ^ (n - f i)) using 1
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i) ^ q ^ (n - f i)
have h₁ : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i * q ^ (n - f i))
Tactic: rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
h₁ :
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i * q ^ (n - f i))
⊢ HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i) ^ q ^ (n - f i)
have h₂ : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ (f i + (n - f i)))
Tactic: rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
h₁ :
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i * q ^ (n - f i))
h₂ :
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ (f i + (n - f i)))
⊢ HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i) ^ q ^ (n - f i)
have h₃ : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ l.support.sup f)
Tactic: rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)
have rw : 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)
Tactic: rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
rw : 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)
have rw₁ : 0 = HPow.hPow (α := E) 0 (q ^ n)
Tactic: rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i_1 : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
rw : 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)
rw₁ : 0 = HPow.hPow (α := E) 0 (q ^ n)
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)
have rw₂ : Eq.{v + 1} (α := E) 0 0
Tactic: rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i : ι
f : (i : ι) → ℕ
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ f i))
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
have hf₁ : ∀ (i : ι),
  Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
Tactic: replace hf (i : ι) : l i ^ q ^ n ∈ (algebraMap F E).range := by
    by_cases hs : i ∈ l.support
    · convert! pow_mem (hf i) (q ^ (n - f i)) using 1
      rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)]
    exact ⟨0, by rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h_1 : ExpChar F q
this_1 : ExpChar K q
l : ι →₀ E
hl : Eq.{w + 1} (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (0 : K)
i : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
hf :
  ∀ (i : ι),
    Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
      (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
have choose : ∀ (lF : (i : ι) → F)
  (hlF :
    ∀ (i : ι),
      ((algebraMap F E : F →+* E) : (a : F) → E) (lF i) = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)),
  Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
Tactic: choose lF hlF using hf
Cleared hypotheses: hf