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_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 ⋯
⊢ 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]
-- 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)
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)

Tactic:
eq_zero_of_pow_eq_zero ((hlF _).symm.trans ?_)

Premises used: eq_zero_of_pow_eq_zero, Eq.symm, Eq.trans
-- 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)
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
refine : Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)
⊢ Eq.{v + 1} (α := E) ((l : (a : ι) → E) i : E) ((0 : (a : ι) → E) i : E)

Tactic:
refine eq_zero_of_pow_eq_zero ((hlF _).symm.trans ?_)

Premises used: eq_zero_of_pow_eq_zero, Eq.symm, Eq.trans
-- 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)
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 : (a : F) → E) 0 : E) (0 : E)

Tactic:
map_zero (algebraMap F E)

Premises used: Algebra.algebraMap, map_zero
-- 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)
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
h₁ : lF i = 0
⊢ Eq.{v + 1} (α := E) (((algebraMap F E : F →+* E) : (a : F) → E) (lF i) : E) (0 : E)

Tactic:
convert! map_zero (algebraMap F E)

Premises used: Algebra.algebraMap, map_zero
-- 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)
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
⊢ lF i = 0

Tactic:
congr($h i)

Premises used: congrArg, id, 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)
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
⊢ lF i = 0

Tactic:
exact congr($h i)
-- 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
S : IntermediateField F K
inst_8 : Algebra.IsSeparable.{u, w} F ↥S
ι : Set ↥S
b : Module.Basis.{w, u, w} (↑ι : Type w) F ↥S
i : (↑ι : Type w)
⊢ IsSeparable F (K := K) (Function.comp (β := ↥S) (⇑S.val : (a : ↥S) → K) (⇑b : (a : (↑ι : Type w)) → ↥S) i)

Tactic:
simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (b i)

Premises used: Algebra.IsSeparable.isSeparable, IntermediateField.minpoly_eq, IsSeparable, 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
inst_8 : Algebra.IsSeparable E K
⊢ 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
-- 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
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : Module.rank F ↥(separableClosure F K) = Module.rank E K), sepDegree 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

Premises used: IntermediateField.rank_top', separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable
-- 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 : Algebra.IsSeparable F E
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)))
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
rw [sepDegree, sepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]

Premises used: Field.sepDegree, separableClosure.eq_restrictScalars_of_isSeparable
-- 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 : Algebra.IsSeparable F E
⊢ 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:
lift_rank_mul_lift_rank F E (separableClosure E K)

Premises used: IntermediateField.restrictScalars, lift_rank_mul_lift_rank, Set.Mem, setOf, Membership.mem, Subtype, IsSeparable, Polynomial.Separable, separableClosure, IsCoprime
-- 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 : Algebra.IsSeparable F E
⊢ 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:
exact lift_rank_mul_lift_rank F E (separableClosure E K)

Premises used: lift_rank_mul_lift_rank, Membership.mem, Subtype, separableClosure
-- 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 v
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
⊢ Module.rank F E * sepDegree E K = sepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_mul_lift_sepDegree_of_isSeparable F E K

Premises used: Field.lift_rank_mul_lift_sepDegree_of_isSeparable, Cardinal.lift_id
-- 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 : Algebra.IsSeparable F E
rw : Module.rank (↥(restrictScalars F (separableClosure E K))) K = Module.rank (↥(separableClosure E K)) K
⊢ insepDegree F K = insepDegree E K

Tactic:
rw [insepDegree, insepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]

Premises used: Field.insepDegree, separableClosure.eq_restrictScalars_of_isSeparable
-- 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 : Algebra.IsSeparable F E
⊢ Module.rank (↥(restrictScalars F (separableClosure E K))) K = Module.rank (↥(separableClosure E K)) K

Tactic:
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
⊢ sepDegree F ↥(separableClosure E K) = Module.rank E ↥(separableClosure E K)

Tactic:
sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K)

Premises used: Membership.mem, Subtype, Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable, separableClosure
-- 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
h : sepDegree F K = sepDegree F ↥(separableClosure E K)
⊢ sepDegree F K = sepDegree E K

Tactic:
convert! sepDegree_eq_of_isPurelyInseparable_of_isSeparable F E (separableClosure E K)

Premises used: Membership.mem, Subtype, Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable, separableClosure
-- 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
⊢ IsScalarTower F (↥(separableClosure E K)) K

Tactic:
haveI : IsScalarTower F (separableClosure E K) K := IsScalarTower.of_algebraMap_eq (congrFun 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
this : IsScalarTower F (↥(separableClosure E K)) K
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)
⊢ sepDegree F K = sepDegree F ↥(separableClosure E K)

Tactic:
rw [sepDegree, ← separableClosure.map_eq_of_separableClosure_eq_bot F
    (separableClosure.separableClosure_eq_bot E K)]

Premises used: Field.sepDegree, separableClosure.map_eq_of_separableClosure_eq_bot, separableClosure.separableClosure_eq_bot
-- 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
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ 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:
(separableClosure F (separableClosure E K)).equivMap
    (IsScalarTower.toAlgHom F (separableClosure E K) K) |>.symm.toLinearEquiv.rank_eq

