awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
rw : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E) × Emb (↥(separableClosure F E)) E)
rw₁ :
  #(Emb F ↥(separableClosure F E)) =
    Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} #(Emb (↥(separableClosure F E)) E)
rw₂ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * Cardinal.lift.{v, v} 1
rw₃ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E)) * 1
rw₄ : #(Emb F ↥(separableClosure F E)) = Cardinal.lift.{v, v} #(Emb F ↥(separableClosure F E))
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb F E)
have rw₅ : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E))
Tactic: rw [← (embProdEmbOfIsAlgebraic F (separableClosure F E) E).cardinal_eq,
    mk_prod, mk_eq_one (Emb _ E), lift_one, mul_one, lift_id]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
h : IsPurelyInseparable (↥L) E
x : E
hx : Membership.mem (γ := IntermediateField F E) (separableClosure F E) x
⊢ x ∈ L
have obtain : ∀ (y : ↥L)
  (hx :
    Membership.mem (α := E) (γ := IntermediateField F E) (separableClosure F E)
      ((algebraMap (↥L) E : (a : ↥L) → E) y : E)),
  Membership.mem (α := E) L ((algebraMap (↥L) E : (a : ↥L) → E) y : E)
Tactic: obtain ⟨y, rfl⟩ := h.inseparable' _ <|
    IsSeparable.tower_top L (mem_separableClosure_iff.1 hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
L : IntermediateField F E
⊢ separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E
have refine : ∀ (h : separableClosure F E ≤ L), IsPurelyInseparable (↥L) E
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ separableClosure_le F E L⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
L : IntermediateField F E
h : separableClosure F E ≤ L
this_1 : Algebra ↥(separableClosure F E) ↥L := (inclusion h).toAlgebra
this : SMul ↥(separableClosure F E) ↥L :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring (separableClosure F E)) CommSemiring.toSemiring _
⊢ IsPurelyInseparable (↥L) E
have this₁ : IsScalarTower (↥(separableClosure F E)) (↥L) E
Tactic: haveI : IsScalarTower (separableClosure F E) L E := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : IsAlgClosed L
inst_5 : Nonempty (E →+* L)
h : Function.Injective (β := F →+* L) fun (f : E →+* L) ↦ f.comp (algebraMap F E)
⊢ IsPurelyInseparable F E
have rw : Subsingleton.{v + 1} (Emb F E) ∧ Nonempty.{v + 1} (Emb F E)
Tactic: rw [isPurelyInseparable_iff_finSepDegree_eq_one, finSepDegree, Nat.card_eq_one_iff_unique]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : IsAlgClosed L
inst_5 : Nonempty (E →+* L)
h : Function.Injective (β := F →+* L) fun (f : E →+* L) ↦ f.comp (algebraMap F E)
this : Algebra E L := RingHom.toAlgebra (Classical.arbitrary (E →+* L))
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
⊢ Eq (α := F →+* L) ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) (j.comp (↑f : E →+* AlgebraicClosure E)))
    ((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) (j.comp (↑g : E →+* AlgebraicClosure E)))
have a : ∀ (x : F),
  Eq.{w + 1} (α := L)
    (((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) (j.comp (↑f : E →+* AlgebraicClosure E)) : (a : F) → L)
        x :
      L)
    (((fun (f : E →+* L) ↦ (f.comp (algebraMap F E) : F →+* L)) (j.comp (↑g : E →+* AlgebraicClosure E)) : (a : F) → L)
        x :
      L)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosure F E
H : IsPurelyInseparable F E
⊢ IsSepClosed F
have this : IsAlgClosed E
Tactic: haveI := IsAlgClosure.isAlgClosed F (K := E)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosure F E
H : IsPurelyInseparable F E
this : IsAlgClosed E
⊢ IsSepClosed F
have rwa : ∀ (H : Eq (α := IntermediateField F E) (separableClosure F E) ⊥) (this : IsAlgClosed E), IsSepClosed F
Tactic: rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsAlgClosure F E
H : IsPurelyInseparable F E
this : IsAlgClosed E
rwa : ∀ (H : Eq (α := IntermediateField F E) (separableClosure F E) ⊥) (this : IsAlgClosed E), IsSepClosed F
⊢ IsSepClosed F
have rwa₁ : ∀ (H : IsSepClosed F) (this : IsAlgClosed E), IsSepClosed F
Tactic: rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
⊢ finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
have h : finSepDegree F E = finSepDegree.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
Tactic: have h := finSepDegree_mul_finSepDegree_of_isAlgebraic F (separableClosure F E) E |>.symm
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : finSepDegree F E = finSepDegree.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
⊢ finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
have rwa : ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E),
  finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
