awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
have 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)
Tactic: have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : IsPurelyInseparable F E
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)
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
have 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)
Tactic: rwa [separableClosure.adjoin_eq_of_isAlgebraic] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
have 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)
Tactic: have h := lift_rank_mul_lift_sepDegree_of_isSeparable F (separableClosure F E) K
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.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)
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
have 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)
Tactic: rwa [sepDegree_eq_of_isPurelyInseparable (separableClosure F E) E K] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
have 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)
Tactic: have h := lift_rank_mul_lift_insepDegree_of_isPurelyInseparable (separableClosure F E) E K
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.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)
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
have 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)
Tactic: rwa [← insepDegree_eq_of_isSeparable F (separableClosure F E) K] 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 : Algebra.IsAlgebraic.{u, w} F ↥(adjoin F S)
inst_8 : IsPurelyInseparable F E
⊢ sepDegree E ↥(adjoin E S) = sepDegree F ↥(adjoin F S)
have set : let M : IntermediateField F K := adjoin F S;
Algebra.IsAlgebraic.{u, w} F ↥M → sepDegree E ↥(adjoin E S) = sepDegree F ↥M
Tactic: set M := adjoin F S
Cleared hypotheses: inst_7
-- 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)
⊢ M ≤ restrictScalars F L
have rw : M ≤ adjoin F ((↑E' : Set K) ∪ S)
Tactic: rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]
-- 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)
⊢ sepDegree E ↥L = sepDegree F ↥M
have hi : 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
-- 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 : SMul ↥M ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring M) DivisionSemiring.toSemiring _
⊢ sepDegree E ↥L = sepDegree F ↥M
have this₁ : IsScalarTower.{u, w, w} F ↥M ↥L
Tactic: haveI : IsScalarTower F M L := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Tower (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
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
have change : IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)
Tactic: change IsPurelyInseparable M (extendScalars 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
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 ↥(extendScalars hi)
have obtain : ∀ (q : ℕ), ExpChar F q → IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)
Tactic: obtain ⟨q, _⟩ := ExpChar.exists F
-- 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 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
| restrictScalars F (extendScalars hi)
have rw : restrictScalars F (L' := ↥(adjoin F S)) (adjoin ↥(adjoin F S) (↑E' : Set K))
Tactic: rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]
-- 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 : IsScalarTower.{u, w, w} F ↥M ↥L
q : ℕ
h : ExpChar F q
⊢ Eq (α := IntermediateField F K) (restrictScalars F (extendScalars hi))
    (restrictScalars F (L' := ↥M) (adjoin ↥M (↑E' : Set K)))
have conv_lhs : 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]
-- 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 : 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)))
⊢ Eq (α := IntermediateField F K) (restrictScalars F (extendScalars hi))
    (restrictScalars F (L' := ↥M) (adjoin ↥M (↑E' : Set K)))
have 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)))
Tactic: conv_lhs => rw [extendScalars_restrictScalars, restrictScalars_adjoin_of_algEquiv
        (E := K) j rfl, ← adjoin_self F E', adjoin_adjoin_comm]
-- 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
q : ℕ
h : ExpChar F q
⊢ IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)
have this₁ : 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]
-- 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)
⊢ IsPurelyInseparable.{w, w} ↥M ↥(extendScalars hi)
have rw : ∀ x ∈ (↑E' : Set K),
  ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)
Tactic: rw [this, isPurelyInseparable_adjoin_iff_pow_mem _ _ q]
-- 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 : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)
have 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)
Tactic: obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y
-- 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
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring K) (RingHom.range (R := ↥M) (algebraMap (↥M) K)) (x ^ q ^ n)
have refine : (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
Tactic: refine ⟨n, algebraMap F M z, ?_⟩
-- 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
⊢ (algebraMap (↥M) K : (a : ↥M) → K) ((algebraMap F ↥M : (a : F) → ↥M) z : ↥M) = x ^ q ^ n
have rw : (algebraMap F K : (a : F) → K) z = 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]
-- 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
⊢ (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) ((algebraMap F E : (a : F) → E) z : E) = 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]
-- 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
⊢ (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) = 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]