Premises used: AlgEquiv.symm, Set.Mem, Field.sepDegree, IsScalarTower.toAlgHom, Membership.mem, Subtype, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, IntermediateField.equivMap, IntermediateField.map, separableClosure
-- 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
this : IsScalarTower F (↥(separableClosure E K)) K
⊢ 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:
exact (separableClosure F (separableClosure E K)).equivMap
    (IsScalarTower.toAlgHom F (separableClosure E K) K) |>.symm.toLinearEquiv.rank_eq

Premises used: AlgEquiv.symm, IsScalarTower.toAlgHom, Membership.mem, Subtype, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, IntermediateField.equivMap, separableClosure
-- 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
⊢ Cardinal.lift.{w, v} (Module.rank F E) *
      Cardinal.lift.{v, w} (Module.rank (↥(adjoin E (↑(separableClosure F K) : Set K))) K) =
    Cardinal.lift.{v, w} (Module.rank (↥(separableClosure F K)) K)

Tactic:
have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left
-- 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
h :
  Cardinal.lift.{w, v} (Module.rank F E) *
      Cardinal.lift.{v, w} (Module.rank (↥(adjoin E (↑(separableClosure F K) : Set K))) K) =
    Cardinal.lift.{v, w} (Module.rank (↥(separableClosure F K)) K)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank (↥(separableClosure E K)) K) =
        Cardinal.lift.{v, w} (Module.rank (↥(separableClosure F K)) K)),
    Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
      Cardinal.lift.{v, w} (insepDegree F K)
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
rwa [separableClosure.adjoin_eq_of_isAlgebraic] at h

Premises used: separableClosure.adjoin_eq_of_isAlgebraic
-- 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 v
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
⊢ Module.rank F E * insepDegree E K = insepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_rank_mul_lift_insepDegree_of_isPurelyInseparable F E K

Premises used: Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable, Cardinal.lift_id
-- 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 : Algebra.IsAlgebraic F E
⊢ Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) *
      Cardinal.lift.{v, w} (sepDegree.{v, w} (↥(separableClosure F E)) K) =
    Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
have h := lift_rank_mul_lift_sepDegree_of_isSeparable F (separableClosure F E) K
-- 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 : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) *
      Cardinal.lift.{v, w} (sepDegree.{v, w} (↥(separableClosure F E)) K) =
    Cardinal.lift.{v, w} (sepDegree F K)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) * Cardinal.lift.{v, w} (sepDegree E K) =
        Cardinal.lift.{v, w} (sepDegree F K)),
    Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
rwa [sepDegree_eq_of_isPurelyInseparable (separableClosure F E) E K] at h

Premises used: Membership.mem, Subtype, Field.sepDegree_eq_of_isPurelyInseparable, separableClosure
-- 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 v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
⊢ sepDegree F E * sepDegree E K = sepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E K

Premises used: Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, Cardinal.lift_id
-- 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 : Algebra.IsAlgebraic F E
⊢ Cardinal.lift.{w, v} (Module.rank (↥(separableClosure F E)) E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree.{v, w} (↥(separableClosure F E)) K)

Tactic:
have h := lift_rank_mul_lift_insepDegree_of_isPurelyInseparable (separableClosure F E) E K
-- 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 : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank (↥(separableClosure F E)) E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree.{v, w} (↥(separableClosure F E)) K)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Cardinal.lift.{w, v} (Module.rank (↥(separableClosure F E)) E) * Cardinal.lift.{v, w} (insepDegree E K) =
        Cardinal.lift.{v, w} (insepDegree F K)),
    Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
      Cardinal.lift.{v, w} (insepDegree F K)
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
rwa [← insepDegree_eq_of_isSeparable F (separableClosure F E) K] at h

Premises used: Membership.mem, Subtype, separableClosure, Field.insepDegree_eq_of_isSeparable
-- 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 v
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
⊢ insepDegree F E * insepDegree E K = insepDegree F K

Tactic:
simpa only [Cardinal.lift_id] using lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic F E K

Premises used: Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic, Cardinal.lift_id
-- 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 : Algebra.IsAlgebraic F E
⊢ finInsepDegree F E * finInsepDegree E K = finInsepDegree F K

Tactic:
simpa only [map_mul, Cardinal.toNat_lift] using
    congr(Cardinal.toNat $(lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic F E K))

Premises used: Cardinal.toNat_lift, map_mul
-- 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
S : Set K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F S)
inst_8 : IsPurelyInseparable F E
set :
  let M : IntermediateField F K := adjoin F S;
  Algebra.IsAlgebraic.{u, w} F ↥M → sepDegree E ↥(adjoin E S) = sepDegree F ↥M
⊢ sepDegree E ↥(adjoin E S) = sepDegree F ↥(adjoin F S)

Tactic:
set M := adjoin F S

Premises used: IntermediateField.adjoin