awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 : ι
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)
⊢ 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)

Premises used: isPurelyInseparable_iff_pow_mem, Iff.mp, DFunLike.coe
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ q ^ n ≠ 0

Tactic:
have := (expChar_pow_pos F q n).ne'
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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))
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))
⊢ 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

Premises used: Finsupp.support
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 ^ f i) ^ q ^ (n - f i))

Tactic:
pow_mem (hf i) (q ^ (n - f i))

Premises used: HSub.hSub, HPow.hPow, pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)
⊢ Membership.mem (γ := Subring E) (RingHom.range.{u, v} (R := F) (algebraMap F E))
    (HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n))

Tactic:
convert! pow_mem (hf i) (q ^ (n - f i)) using 1

Premises used: HSub.hSub, HPow.hPow, pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)))
h₃ h₄ :
  HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n) =
    HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ l.support.sup f)
⊢ 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)]

Premises used: pow_add, Nat.add_sub_of_le, pow_mul, Finset.le_sup
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)
rw₂ rw₃ : Eq.{v + 1} (α := E) 0 0
⊢ ((algebraMap F E : F →+* E) : (a : F) → E) 0 = HPow.hPow (α := E) ((l : (a : ι) → E) i : E) (q ^ n)

Tactic:
rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]

Premises used: Finsupp.notMem_support_iff, map_zero, Iff.mp, zero_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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))

Tactic:
exact ⟨0, by rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
⊢ ∀ (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]⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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))
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)
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)

Tactic:
choose lF hlF using hf
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 : ι
contrapose : i ∉ l.support → lF i = 0
⊢ lF i ≠ 0 → i ∈ l.support

Tactic:
contrapose
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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

Tactic:
fun hs ↦ (injective_iff_map_eq_zero _).mp (algebraMap F E).injective _ ?_

Premises used: Algebra.algebraMap, RingHom.injective, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 : ι
refine : ∀ (hs : i ∉ l.support), Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
⊢ i ∉ l.support → lF i = 0

Tactic:
refine fun hs ↦ (injective_iff_map_eq_zero _).mp (algebraMap F E).injective _ ?_

Premises used: Algebra.algebraMap, RingHom.injective, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
rw₂ rw₃ : Eq.{v + 1} (α := E) 0 0
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)

Tactic:
rw [hlF, Finsupp.notMem_support_iff.1 hs, zero_pow this]

Premises used: Finsupp.notMem_support_iff, Iff.mp, zero_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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 ⋯
⊢ 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)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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) (∑ 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

Premises used: sum_pow_char_pow, Finsupp.sum, Finsupp.linearCombination_apply, zero_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
x : ι
⊢ HSMul.hSMul.{u, w, w} (α := F) 0 (v x ^ q ^ n) = 0

Tactic:
zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
x : ι
⊢ HSMul.hSMul.{u, w, w} (α := F) 0 (v x ^ q ^ n) = 0

Tactic:
exact zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
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)
⊢ Eq.{w + 1} (α := K) ((Finsupp.linearCombination F fun (x : ι) ↦ v x ^ q ^ n : (a : ι →₀ F) → K) lF₀ : K) (0 : K)

Tactic:
rw [← hl, Finsupp.linearCombination_apply,
      Finsupp.onFinset_sum _ (fun _ ↦ by exact zero_smul _ _)]

Premises used: Finsupp.onFinset_sum, Finsupp.linearCombination_apply
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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)

Tactic:
Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
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
⊢ 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:
refine Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Tower
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
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
⊢ lF i • v i ^ q ^ n = HSMul.hSMul.{v, w, w} (α := E) ((l : (a : ι) → E) i : E) (v i) ^ q ^ n

Tactic:
simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]

Premises used: map_pow, Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply