awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k : Type u_3
K : Type u_4
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H
⊢ Subset (α := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
      ((fun (a : Gal(K/k)) ↦
          (mulEquivToLimit k K : (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) a) ''
        (↑L.fixingSubgroup : Set Gal(K/k)))
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H) ∧
    True ∧
      Membership.mem (γ := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((fun (a : Gal(K/k)) ↦
            (mulEquivToLimit k K : (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) a) ''
          (↑L.fixingSubgroup : Set Gal(K/k)))
        1

Tactic:
simpa [one_mem] using Set.image_subset_iff.mp (Set.image_mono le)

Premises used: Set.image_mono, Iff.mp, Set.image_subset_iff, OneMemClass.one_mem
-- Module: Mathlib.FieldTheory.Galois.Profinite
Goal:
k_1 : Type u_1
K_1 : Type u_2
inst : Field k_1
inst_1 : Field K_1
inst_2 : Algebra k_1 K_1
k : Type u_3
K : Type u_4
inst_3 : Field k
inst_4 : Field K
inst_5 : Algebra k K
inst_6 : IsGalois k K
⊢ CompactSpace.{u_4} Gal(K/k)

Tactic:
(continuousMulEquivToLimit k K).symm.compactSpace

Premises used: Homeomorph.compactSpace, ContinuousMulEquiv.symm, InfiniteGalois.continuousMulEquivToLimit, ContinuousMulEquiv.toHomeomorph
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ LE.le (α := Subalgebra F E) (Algebra.adjoin F S) (toSubalgebra (adjoin F S))

Tactic:
Algebra.adjoin_le (subset_adjoin _ _)

Premises used: IntermediateField.subset_adjoin, Algebra.adjoin_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : ↥(Algebra.adjoin F S)
⊢ (↑((algebraMap ↥(Algebra.adjoin F S) ↥(adjoin F S) : (a : ↥(Algebra.adjoin F S)) → ↥(adjoin F S)) x) : E) = (↑x : E)

Tactic:
rfl

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.range, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Eq (α := ↥F⟮x⟯)
    ((algebraMap ↥F[x] ↥F⟮x⟯ : (a : ↥F[x]) → ↥F⟮x⟯)
        (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Subalgebra F E) F[x] x_1) x ⋯) :
      ↥F⟮x⟯)
    (AdjoinSimple.gen F x : ↥F⟮x⟯)

Tactic:
rfl

Premises used: Set.Mem, IntermediateField.AdjoinSimple.gen, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
X : Type u_3
inst_3 : SMul X F
inst_4 : SMul X E
inst_5 : IsScalarTower X F E
⊢ IsScalarTower.{u_3, u_2, u_2} X ↥(Algebra.adjoin F S) ↥(adjoin F S)

Tactic:
Subalgebra.inclusion.isScalarTower_left (algebra_adjoin_le_adjoin F S) _

Premises used: Subalgebra.inclusion.isScalarTower_left, Set.Mem, IntermediateField.adjoin, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
X : Type u_3
inst_3 : MulAction E X
⊢ IsScalarTower.{u_2, u_2, u_3} (↥(Algebra.adjoin F S)) (↥(adjoin F S)) X

Tactic:
Subalgebra.inclusion.isScalarTower_right (algebra_adjoin_le_adjoin F S) _

Premises used: Set.Mem, Subalgebra.inclusion.isScalarTower_right, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ FaithfulSMul.{u_2, u_2} ↥(Algebra.adjoin F S) ↥(adjoin F S)

Tactic:
Subalgebra.inclusion.faithfulSMul (algebra_adjoin_le_adjoin F S)

Premises used: Set.Mem, Subalgebra.inclusion.faithfulSMul, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ IsFractionRing.{u_2, u_2} ↥(Algebra.adjoin F S) ↥(adjoin F S)

Tactic:
.of_field _ _ fun ⟨_, h⟩ ↦ have ⟨x, hx, y, hy, eq⟩ := mem_adjoin_iff_div.mp h
    ⟨⟨x, hx⟩, ⟨y, hy⟩, Subtype.ext eq⟩

Premises used: Subsemiring.mk', Algebra.algebraMap, Subsemiring.closure, Set.Mem, _private.0.IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin.match_1, _private.0.IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin.match_2, Algebra.adjoin, Membership.mem, Exists, IsFractionRing.of_field, Subtype, HDiv.hDiv, IntermediateField.mem_adjoin_iff_div, Subtype.mk, IntermediateField.adjoin, Exists.intro, Iff.mp, Eq, DFunLike.coe, Subtype.ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
⊢ Algebra.IsAlgebraic.{u_2, u_2} ↥(Algebra.adjoin F S) ↥(adjoin F S)

Tactic:
IsLocalization.isAlgebraic _ (nonZeroDivisors (Algebra.adjoin F S))

Premises used: Algebra.adjoin, Membership.mem, nonZeroDivisors, Subtype, IsLocalization.isAlgebraic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
inv_mem :
  ∀ (x : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x →
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x⁻¹
⊢ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) (Algebra.adjoin F S)

Tactic:
le_antisymm
    (show adjoin F S ≤
        { Algebra.adjoin F S with
          inv_mem' := inv_mem }
      from adjoin_le_iff.mpr Algebra.subset_adjoin)
    (algebra_adjoin_le_adjoin _ _)

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, Algebra.subset_adjoin, le_antisymm, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
a : K.toSubalgebra = toSubalgebra (adjoin F S)
⊢ K = adjoin F S

Tactic:
apply toSubalgebra_injective

Premises used: IntermediateField.toSubalgebra_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
a : Eq (α := Subalgebra F E) (Algebra.adjoin F S) (toSubalgebra (adjoin F S))
⊢ K.toSubalgebra = toSubalgebra (adjoin F S)

Tactic:
rw [h]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
⊢ Eq (α := Subalgebra F E) (Algebra.adjoin F S) (toSubalgebra (adjoin F S))

Tactic:
(adjoin_eq_algebra_adjoin F _ fun x ↦ ?_).symm

Premises used: IntermediateField.adjoin_eq_algebra_adjoin, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
a :
  ∀ (x : E),
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x →
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x⁻¹
⊢ Eq (α := Subalgebra F E) (Algebra.adjoin F S) (toSubalgebra (adjoin F S))

Tactic:
refine (adjoin_eq_algebra_adjoin F _ fun x ↦ ?_).symm

Premises used: IntermediateField.adjoin_eq_algebra_adjoin, Eq.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
a : x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra
⊢ Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x →
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x⁻¹

Tactic:
rw [← h]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra

Tactic:
K.inv_mem

Premises used: Set.Mem, IntermediateField.inv_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : IntermediateField F E
h : K.toSubalgebra = Algebra.adjoin F S
x : E
⊢ x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra

Tactic:
exact K.inv_mem

Premises used: IntermediateField.inv_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
hS : Eq (α := Subalgebra F E) (Algebra.adjoin F S) ⊤
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊤

Tactic:
top_le_iff.mp (hS.symm.trans_le <| algebra_adjoin_le_adjoin F S)

Premises used: Eq.trans_le, top_le_iff, Iff.mp, Eq.symm, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
mp : FG.{u_1, u_2} (F := F) (E := E) ⊤ → Algebra.EssFiniteType F E
mpr : Algebra.EssFiniteType F E → FG.{u_1, u_2} (F := F) (E := E) ⊤
⊢ FG.{u_1, u_2} (F := F) (E := E) ⊤ ↔ Algebra.EssFiniteType F E

Tactic:
constructor
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ Algebra.FiniteType.{u_1, u_2} F ↥(Algebra.adjoin F (↑s : Set E))

Tactic:
have : Algebra.FiniteType F (Algebra.adjoin F (s : Set E)) := .adjoin_of_finite s.finite_toSet
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : Algebra.FiniteType.{u_1, u_2} F ↥(Algebra.adjoin F (↑s : Set E))
⊢ Algebra.EssFiniteType.{u_2, u_2} ↥(Algebra.adjoin F (↑s : Set E)) ↥(adjoin F (↑s : Set E))

Tactic:
have : Algebra.EssFiniteType (Algebra.adjoin F (s : Set E)) (adjoin F (s : Set E)) :=
      .of_isLocalization _ (nonZeroDivisors _)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this_1 : Algebra.FiniteType.{u_1, u_2} F ↥(Algebra.adjoin F (↑s : Set E))
this : Algebra.EssFiniteType.{u_2, u_2} ↥(Algebra.adjoin F (↑s : Set E)) ↥(adjoin F (↑s : Set E))
⊢ Algebra.EssFiniteType.{u_1, u_2} F ↥(adjoin F (↑s : Set E))

Tactic:
have : Algebra.EssFiniteType F (adjoin F (s : Set E)) :=
      .comp _ (Algebra.adjoin F (s : Set E)) _
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this_1 : Algebra.FiniteType.{u_1, u_2} F ↥(Algebra.adjoin F (↑s : Set E))
this_2 : Algebra.EssFiniteType.{u_2, u_2} ↥(Algebra.adjoin F (↑s : Set E)) ↥(adjoin F (↑s : Set E))
this : Algebra.EssFiniteType.{u_1, u_2} F ↥(adjoin F (↑s : Set E))
⊢ Algebra.EssFiniteType.{u_1, u_2} F ↥⊤

Tactic:
rw [hs] at this
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this_1 : Algebra.FiniteType.{u_1, u_2} F ↥(Algebra.adjoin F (↑s : Set E))
this_2 : Algebra.EssFiniteType.{u_2, u_2} ↥(Algebra.adjoin F (↑s : Set E)) ↥(adjoin F (↑s : Set E))
this : Algebra.EssFiniteType.{u_1, u_2} F ↥⊤
⊢ Algebra.EssFiniteType F E

Tactic:
.of_surjective IntermediateField.topEquiv.toAlgHom IntermediateField.topEquiv.surjective

Premises used: AlgEquiv.toAlgHom, AlgEquiv.surjective, IntermediateField.topEquiv, Algebra.EssFiniteType.of_surjective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this_1 : Algebra.FiniteType.{u_1, u_2} F ↥(Algebra.adjoin F (↑s : Set E))
this_2 : Algebra.EssFiniteType.{u_2, u_2} ↥(Algebra.adjoin F (↑s : Set E)) ↥(adjoin F (↑s : Set E))
this : Algebra.EssFiniteType.{u_1, u_2} F ↥⊤
⊢ Algebra.EssFiniteType F E

Tactic:
exact .of_surjective IntermediateField.topEquiv.toAlgHom IntermediateField.topEquiv.surjective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h_1 : Algebra.EssFiniteType F E
h : Eq (α := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) ⊤
⊢ FG.{u_1, u_2} (F := F) (E := E) ⊤

Tactic:
use Algebra.EssFiniteType.finset F E

Premises used: Algebra.EssFiniteType.finset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Algebra.EssFiniteType F E
⊢ Eq (α := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) ⊤

Tactic:
top_le_iff.mp fun x _ ↦ ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h_1 : Algebra.EssFiniteType F E
h :
  ∀ (x : E),
    Membership.mem (γ := IntermediateField F E) ⊤ x →
      Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) x
⊢ Eq (α := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) ⊤

Tactic:
refine top_le_iff.mp fun x _ ↦ ?_

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h_1 : Algebra.EssFiniteType F E
x : E
h_2 : Membership.mem (γ := IntermediateField F E) ⊤ x
h :
  ∀ (x : ↥(Algebra.EssFiniteType.subalgebra F E)) (s : ↥(Algebra.EssFiniteType.submonoid F E)),
    Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s) →
      Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
        (IsLocalization.mk' E x s)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (Algebra.EssFiniteType.submonoid F E) x

Premises used: Algebra.EssFiniteType.submonoid, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
h_1 : Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s)
⊢ (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0

Tactic:
have hs : s.1.1 ≠ 0 := (IsLocalization.map_units E s).ne_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
h_1 : Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s)
hs : (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0
⊢ IsLocalization.mk' E x s = (↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E)

Tactic:
simp [IsLocalization.mk'_eq_iff_eq_mul, hs]

Premises used: IsLocalization.mk'_eq_iff_eq_mul
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
h_1 : Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s)
hs : (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0
⊢ IsLocalization.mk' E x s = (↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E)

Tactic:
have H : IsLocalization.mk' E x s = x / s := by
      simp [IsLocalization.mk'_eq_iff_eq_mul, hs]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h_1 : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
h_2 : Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s)
hs : (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0
H : IsLocalization.mk' E x s = (↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E)
h :
  Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
    ((↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E))
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
    (IsLocalization.mk' E x s)

Tactic:
rw [H]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
h_1 : Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s)
hs : (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0
H : IsLocalization.mk' E x s = (↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
    ((↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E))

Tactic:
div_mem (IntermediateField.algebra_adjoin_le_adjoin _ _ x.2)
      (IntermediateField.algebra_adjoin_le_adjoin _ _ s.1.2)

Premises used: div_mem, Subtype.val, Subtype.property, IntermediateField.algebra_adjoin_le_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
h : Algebra.EssFiniteType F E
x : ↥(Algebra.EssFiniteType.subalgebra F E)
s : ↥(Algebra.EssFiniteType.submonoid F E)
h_1 : Membership.mem (γ := IntermediateField F E) ⊤ (IsLocalization.mk' E x s)
hs : (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0
H : IsLocalization.mk' E x s = (↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
    ((↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E))

Tactic:
exact div_mem (IntermediateField.algebra_adjoin_le_adjoin _ _ x.2)
      (IntermediateField.algebra_adjoin_le_adjoin _ _ s.1.2)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 rwa rwa₁ rwa₂ rwa₃ : Algebra.EssFiniteType F E
⊢ FG.{u_1, u_2} (F := F) (E := E) ⊤

Tactic:
rwa [fg_top_iff]

Premises used: IntermediateField.fg_top_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
this :
  (∃ (s : Finset E), (↑s : Set E) ⊆ (↑K : Set E) ∧ adjoin F (↑s : Set E) = K) ↔
    ∃ (t : Finset E), adjoin F (↑t : Set E) = K
⊢ Algebra.EssFiniteType.{u_1, u_2} F ↥K ↔ K.FG

Tactic:
simpa [IntermediateField.FG, (Equiv.finsetSubtypeComm _).exists_congr_left,
      ← (IntermediateField.map_injective K.val).eq_iff, ← IntermediateField.fg_top_iff,
      adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using this

Premises used: Set.range_comp, AlgHom.fieldRange_eq_map, Equiv.exists_congr_left, IntermediateField.FG, Function.Injective.eq_iff, IntermediateField.adjoin_map, IntermediateField.map_injective, Function.comp_def, Equiv.finsetSubtypeComm, IntermediateField.val, IntermediateField.fg_top_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
suffices :
  (∃ (s : Finset E), (↑s : Set E) ⊆ (↑K : Set E) ∧ adjoin F (↑s : Set E) = K) ↔
    ∃ (t : Finset E), adjoin F (↑t : Set E) = K
⊢ Algebra.EssFiniteType.{u_1, u_2} F ↥K ↔ K.FG

Tactic:
suffices (∃ s : Finset E, (s : Set E) ⊆ K ∧ adjoin F ↑s = K) ↔
      ∃ t : Finset E, adjoin F ↑t = K by
    simpa [IntermediateField.FG, (Equiv.finsetSubtypeComm _).exists_congr_left,
      ← (IntermediateField.map_injective K.val).eq_iff, ← IntermediateField.fg_top_iff,
      adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using this
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ (∃ (s : Finset E), (↑s : Set E) ⊆ (↑K : Set E) ∧ adjoin F (↑s : Set E) = K) ↔
    ∃ (t : Finset E), adjoin F (↑t : Set E) = K

Tactic:
⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩

Premises used: _private.0.IntermediateField.essFiniteType_iff.match_4, Exists, Eq.rec, _private.0.IntermediateField.essFiniteType_iff.match_5, HasSubset.Subset, IntermediateField.subset_adjoin, And, SetLike.coe, And.intro, IntermediateField.adjoin, Iff.intro, Exists.intro, Eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ (∃ (s : Finset E), (↑s : Set E) ⊆ (↑K : Set E) ∧ adjoin F (↑s : Set E) = K) ↔
    ∃ (t : Finset E), adjoin F (↑t : Set E) = K

Tactic:
exact ⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
rw : IsIntegral F (A := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) : E)
| IsIntegral F α

Tactic:
rw [← AdjoinSimple.algebraMap_gen F α]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
conv_rhs :
  IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F (A := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) : E)
⊢ IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F α

Tactic:
conv_rhs => rw [← AdjoinSimple.algebraMap_gen F α]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
rw rw₁ : IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F (A := ↥F⟮α⟯) (gen F α)
⊢ IsIntegral F (A := ↥F⟮α⟯) (gen F α) ↔ IsIntegral F (A := E) ((algebraMap (↥F⟮α⟯) E : (a : ↥F⟮α⟯) → E) (gen F α) : E)

Tactic:
rw [isIntegral_algebraMap_iff (algebraMap F⟮α⟯ E).injective]

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, isIntegral_algebraMap_iff, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
hS : ∀ x ∈ S, IsAlgebraic F x
⊢ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) (Algebra.adjoin F S)

Tactic:
adjoin_eq_algebra_adjoin _ _ fun _ ↦
    (Algebra.IsIntegral.adjoin fun x hx ↦ (hS x hx).isIntegral).inv_mem

Premises used: IntermediateField.adjoin_eq_algebra_adjoin, Algebra.IsIntegral.inv_mem