awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
i : ι
⊢ lF i ≠ 0 → i ∈ l.support
have contrapose : i ∉ l.support → lF i = 0
Tactic: contrapose
-- 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
i : ι
⊢ i ∉ l.support → lF i = 0
have refine : ∀ (hs : i ∉ l.support), Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
Tactic: refine fun hs ↦ (injective_iff_map_eq_zero _).mp (algebraMap F E).injective _ ?_
-- 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
i : ι
hs : i ∉ l.support
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
have rw : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) = 0
Tactic: rw [hlF, 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
i : ι
hs : i ∉ l.support
rw : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) = 0
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
have rw₁ : HPow.hPow (α := E) 0 (q ^ n) = 0
Tactic: rw [hlF, 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
i : ι
hs : i ∉ l.support
rw : HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) = 0
rw₁ : HPow.hPow (α := E) 0 (q ^ n) = 0
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
have rw₂ : Eq.{v + 1} (α := E) 0 0
Tactic: rw [hlF, 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
⊢ Eq.{w + 1} (α := K) ((Finsupp.linearCombination F fun (x : ι) ↦ v x ^ q ^ n : (a : ι →₀ F) → K) lF₀ : K) (0 : K)
have hl₁ : HPow.hPow (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (q ^ n) = HPow.hPow (α := K) 0 (q ^ n)
Tactic: replace hl := congr($hl ^ q ^ n)
Cleared hypotheses: hl
-- 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
i : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl :
  HPow.hPow (α := K) ((Finsupp.linearCombination E v : (a : ι →₀ E) → K) l : K) (q ^ n) = HPow.hPow (α := K) 0 (q ^ n)
⊢ Eq.{w + 1} (α := K) ((Finsupp.linearCombination F fun (x : ι) ↦ v x ^ q ^ n : (a : ι →₀ F) → K) lF₀ : K) (0 : K)
have hl₁ : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
Tactic: rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_pow_char_pow, zero_pow this] at hl
Cleared hypotheses: hl
-- 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
i : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
⊢ Eq.{w + 1} (α := K) ((Finsupp.linearCombination F fun (x : ι) ↦ v x ^ q ^ n : (a : ι →₀ F) → K) lF₀ : K) (0 : K)
have rw : Eq.{w + 1} (α := K) (∑ a ∈ l.support, lF a • v a ^ q ^ n)
  (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n)
Tactic: rw [← hl, Finsupp.linearCombination_apply,
      Finsupp.onFinset_sum _ (fun _ ↦ by exact zero_smul _ _)]
-- 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
i : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
⊢ Eq.{w + 1} (α := K) (∑ a ∈ l.support, lF a • v a ^ q ^ n)
    (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n)
have refine : ∀ i ∈ l.support, lF i • v i ^ q ^ n = HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n
Tactic: refine Finset.sum_congr rfl 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_1 : ExpChar K q
l : ι →₀ E
i_1 : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
i : ι
h_2 : i ∈ l.support
⊢ lF i • v i ^ q ^ n = HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n
have simp_rw : HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
  HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (v i) ^ q ^ n
Tactic: simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
-- 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
i_1 : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
i : ι
h_2 : i ∈ l.support
simp_rw :
  HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
    HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (v i) ^ q ^ n
⊢ lF i • v i ^ q ^ n = HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n
have simp_rw₁ : HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
  HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (q ^ n) * v i ^ q ^ n
Tactic: simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
-- 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
i_1 : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
i : ι
h_2 : i ∈ l.support
simp_rw :
  HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
    HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (v i) ^ q ^ n
simp_rw₁ :
  HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
    HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (q ^ n) * v i ^ q ^ n
⊢ lF i • v i ^ q ^ n = HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n
have simp_rw₂ : HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) (lF i) : E) : K) (v i ^ q ^ n) =
  HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (q ^ n) * v i ^ q ^ n
Tactic: simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
-- 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
i_1 : ι
f : (i : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
hl : Eq.{w + 1} (α := K) (∑ i ∈ l.support, HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n) 0
i : ι
h_2 : i ∈ l.support
simp_rw :
  HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
    HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (v i) ^ q ^ n
simp_rw₁ :
  HMul.hMul (α := K) ((algebraMap F K : (a : F) → K) (lF i) : K) (v i ^ q ^ n) =
    HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (q ^ n) * v i ^ q ^ n
simp_rw₂ :
  HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) (lF i) : E) : K) (v i ^ q ^ n) =
    HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (q ^ n) * v i ^ q ^ n
