awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
⊢ Algebra.IsSeparable.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)

Tactic:
haveI : Algebra.IsSeparable F (restrictScalars F L⟮x⟯) := Algebra.IsSeparable.trans F L L⟮x⟯
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this_1 : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
⊢ Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) x

Tactic:
have hx : x ∈ L⟮x⟯.restrictScalars F := mem_adjoin_simple_self _ x
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this_1 : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
hx : Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) x
⊢ Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x

Tactic:
⟨⟨x, mem_separableClosure_iff.2 <| isSeparable_of_mem_isSeparable F E hx⟩, rfl⟩

Premises used: IntermediateField.isSeparable_of_mem_isSeparable, Iff.mpr, Set.Mem, setOf, Subtype.mk, Exists.intro, mem_separableClosure_iff, Set.range, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this_1 : Algebra.IsSeparable.{v, v} ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable.{u, v} F ↥(IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯)
hx : Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (↥L)⟮x⟯) x
⊢ Membership.mem (γ := Subring E) (RingHom.range (R := ↥L) (algebraMap (↥L) E)) x

Tactic:
exact ⟨⟨x, mem_separableClosure_iff.2 <| isSeparable_of_mem_isSeparable F E hx⟩, rfl⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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))
rw₅ rw₆ : #(Emb F ↥(separableClosure F E)) = #(Emb F ↥(separableClosure F E))
⊢ #(Emb F ↥(separableClosure F E)) = #(Emb 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]

Premises used: Field.embProdEmbOfIsAlgebraic, Membership.mem, Subtype, Cardinal.lift_one, Cardinal.mk_eq_one, mul_one, separableClosure, Field.Emb, Cardinal.lift_id, Equiv.cardinal_eq, Cardinal.mk_prod
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
q : ℕ
inst_3 : ExpChar F q
inst_4 : FiniteDimensional F E
⊢ ∃ (n : ℕ), finInsepDegree F E = q ^ n

Tactic:
IsPurelyInseparable.finrank_eq_pow ..

Premises used: Field.finInsepDegree, IsPurelyInseparable.finrank_eq_pow, Set.Mem, separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
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)
⊢ x ∈ L

Tactic:
obtain ⟨y, rfl⟩ := h.inseparable' _ <|
    IsSeparable.tower_top L (mem_separableClosure_iff.1 hx)

Premises used: IsPurelyInseparable.inseparable', Membership.mem, Subtype, IsSeparable.tower_top, Iff.mp, mem_separableClosure_iff, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
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:
y.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
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:
exact y.2

Premises used: Subtype.property
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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

Tactic:
⟨fun h ↦ ?_, fun _ ↦ separableClosure_le F E L⟩

Premises used: separableClosure_le, Iff.intro
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
refine : ∀ (h : separableClosure F E ≤ L), IsPurelyInseparable (↥L) E
⊢ separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ separableClosure_le F E L⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 _
⊢ IsScalarTower (↥(separableClosure F E)) (↥L) E

Tactic:
haveI : IsScalarTower (separableClosure F E) L E := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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_2 : SMul ↥(separableClosure F E) ↥L :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring (separableClosure F E)) CommSemiring.toSemiring _
this : IsScalarTower (↥(separableClosure F E)) (↥L) E
⊢ IsPurelyInseparable (↥L) E

Tactic:
IsPurelyInseparable.tower_top (separableClosure F E) L E

Premises used: Membership.mem, Subtype, separableClosure, IsPurelyInseparable.tower_top
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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_2 : SMul ↥(separableClosure F E) ↥L :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring (separableClosure F E)) CommSemiring.toSemiring _
this : IsScalarTower (↥(separableClosure F E)) (↥L) E
⊢ IsPurelyInseparable (↥L) E

Tactic:
exact IsPurelyInseparable.tower_top (separableClosure F E) L E

Premises used: Membership.mem, Subtype, separableClosure, IsPurelyInseparable.tower_top
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : Algebra.IsSeparable.{u, v} F ↥L
inst_4 : IsPurelyInseparable (↥L) E
⊢ L = separableClosure F E

Tactic:
le_antisymm (le_separableClosure F E L) (separableClosure_le F E L)

Premises used: separableClosure_le, le_antisymm, le_separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ Algebra.IsSeparable.{u, v} F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(separableClosure F E)) E

Tactic:
⟨isSeparable F E, isPurelyInseparable F E⟩

Premises used: And.intro, separableClosure.isSeparable, separableClosure.isPurelyInseparable
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ Algebra.IsSeparable.{u, v} F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(separableClosure F E)) E

