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

Tactic:
set L := adjoin E S

Premises used: IntermediateField.adjoin
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
rw : M ≤ adjoin F ((↑E' : Set K) ∪ S)
⊢ M ≤ restrictScalars F L

Tactic:
rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]

Premises used: IntermediateField.restrictScalars_adjoin_of_algEquiv, IntermediateField.restrictScalars_adjoin, 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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ M ≤ adjoin F ((↑E' : Set K) ∪ S)

Tactic:
adjoin.mono _ _ _ Set.subset_union_right

Premises used: IntermediateField.adjoin.mono, Set.Mem, Set.subset_union_right
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ M ≤ adjoin F ((↑E' : Set K) ∪ S)

Tactic:
exact adjoin.mono _ _ _ Set.subset_union_right

Premises used: IntermediateField.adjoin.mono, Set.subset_union_right
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ M ≤ restrictScalars F L

Tactic:
have hi : M ≤ L.restrictScalars F := by
    rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]
    exact adjoin.mono _ _ _ Set.subset_union_right
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
⊢ IsScalarTower.{u, w, w} F ↥M ↥L

Tactic:
haveI : IsScalarTower F M L := 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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this : IsScalarTower.{u, w, w} F ↥M ↥L
change : IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)
⊢ IsPurelyInseparable.{w, w} ↥M ↥L

Tactic:
change IsPurelyInseparable M (extendScalars hi)

Premises used: Membership.mem, Subtype, IntermediateField.extendScalars, IsPurelyInseparable
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this : IsScalarTower.{u, w, w} F ↥M ↥L
obtain : ∀ (q : ℕ), ExpChar F q → IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)
⊢ IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Premises used: ExpChar.exists
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
rw : restrictScalars F (L' := ↥(adjoin F S)) (adjoin ↥(adjoin F S) (↑E' : Set K))
| restrictScalars F (extendScalars hi)

Tactic:
rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]

Premises used: IntermediateField.restrictScalars_adjoin_of_algEquiv, IntermediateField.adjoin_adjoin_comm, IntermediateField.extendScalars_restrictScalars, IntermediateField.adjoin_self, 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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
conv_lhs :
  Eq (α := IntermediateField F K) (restrictScalars F (extendScalars hi))
    (restrictScalars F (L' := ↥M) (adjoin ↥M (↑E' : Set K)))
conv_lhs₁ :
  Eq (α := IntermediateField F K) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin ↥(adjoin F S) (↑E' : Set K)))
    (restrictScalars F (L' := ↥M) (adjoin ↥M (↑E' : Set K)))
⊢ Eq (α := IntermediateField F K) (restrictScalars F (extendScalars hi))
    (restrictScalars F (L' := ↥M) (adjoin ↥M (↑E' : Set K)))

Tactic:
conv_lhs => rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]