⊢ lF i • v i ^ q ^ n = HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n
have simp_rw₃ : HMul.hMul (α := K) ((algebraMap E K : (a : E) → K) (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)) : K)
    (v i ^ q ^ n) =
  HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) ((l : (a : ι) → E) i : E) : K) (q ^ n) * v i ^ q ^ n
Tactic: simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
-- 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 : ι) → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
have h₁ : lF₀ = 0
Tactic: replace h := linearIndependent_iff.1 (h.map_pow_expChar_pow_of_isSeparable' q n hsep) lF₀ <| by
    replace hl := congr($hl ^ q ^ n)
    rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_pow_char_pow, zero_pow this] at hl
    rw [← hl, Finsupp.linearCombination_apply,
      Finsupp.onFinset_sum _ (fun _ ↦ by exact zero_smul _ _)]
    refine Finset.sum_congr rfl fun i _ ↦ ?_
    simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
Cleared hypotheses: 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)
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
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
h : lF₀ = 0
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)
have refine : Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
Tactic: refine eq_zero_of_pow_eq_zero ((hlF _).symm.trans ?_)
-- 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)
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
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)
lF₀ : ι →₀ F := Finsupp.onFinset l.support lF ⋯
h : lF₀ = 0
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
have h₁ : lF i = 0
Tactic: convert! map_zero (algebraMap F E)
-- 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
inst_8 : Algebra.IsSeparable E K
⊢ sepDegree F K = Module.rank E K
have h : Module.rank F ↥(separableClosure F K) = Module.rank E ↥(adjoin E (↑(separableClosure F K) : Set K))
Tactic: have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.adjoin_rank_eq_rank_left_of_isAlgebraic_left |>.symm
-- 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
inst_8 : Algebra.IsSeparable E K
h : Module.rank F ↥(separableClosure F K) = Module.rank E ↥(adjoin E (↑(separableClosure F K) : Set K))
⊢ sepDegree F K = Module.rank E K
have rwa : ∀ (h : Module.rank F ↥(separableClosure F K) = Module.rank E ↥⊤), sepDegree F K = Module.rank E K
Tactic: rwa [separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable K, rank_top'] at h
Cleared hypotheses: 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
inst_8 : Algebra.IsSeparable E K
h : Module.rank F ↥(separableClosure F K) = Module.rank E ↥(adjoin E (↑(separableClosure F K) : Set K))
rwa : ∀ (h : Module.rank F ↥(separableClosure F K) = Module.rank E ↥⊤), sepDegree F K = Module.rank E K
⊢ sepDegree F K = Module.rank E K
have rwa₁ : ∀ (h : Module.rank F ↥(separableClosure F K) = Module.rank E K), sepDegree F K = Module.rank E K
Tactic: rwa [separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable K, rank_top'] at h
Cleared hypotheses: 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 : Algebra.IsSeparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
have rw : Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank E ↥(separableClosure E K)) =
  Cardinal.lift.{v, w} (Module.rank F ↥(restrictScalars F (separableClosure E K)))
Tactic: rw [sepDegree, sepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]
-- 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 : Algebra.IsSeparable F E
⊢ insepDegree F K = insepDegree E K
have rw : Module.rank (↥(restrictScalars F (separableClosure E K))) K = Module.rank (↥(separableClosure E K)) K
Tactic: rw [insepDegree, insepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]
-- 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
⊢ sepDegree F K = sepDegree E K
have h : sepDegree F K = sepDegree F ↥(separableClosure E K)
Tactic: convert! sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K)
-- 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
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)
have this : IsScalarTower F (↥(separableClosure E K)) K
Tactic: haveI : IsScalarTower F (separableClosure E K) K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- 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
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)
have h : Module.rank F
    ↥(IntermediateField.map (L := ↥(separableClosure E K)) (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K)
        (separableClosure F ↥(separableClosure E K))) =
  sepDegree F ↥(separableClosure E K)
Tactic: rw [sepDegree, ← separableClosure.map_eq_of_separableClosure_eq_bot F
    (separableClosure.separableClosure_eq_bot E K)]