Tactic: rwa [finSepDegree_eq_finrank_of_isSeparable F (separableClosure F E),
    IsPurelyInseparable.finSepDegree_eq_one (separableClosure F E) E, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : finSepDegree F E = finSepDegree.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
rwa :
  ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E),
    finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
⊢ finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
have rwa₁ : ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E) * 1),
  finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
Tactic: rwa [finSepDegree_eq_finrank_of_isSeparable F (separableClosure F E),
    IsPurelyInseparable.finSepDegree_eq_one (separableClosure F E) E, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : finSepDegree F E = finSepDegree.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E
rwa :
  ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E) * finSepDegree (↥(separableClosure F E)) E),
    finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
rwa₁ :
  ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E) * 1),
    finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
⊢ finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
have rwa₂ : ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E)),
  finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E)
Tactic: rwa [finSepDegree_eq_finrank_of_isSeparable F (separableClosure F E),
    IsPurelyInseparable.finSepDegree_eq_one (separableClosure F E) E, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have pos : ∀ (halg : Algebra.IsAlgebraic F E), finSepDegree F E * finInsepDegree F E = finrank F E
Tactic: by_cases halg : Algebra.IsAlgebraic F E
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
pos : ∀ (halg : Algebra.IsAlgebraic F E), finSepDegree F E * finInsepDegree F E = finrank F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have neg : ∀ (halg : ¬Algebra.IsAlgebraic F E), finSepDegree F E * finInsepDegree F E = finrank F E
Tactic: by_cases halg : Algebra.IsAlgebraic F E
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have this : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E * insepDegree F E) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F E) : ℕ)
Tactic: have := congr_arg Cardinal.toNat (sepDegree_mul_insepDegree F E)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : Algebra.IsAlgebraic F E
this :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E * insepDegree F E) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F E) : ℕ)
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have pos : ∀
  (this :
    HMul.hMul (α := ℕ) (β := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E) : ℕ)
        ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (insepDegree F E) : ℕ) =
      (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F E)),
  finSepDegree F E * finInsepDegree F E = finrank F E
Tactic: rwa [Cardinal.toNat_mul, ← finSepDegree_eq F E] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : Algebra.IsAlgebraic F E
this :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E * insepDegree F E) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F E) : ℕ)
pos :
  ∀
    (this :
      HMul.hMul (α := ℕ) (β := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree F E) : ℕ)
          ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (insepDegree F E) : ℕ) =
        (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F E)),
    finSepDegree F E * finInsepDegree F E = finrank F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have pos₁ : ∀
  (this :
    HMul.hMul (β := ℕ) (finSepDegree F E) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (insepDegree F E) : ℕ) =
      (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Module.rank F E)),
  finSepDegree F E * finInsepDegree F E = finrank F E