Premises used: IntermediateField.restrictScalars_adjoin_of_algEquiv, IntermediateField.adjoin_adjoin_comm, IntermediateField.extendScalars_restrictScalars, IntermediateField.adjoin_self, 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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
⊢ extendScalars hi = adjoin ↥M (↑E' : Set K)

Tactic:
have : extendScalars hi = adjoin M (E' : Set K) := restrictScalars_injective F <| by
      conv_lhs => rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
this : extendScalars hi = adjoin ↥M (↑E' : Set K)
rw :
  ∀ x ∈ (↑E' : Set K),
    ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)
⊢ IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)

Tactic:
rw [this, isPurelyInseparable_adjoin_iff_pow_mem _ _ q]

Premises used: IntermediateField.isPurelyInseparable_adjoin_iff_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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
this : extendScalars hi = adjoin ↥M (↑E' : Set K)
x : K
y : E
hy : (AlgHom.toRingHom (IsScalarTower.toAlgHom F E K) : (a : E) → K) y = x
obtain :
  ∀ (n : ℕ) (z : F) (hz : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ n),
    ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)

Tactic:
obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y

Premises used: IsPurelyInseparable.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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
this : extendScalars hi = adjoin ↥M (↑E' : Set K)
x : K
y : E
hy : (AlgHom.toRingHom (IsScalarTower.toAlgHom F E K) : (a : E) → K) y = x
n : ℕ
z : F
hz : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)

Tactic:
⟨n, algebraMap F M z, ?_⟩

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Exists.intro, 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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
this : extendScalars hi = adjoin ↥M (↑E' : Set K)
x : K
y : E
hy : (AlgHom.toRingHom (IsScalarTower.toAlgHom F E K) : (a : E) → K) y = x
n : ℕ
z : F
hz : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ n
refine : (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)

Tactic:
refine ⟨n, algebraMap F M z, ?_⟩
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
this : extendScalars hi = adjoin ↥M (↑E' : Set K)
x : K
y : E
hy : (AlgHom.toRingHom (IsScalarTower.toAlgHom F E K) : (a : E) → K) y = x
n : ℕ
z : F
hz : ((algebraMap F E : F →+* E) : (a : F) → E) z = y ^ q ^ n
rw : (algebraMap F K : (a : F) → K) z = x ^ q ^ n
rw₁ : (algebraMap E K : (a : E) → K) ((algebraMap F E : (a : F) → E) z : E) = x ^ q ^ n
rw₂ : (algebraMap E K : (a : E) → K) (y ^ q ^ n) = x ^ q ^ n
rw₃ :
  (algebraMap E K : (a : E) → K) (y ^ q ^ n) =
    HPow.hPow (α := K) ((AlgHom.toRingHom (IsScalarTower.toAlgHom F E K) : (a : E) → K) y : K) (q ^ n)
rw₄ :
  HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ n) =
    HPow.hPow (α := K) ((AlgHom.toRingHom (IsScalarTower.toAlgHom F E K) : (a : E) → K) y : K) (q ^ n)
rw₅ :
  HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ n) =
    HPow.hPow (α := K) (((↑(IsScalarTower.toAlgHom F E K) : E →+* K) : (a : E) → K) y : K) (q ^ n)
rw₆ rw₇ :
  HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ n) =
    HPow.hPow (α := K) ((algebraMap E K : (a : E) → K) y : K) (q ^ n)
⊢ (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n

Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]

Premises used: IsScalarTower.coe_toAlgHom, map_pow, AlgHom.toRingHom_eq_coe, IsScalarTower.algebraMap_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
S : Set K
inst_7 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this : IsScalarTower.{u, w, w} F ↥M ↥L
⊢ IsPurelyInseparable.{w, w} ↥M ↥L

Tactic:
haveI : IsPurelyInseparable M L := by
    change IsPurelyInseparable M (extendScalars hi)
    obtain ⟨q, _⟩ := ExpChar.exists F
    have : extendScalars hi = adjoin M (E' : Set K) := restrictScalars_injective F <| by
      conv_lhs => rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]
    rw [this, isPurelyInseparable_adjoin_iff_pow_mem _ _ q]
    rintro x ⟨y, hy⟩
    obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y
    refine ⟨n, algebraMap F M z, ?_⟩
    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
this : IsPurelyInseparable.{w, w} ↥M ↥L
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E ↥L) = Cardinal.lift.{v, w} (sepDegree F ↥L)

Tactic:
have h := lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E L
-- 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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
this : IsPurelyInseparable.{w, w} ↥M ↥L
h : Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E ↥L) = Cardinal.lift.{v, w} (sepDegree F ↥L)
⊢ Cardinal.lift.{v, w} (sepDegree E ↥L) = Cardinal.lift.{v, w} (sepDegree F ↥L)

Tactic:
rw [IsPurelyInseparable.sepDegree_eq_one F E, Cardinal.lift_one, one_mul] at h

Premises used: IsPurelyInseparable.sepDegree_eq_one, Cardinal.lift_one, one_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 : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst_8 : Algebra.IsAlgebraic.{u, w} F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := AlgHom.fieldRange (IsScalarTower.toAlgHom F E K)
j : AlgEquiv.{u, v, w} F E ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this_1 : Algebra ↥M ↥L := i.toAlgebra
this_2 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
this_3 : IsScalarTower.{u, w, w} F ↥M ↥L
this : IsPurelyInseparable.{w, w} ↥M ↥L
h : Cardinal.lift.{v, w} (sepDegree E ↥L) = Cardinal.lift.{v, w} (sepDegree F ↥L)
rw : sepDegree F ↥L = sepDegree F ↥M
rw₁ : sepDegree F ↥M * sepDegree ↥M ↥L = sepDegree F ↥M
rw₂ : sepDegree F ↥M * 1 = sepDegree F ↥M
rw₃ rw₄ : sepDegree F ↥M = sepDegree F ↥M
⊢ sepDegree E ↥L = sepDegree F ↥M

Tactic:
rw [Cardinal.lift_injective h, ← sepDegree_mul_sepDegree_of_isAlgebraic F M L,
    IsPurelyInseparable.sepDegree_eq_one M L, mul_one]

Premises used: IsPurelyInseparable.sepDegree_eq_one, Membership.mem, Subtype, mul_one, Field.sepDegree_mul_sepDegree_of_isAlgebraic, Cardinal.lift_injective
-- 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 : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
rwa rwa₁ rwa₂ rwa₃ : Algebra.IsAlgebraic.{u, w} F ↥S
⊢ Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))

Tactic:
rwa [adjoin_self]

Premises used: IntermediateField.adjoin_self