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
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
⊢ (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
have 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)
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
-- 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
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)
⊢ (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
have 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)
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
-- 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
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)
⊢ (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
have 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)
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
-- 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
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)
⊢ (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
have 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)
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
-- 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
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
⊢ sepDegree E ↥L = sepDegree F ↥M
have this₁ : 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]
-- 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
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
⊢ sepDegree E ↥L = sepDegree F ↥M
have h : 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
-- 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
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)
⊢ sepDegree E ↥L = sepDegree F ↥M
have h₁ : 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
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
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)
⊢ sepDegree E ↥L = sepDegree F ↥M
have rw : sepDegree F ↥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]
-- 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
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
⊢ sepDegree E ↥L = sepDegree F ↥M
have rw₁ : sepDegree F ↥M * sepDegree ↥M ↥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]
-- 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
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
⊢ sepDegree E ↥L = sepDegree F ↥M
have rw₂ : sepDegree F ↥M * 1 = 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]
-- 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
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
⊢ sepDegree E ↥L = sepDegree F ↥M
have rw₃ : sepDegree F ↥M = 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]
-- 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
S : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
⊢ sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S
have this : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))
Tactic: have : Algebra.IsAlgebraic F (adjoin F (S : Set K)) := by rwa [adjoin_self]
-- 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
S : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
this : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))
⊢ sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S
have this₁ : sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥(adjoin F (↑S : Set K))
Tactic: have := sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E (S : Set 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
S : IntermediateField F K
inst_7 : Algebra.IsAlgebraic.{u, w} F ↥S
inst_8 : IsPurelyInseparable F E
this_1 : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F (↑S : Set K))
this : sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥(adjoin F (↑S : Set K))
⊢ sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S
have rwa : ∀ (this : sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S), sepDegree E ↥(adjoin E (↑S : Set K)) = sepDegree F ↥S
Tactic: rwa [adjoin_self] at this
Cleared hypotheses: 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)
have hi : IsIntegral F x
Tactic: have hi := IsSeparable.isIntegral hsep
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)
have hi' : IsIntegral E x
Tactic: have hi' : IsIntegral E x := IsIntegral.tower_top hi
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) (minpoly F x)) (minpoly E x)
have refine : natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le (monic hi') ((monic hi).map (algebraMap F E))
    (dvd_map_of_isScalarTower F E x) (le_of_eq ?_)
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have hsep' : IsSeparable E x
Tactic: have hsep' := IsSeparable.tower_top E hsep
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have this : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
Tactic: haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have this₁ : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
Tactic: haveI := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep'
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have this₁ : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
Tactic: have := Algebra.IsSeparable.isAlgebraic F F⟮x⟯
-- 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
x : K
hsep : IsSeparable F x
inst_7 : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this_1 : Algebra.IsSeparable.{u, w} F ↥F⟮x⟯
this_2 : Algebra.IsSeparable.{v, w} E ↥E⟮x⟯
this : Algebra.IsAlgebraic.{u, w} F ↥F⟮x⟯
⊢ natDegree (Polynomial.map (algebraMap F E) (minpoly F x)) = natDegree (minpoly E x)
have rw : natDegree (minpoly F x) = natDegree (minpoly E x)
Tactic: rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]