awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (hypothesis)
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
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
⊢ Eq.{u_4 + 1} (α := K)
    (↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K)
    (↑(((↑g :
                (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                  (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
              L :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K)
have this : Eq (α := K)
  ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K) :
    K)
  ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
Tactic: have : ((limitToAlgEquiv g).restrictNormal L.unop) x = (limitToAlgEquiv g) x.1 := by
      exact AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
g :
  (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
        fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
    Type u_4)
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
x : ↥(unop L).toIntermediateField
this :
  Eq (α := K)
    ((↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
              (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
            x) :
        K) :
      K)
    ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
⊢ Eq.{u_4 + 1} (α := K)
    (↑(((limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K)
    (↑(((↑g :
                (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                  (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
              L :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K)
have a : Eq (α := K) ((limitToAlgEquiv g : (a : K) → K) (↑x : K) : K)
  ((↑(((↑g :
                (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
                  (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
              L :
            (a : ↥(unop L).toIntermediateField) → ↥(unop L).toIntermediateField)
          x) :
      K) :
    K)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
A : Set Gal(K/k)
⊢ Membership.mem (γ := Filter Gal(K/k)) (𝓝 1) A ↔
    ∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A
have rw : (∃ (E : IntermediateField k K),
    FiniteDimensional.{u_3, u_4} k ↥E ∧ Normal.{u_3, u_4} k ↥E ∧ (↑E.fixingSubgroup : Set Gal(K/k)) ⊆ A) ↔
  ∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A
Tactic: rw [krullTopology_mem_nhds_one_iff_of_normal]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
    (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
          TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4)) :=
  {f :
    (L : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) L).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4) |
    Eq.{u_4 + 1} (α :=
      (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) (op L)).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
            TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
        Type u_4))
      (f (op L)) 1}
⊢ IsOpen (X :=
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    ((⇑(mulEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
      (↑L.fixingSubgroup : Set Gal(K/k)))
have suffices : Eq (α :=
  Set
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
  ((⇑(mulEquivToLimit k K) :
      (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
    (↑L.fixingSubgroup : Set Gal(K/k)))
  (Subtype.val (p :=
      fun
        (x :
          (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                  TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
              Type u_4)) ↦
      Membership.mem (γ :=
        Subgroup
          ((j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((Functor.obj (asProfiniteGaloisGroupFunctor k K) j).toProfinite.toTop (P := fun (X : TopCat.{u_4}) ↦
                  TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
              Type u_4)))
        (limitConePtAux (asProfiniteGaloisGroupFunctor k K)) x) ⁻¹'
    fix1)
Tactic: suffices mulEquivToLimit k K '' L.1.fixingSubgroup = Set.preimage Subtype.val fix1 by
    rw [this]
    exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
⊢ Continuous (X :=
    (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop (P :=
          fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
      Type u_4))
    (Y := Gal(K/k))
    (⇑(MulEquiv.symm (mulEquivToLimit k K)) :
      (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k))
have apply : ∀ (A : Set Gal(K/k)),
  Membership.mem (γ := Filter Gal(K/k))
      (nhds
          ((MulEquiv.symm (mulEquivToLimit k K) :
              (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k))
            1) :
        Filter Gal(K/k))
      A →
    Membership.mem (γ :=
      Filter
        (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
              (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
          Type u_4))
      (nhds 1)
      ((⇑(MulEquiv.symm (mulEquivToLimit k K)) :
          (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k)) ⁻¹'
        A)
Tactic: apply continuous_of_continuousAt_one _ (continuousAt_def.mpr _)
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
⊢ ∀ (A : Set Gal(K/k)),
    Membership.mem (γ := Filter Gal(K/k))
        (nhds
            ((MulEquiv.symm (mulEquivToLimit k K) :
                (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k))
              1) :
          Filter Gal(K/k))
        A →
      Membership.mem (γ :=
        Filter
          (↑((limit (J := (FiniteGaloisIntermediateField k K)ᵒᵖ) (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
                (P := fun (X : TopCat.{u_4}) ↦ TotallyDisconnectedSpace.{u_4} (↑X : Type u_4))) :
            Type u_4))
        (nhds 1)
        ((⇑(MulEquiv.symm (mulEquivToLimit k K)) :
            (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) → Gal(K/k)) ⁻¹'
          A)
have simp : ∀ (A : Set Gal(K/k)),
  (∃ (L : FiniteGaloisIntermediateField k K), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ A) →
    Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        A)
Tactic: simp only [map_one, krullTopology_mem_nhds_one_iff_of_isGalois, ← MulEquiv.coe_toEquiv_symm,
    ← MulEquiv.toEquiv_eq_coe, ← (mulEquivToLimit k K).image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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), (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H) →
    Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
      ((fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H)
have this : ∀ (L : FiniteGaloisIntermediateField k K) (le : (↑L.fixingSubgroup : Set Gal(K/k)) ⊆ H),
  Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
    ((fun (a : Gal(K/k)) ↦
        (MulEquiv.toEquiv (mulEquivToLimit k K) :
            (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
          a) ''
      H)
Tactic: ⟨L, le⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
⊢ Membership.mem (γ := Filter ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K))) (nhds 1)
    ((fun (a : Gal(K/k)) ↦
        (MulEquiv.toEquiv (mulEquivToLimit k K) :
            (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
          a) ''
      H)
have rw : ∃
  t ⊆
    (fun (a : Gal(K/k)) ↦
        (MulEquiv.toEquiv (mulEquivToLimit k K) :
            (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
          a) ''
      H,
  IsOpen t ∧ 1 ∈ t
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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
⊢ ∃
    t ⊆
      (fun (a : Gal(K/k)) ↦
          (MulEquiv.toEquiv (mulEquivToLimit k K) :
              (a : Gal(K/k)) → ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
            a) ''
        H,
    IsOpen t ∧ 1 ∈ t
have h : Subset (α := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
    ((⇑(mulEquivToLimit k K) :
        (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
      (↑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) ∧
  IsOpen (X := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
      ((⇑(mulEquivToLimit k K) :
          (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
        (↑L.fixingSubgroup : Set Gal(K/k))) ∧
    Membership.mem (γ := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
      ((⇑(mulEquivToLimit k K) :
          (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
        (↑L.fixingSubgroup : Set Gal(K/k)))
      1
Tactic: use mulEquivToLimit k K '' L.1.fixingSubgroup
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Profinite (goal)
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)))
      ((⇑(mulEquivToLimit k K) :
          (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
        (↑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) ∧
    IsOpen (X := ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((⇑(mulEquivToLimit k K) :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
          (↑L.fixingSubgroup : Set Gal(K/k))) ∧
      Membership.mem (γ := Set ↥(limitConePtAux (asProfiniteGaloisGroupFunctor k K)))
        ((⇑(mulEquivToLimit k K) :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) ''
          (↑L.fixingSubgroup : Set Gal(K/k)))
        1
have 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: simp only [isOpen_mulEquivToLimit_image_fixingSubgroup L]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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
⊢ K = adjoin F S
have a : K.toSubalgebra = toSubalgebra (adjoin F S)
Tactic: apply toSubalgebra_injective
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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
⊢ K.toSubalgebra = toSubalgebra (adjoin F S)
have a : Eq (α := Subalgebra F E) (Algebra.adjoin F S) (toSubalgebra (adjoin F S))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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))
have a : ∀ (x : E),
  Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x →
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x⁻¹
Tactic: refine (adjoin_eq_algebra_adjoin F _ fun x ↦ ?_).symm
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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
⊢ Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x →
    Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F S) x⁻¹
have a : x ∈ K.toSubalgebra → x⁻¹ ∈ K.toSubalgebra
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
⊢ FG.{u_1, u_2} (F := F) (E := E) ⊤ ↔ Algebra.EssFiniteType F E
have mp : FG.{u_1, u_2} (F := F) (E := E) ⊤ → Algebra.EssFiniteType F E
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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
⊢ FG.{u_1, u_2} (F := F) (E := E) ⊤ ↔ Algebra.EssFiniteType F E
have mpr : Algebra.EssFiniteType F E → FG.{u_1, u_2} (F := F) (E := E) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
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.EssFiniteType F E
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
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 F E
have this₁ : 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 _)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
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 F E
have this₁ : 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)) _
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
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 F E
have this₁ : Algebra.EssFiniteType.{u_1, u_2} F ↥⊤
Tactic: rw [hs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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
⊢ FG.{u_1, u_2} (F := F) (E := E) ⊤
have h : Eq (α := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) ⊤
Tactic: use Algebra.EssFiniteType.finset F E
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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)) ⊤
have h : ∀ (x : E),
  Membership.mem (γ := IntermediateField F E) ⊤ x →
    Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) x
Tactic: refine top_le_iff.mp fun x _ ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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 : E
h_1 : Membership.mem (γ := IntermediateField F E) ⊤ x
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E)) x
have 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)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (Algebra.EssFiniteType.submonoid F E) x
Cleared hypotheses: x, h_1
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
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)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
    (IsLocalization.mk' E x s)
have hs : (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E) ≠ 0
Tactic: have hs : s.1.1 ≠ 0 := (IsLocalization.map_units E s).ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (hypothesis)
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
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
    (IsLocalization.mk' E x s)
have H : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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))
    (IsLocalization.mk' E x s)
have h : Membership.mem (γ := IntermediateField F E) (adjoin F (↑(Algebra.EssFiniteType.finset F E) : Set E))
  ((↑x : E) / (↑(↑s : ↥(Algebra.EssFiniteType.subalgebra F E)) : E))
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra (goal)
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
⊢ Algebra.EssFiniteType.{u_1, u_2} F ↥K ↔ K.FG
have 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
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