Tactic:
exact ⟨isSeparable F E, isPurelyInseparable F E⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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)
rw : Subsingleton.{v + 1} (Emb F E) ∧ Nonempty.{v + 1} (Emb F E)
⊢ IsPurelyInseparable F E

Tactic:
rw [isPurelyInseparable_iff_finSepDegree_eq_one, finSepDegree, Nat.card_eq_one_iff_unique]

Premises used: Field.finSepDegree, Nat.card_eq_one_iff_unique, isPurelyInseparable_iff_finSepDegree_eq_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
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)
⊢ 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)))

Tactic:
ext
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
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:
simp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ Subsingleton.{v + 1} (Emb F E) ∧ Nonempty.{v + 1} (Emb F E)

Tactic:
exact ⟨⟨fun f g ↦ DFunLike.ext' <| j.injective.comp_left (congr_arg (⇑) <|
    @h (j.toRingHom.comp f) (j.toRingHom.comp g) (by ext; simp))⟩, inferInstance⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ IsPurelyInseparable.{u, v} F ↥⊥

Tactic:
(botEquiv F E).symm.isPurelyInseparable

Premises used: AlgEquiv.symm, AlgEquiv.isPurelyInseparable, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ IsAlgClosed E

Tactic:
haveI := IsAlgClosure.isAlgClosed F (K := E)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (H : IsSepClosed F) (this : IsAlgClosed E), IsSepClosed F
⊢ IsSepClosed F

Tactic:
rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H

Premises used: IsSepClosed.separableClosure_eq_bot_iff, separableClosure.eq_bot_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
inst_4 : IsSepClosed F
⊢ IsSepClosed E

Tactic:
have : Algebra.IsAlgebraic F (AlgebraicClosure E) := .trans F E _
  (isSepClosed_iff_isPurelyInseparable_algebraicClosure E _).mpr
    (IsPurelyInseparable.tower_top F E <| AlgebraicClosure E)

Premises used: Iff.mpr, Algebra.IsAlgebraic.trans, isSepClosed_iff_isPurelyInseparable_algebraicClosure, AlgebraicClosure, IsPurelyInseparable.tower_top
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 = 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
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (h : finSepDegree F E = finrank.{u, v} F ↥(separableClosure F E)),
    finSepDegree F E = (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (sepDegree 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

Premises used: Membership.mem, Subtype, Field.finSepDegree_eq_finrank_of_isSeparable, mul_one, IsPurelyInseparable.finSepDegree_eq_one, separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
neg : ∀ (halg : ¬Algebra.IsAlgebraic F E), finSepDegree F E * finInsepDegree F E = finrank F E
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
by_cases halg : Algebra.IsAlgebraic F E

Premises used: Algebra.IsAlgebraic
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
halg : Algebra.IsAlgebraic F E
⊢ 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)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
pos₁ pos₂ pos₃ 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
⊢ finSepDegree F E * finInsepDegree F E = finrank F E

Tactic:
rwa [Cardinal.toNat_mul, ← finSepDegree_eq F E] at this

Premises used: Cardinal.toNat_mul, Field.finSepDegree_eq
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
neg₃ neg₄ : Eq (α := ℕ) 0 0
⊢ finSepDegree F E * finInsepDegree F 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]

Premises used: Field.finInsepDegree, Algebra.IsAlgebraic.of_finite, Membership.mem, Algebra.IsAlgebraic.trans, Subtype, MulZeroClass.mul_zero, Module.finrank_of_infinite_dimensional, separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
set :
  let S : IntermediateField F K := separableClosure F K;
  Membership.mem (γ := IntermediateField E K) (adjoin E (↑S : Set K)) x
⊢ Membership.mem (γ := IntermediateField E K) (adjoin E (↑(separableClosure F K) : Set K)) x

Tactic:
set S := separableClosure F K

Premises used: separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
set :
  let L : IntermediateField E K := adjoin E (↑S : Set K);
  x ∈ L
⊢ Membership.mem (γ := IntermediateField E K) (adjoin E (↑S : Set K)) x

Tactic:
set L := adjoin E (S : Set K)

Premises used: SetLike.coe, IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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)
⊢ Algebra.IsSeparable (↥L) K

Tactic:
have := Algebra.isSeparable_tower_top_of_isSeparable E L K
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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 _
⊢ IsScalarTower (↥S) (↥L) K

Tactic:
have : IsScalarTower S L K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ Algebra.IsAlgebraic F K

Tactic:
have := Algebra.IsAlgebraic.trans F E K
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ IsPurelyInseparable (↥S) K

Tactic:
have : IsPurelyInseparable S K := separableClosure.isPurelyInseparable F K
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
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
⊢ IsPurelyInseparable (↥L) K

Tactic:
have := IsPurelyInseparable.tower_top S L K