Tactic: rwa [Cardinal.toNat_mul, ← finSepDegree_eq F E] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have neg : finSepDegree F E * finrank (↥(separableClosure F E)) E = finrank F E
Tactic: rw [finInsepDegree, finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦
      halg (Algebra.IsAlgebraic.of_finite F E),
    finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
      halg (.trans _ (separableClosure F E) _),
    mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
neg : finSepDegree F E * finrank (↥(separableClosure F E)) E = finrank F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have neg₁ : finSepDegree F E * finrank (↥(separableClosure F E)) E = 0
Tactic: rw [finInsepDegree, finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦
      halg (Algebra.IsAlgebraic.of_finite F E),
    finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
      halg (.trans _ (separableClosure F E) _),
    mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
neg : finSepDegree F E * finrank (↥(separableClosure F E)) E = finrank F E
neg₁ : finSepDegree F E * finrank (↥(separableClosure F E)) E = 0
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have neg₂ : finSepDegree F E * 0 = 0
Tactic: rw [finInsepDegree, finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦
      halg (Algebra.IsAlgebraic.of_finite F E),
    finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
      halg (.trans _ (separableClosure F E) _),
    mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : ¬Algebra.IsAlgebraic F E
neg : finSepDegree F E * finrank (↥(separableClosure F E)) E = finrank F E
neg₁ : finSepDegree F E * finrank (↥(separableClosure F E)) E = 0
neg₂ : finSepDegree F E * 0 = 0
⊢ finSepDegree F E * finInsepDegree F E = finrank F E
have neg₃ : Eq (α := ℕ) 0 0
Tactic: rw [finInsepDegree, finrank_of_infinite_dimensional (K := F) (V := E) fun _ ↦
      halg (Algebra.IsAlgebraic.of_finite F E),
    finrank_of_infinite_dimensional (K := separableClosure F E) (V := E) fun _ ↦
      halg (.trans _ (separableClosure F E) _),
    mul_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
⊢ x ∈ L
have this : Algebra.IsSeparable (↥L) K
Tactic: have := Algebra.isSeparable_tower_top_of_isSeparable E L K
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x_1 : Algebra ↥S ↥L := i.toAlgebra
x_2 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
⊢ x ∈ L
have this₁ : IsScalarTower (↥S) (↥L) K
Tactic: have : IsScalarTower S L K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x_1 : Algebra ↥S ↥L := i.toAlgebra
x_2 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this : IsScalarTower (↥S) (↥L) K
⊢ x ∈ L
have this₁ : Algebra.IsAlgebraic F K
Tactic: have := Algebra.IsAlgebraic.trans F E K
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x_1 : Algebra ↥S ↥L := i.toAlgebra
x_2 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this_2 : IsScalarTower (↥S) (↥L) K
this : Algebra.IsAlgebraic F K
⊢ x ∈ L
have this₁ : IsPurelyInseparable (↥S) K
Tactic: have : IsPurelyInseparable S K := separableClosure.isPurelyInseparable F K
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x_1 : Algebra ↥S ↥L := i.toAlgebra
x_2 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this_2 : IsScalarTower (↥S) (↥L) K
this_3 : Algebra.IsAlgebraic F K
this : IsPurelyInseparable (↥S) K
⊢ x ∈ L
have this₁ : IsPurelyInseparable (↥L) K
Tactic: have := IsPurelyInseparable.tower_top S L K
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x_1 : Algebra ↥S ↥L := i.toAlgebra
x_2 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this_2 : IsScalarTower (↥S) (↥L) K
this_3 : Algebra.IsAlgebraic F K
this_4 : IsPurelyInseparable (↥S) K
this : IsPurelyInseparable (↥L) K
⊢ x ∈ L
have obtain : ∀ (y : ↥L),
  Membership.mem (α := K) (γ := IntermediateField E K) ⊤ ((algebraMap (↥L) K : (a : ↥L) → K) y : K) →
    Membership.mem (α := K) L ((algebraMap (↥L) K : (a : ↥L) → K) y : K)
Tactic: obtain ⟨y, rfl⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable L K x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
S : IntermediateField E K := separableClosure E K
⊢ adjoin E (↑(separableClosure F K) : Set K) = S
have h : lift (adjoin E (↑(separableClosure F ↥S) : Set ↥S)) = lift (F := S) ⊤
Tactic: have h := congr_arg lift (adjoin_eq_of_isAlgebraic_of_isSeparable (F := F) S)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
S : IntermediateField E K := separableClosure E K
h : lift (adjoin E (↑(separableClosure F ↥S) : Set ↥S)) = lift (F := S) ⊤
⊢ adjoin E (↑(separableClosure F K) : Set K) = S
have h₁ : adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S
Tactic: rw [lift_top, lift_adjoin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S
⊢ adjoin E (↑(separableClosure F K) : Set K) = S
have this : IsScalarTower F (↥S) K
Tactic: haveI : IsScalarTower F S K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S
this : IsScalarTower F (↥S) K
⊢ adjoin E (↑(separableClosure F K) : Set K) = S
have rw : Eq (α := IntermediateField E K)
  (adjoin E
    (↑(IntermediateField.map (L := ↥(separableClosure E K)) (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K)
          (separableClosure F ↥(separableClosure E K))) :
      Set K))
  (adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)))
Tactic: rw [← h, ← map_eq_of_separableClosure_eq_bot F (separableClosure_eq_bot E K)]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
⊢ Membership.mem (γ := Set A)
    {x : A | ∃ (n : ℕ), Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)} (x * y)
have h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x * y) ^ p ^ (n + m))
Tactic: use n + m
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (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
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x * y) ^ p ^ (n + m))
have h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m * (y ^ p ^ m) ^ p ^ n)
Tactic: rw [mul_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]