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
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₁ L₂ : FiniteGaloisIntermediateField k K
h : L₁ ⟶ L₂
⊢ Eq (α := (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4)) (Functor.obj (finGaloisGroupFunctor k K) (op L₁)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FiniteGrp.{u_4}) ↦ (↑x1.toGrp : Type u_4) →* (↑x2.toGrp : Type u_4))
            (CC := fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4)) (X :=
            Functor.obj (finGaloisGroupFunctor k K) (op L₂))
            (CategoryTheory.Functor.map (finGaloisGroupFunctor k K) h.op) :
          (a : (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4)) ((finGaloisGroupFunctor k K).obj (op L₂))) →
            (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4)) ((finGaloisGroupFunctor k K).obj (op L₁)))
        ((proj L₂ :
              (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                Gal(↥L₂.toIntermediateField/k))
            g :
          Gal(↥L₂.toIntermediateField/k)) :
      (fun (X : FiniteGrp.{u_4}) ↦ (↑X.toGrp : Type u_4)) (Functor.obj (finGaloisGroupFunctor k K) (op L₁)))
    ((proj L₁ :
          (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
            Gal(↥L₁.toIntermediateField/k))
        g :
      Gal(↥L₁.toIntermediateField/k))

Tactic:
g.prop h.op

Premises used: Quiver.Hom.op, Subtype.prop
-- 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
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
L : IntermediateField k K
finiteDimensional : FiniteDimensional.{u_3, u_4} k ↥L
isGalois : IsGalois.{u_3, u_4} k ↥L
x :
  ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
        FiniteGaloisIntermediateField k K }.toIntermediateField
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
      FiniteGaloisIntermediateField k K } ≤
    L'
⊢ Eq.{u_4 + 1} (α := K)
    (↑((((proj
                    { toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
                      FiniteGaloisIntermediateField k K } :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥{ toIntermediateField := L, finiteDimensional := finiteDimensional,
                            isGalois := isGalois }.toIntermediateField/k))
                g :
              Gal(↥{ toIntermediateField := L, finiteDimensional := finiteDimensional, isGalois := isGalois :
                      FiniteGaloisIntermediateField k K }.toIntermediateField/k)) :
            (a :
                ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional,
                      isGalois := isGalois }.toIntermediateField) →
              ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional,
                    isGalois := isGalois }.toIntermediateField)
          x) :
      K)
    (↑((((proj L' :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L'.toIntermediateField/k))
                g :
              Gal(↥L'.toIntermediateField/k)) :
            (a : ↥L'.toIntermediateField) → ↥L'.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L'.toIntermediateField) (↑x : K) ⋯)) :
      K)

Tactic:
?_
-- 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
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)
x : K
y : ↥(toIntermediateField (adjoin k {x}))
L : FiniteGaloisIntermediateField k K
h : x ∈ L.toIntermediateField
⊢ Eq.{u_4 + 1} (α := K)
    (↑((((proj (adjoin k {x}) :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥(adjoin k {x}).toIntermediateField/k))
                g :
              Gal(↥(toIntermediateField (adjoin k {x}))/k)) :
            (a : ↥(adjoin k {x}).toIntermediateField) → ↥(adjoin k {x}).toIntermediateField)
          y) :
      K)
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) (↑y : K) ⋯)) :
      K)

Tactic:
proj_of_le _ g y _ _

Premises used: InfiniteGalois.proj_of_le
-- 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
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)
x : K
⊢ Membership.mem (γ := Set K) {x} x

Tactic:
simp only [Set.mem_singleton_iff]

Premises used: Set.mem_singleton_iff
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g x =
    (↑((((proj L :
                  (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                    Gal(↥L.toIntermediateField/k))
                g :
              Gal(↥L.toIntermediateField/k)) :
            (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
          (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
      K)

Tactic:
proj_adjoin_singleton_val g _ _ L hx

Premises used: InfiniteGalois.proj_adjoin_singleton_val, _private.0.InfiniteGalois.toAlgEquivAux
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
rw :
  Eq (α := K)
    ((↑((((proj L :
                    (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                      Gal(↥L.toIntermediateField/k))
                  g :
                Gal(↥L.toIntermediateField/k)) :
              (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
        K) :
      K)
    ((AlgEquiv.liftNormal (K₁ := ↥L.toIntermediateField) (K₂ := ↥L.toIntermediateField)
            ((proj L :
                (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                  Gal(↥L.toIntermediateField/k))
              g)
            K :
          (a : K) → K)
        x :
      K)
⊢ toAlgEquivAux g x =
    (AlgEquiv.liftNormal (K₁ := ↥L.toIntermediateField) (K₂ := ↥L.toIntermediateField)
          ((proj L :
              (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                Gal(↥L.toIntermediateField/k))
            g)
          K :
        (a : K) → K)
      x

Tactic:
rw [toAlgEquivAux_eq_proj_of_mem g x L hx]

Premises used: InfiniteGalois.toAlgEquivAux_eq_proj_of_mem
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ Eq (α := K)
    ((↑((((proj L :
                    (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                      Gal(↥L.toIntermediateField/k))
                  g :
                Gal(↥L.toIntermediateField/k)) :
              (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
        K) :
      K)
    ((AlgEquiv.liftNormal (K₁ := ↥L.toIntermediateField) (K₂ := ↥L.toIntermediateField)
            ((proj L :
                (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                  Gal(↥L.toIntermediateField/k))
              g)
            K :
          (a : K) → K)
        x :
      K)

Tactic:
(AlgEquiv.liftNormal_commutes (proj L g) _ ⟨x, hx⟩).symm

Premises used: InfiniteGalois.proj, Subtype.mk, AlgEquiv.liftNormal_commutes, Eq.symm, DFunLike.coe
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ Eq (α := K)
    ((↑((((proj L :
                    (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                      Gal(↥L.toIntermediateField/k))
                  g :
                Gal(↥L.toIntermediateField/k)) :
              (a : ↥L.toIntermediateField) → ↥L.toIntermediateField)
            (Subtype.mk (p := fun (x : K) ↦ x ∈ L.toIntermediateField) x hx)) :
        K) :
      K)
    ((AlgEquiv.liftNormal (K₁ := ↥L.toIntermediateField) (K₂ := ↥L.toIntermediateField)
            ((proj L :
                (a : (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4)) →
                  Gal(↥L.toIntermediateField/k))
              g)
            K :
          (a : K) → K)
        x :
      K)

Tactic:
exact (AlgEquiv.liftNormal_commutes (proj L g) _ ⟨x, hx⟩).symm

Premises used: InfiniteGalois.proj, Subtype.mk, AlgEquiv.liftNormal_commutes, Eq.symm, DFunLike.coe
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g x}
⊢ x ∈ L.toIntermediateField

Tactic:
have hx : x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert x {toAlgEquivAux g x})
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g x}
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g x ∈ L.toIntermediateField

Tactic:
have hx' : toAlgEquivAux g x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert_of_mem x rfl)
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g x}
hx : x ∈ L.toIntermediateField
hx' : toAlgEquivAux g x ∈ L.toIntermediateField
⊢ toAlgEquivAux g⁻¹ (toAlgEquivAux g x) = x

Tactic:
simp only [toAlgEquivAux_eq_proj_of_mem _ _ L hx', map_inv, AlgEquiv.aut_inv,
      mk_toAlgEquivAux g x L hx' hx, AlgEquiv.symm_apply_apply]

Premises used: map_inv, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, AlgEquiv.aut_inv, AlgEquiv.symm_apply_apply, InfiniteGalois.mk_toAlgEquivAux
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g⁻¹ x}
⊢ x ∈ L.toIntermediateField

Tactic:
have hx : x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert x {toAlgEquivAux g⁻¹ x})
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g⁻¹ x}
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g⁻¹ x ∈ L.toIntermediateField

Tactic:
have hx' : toAlgEquivAux g⁻¹ x ∈ L.1 := subset_adjoin _ _ (Set.mem_insert_of_mem x rfl)
-- 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
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)
x : K
L : FiniteGaloisIntermediateField k K := adjoin k {x, toAlgEquivAux g⁻¹ x}
hx : x ∈ L.toIntermediateField
hx' : toAlgEquivAux g⁻¹ x ∈ L.toIntermediateField
⊢ toAlgEquivAux g (toAlgEquivAux g⁻¹ x) = x

Tactic:
simp only [toAlgEquivAux_eq_proj_of_mem _ _ L hx', mk_toAlgEquivAux g⁻¹ x L hx' hx, map_inv,
      AlgEquiv.aut_inv, AlgEquiv.apply_symm_apply]

Premises used: map_inv, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, AlgEquiv.aut_inv, AlgEquiv.apply_symm_apply, Inv.inv, InfiniteGalois.mk_toAlgEquivAux
-- 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
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)
x y : K
⊢ Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) x

Tactic:
have hx : x ∈ (adjoin k {x, y}).1 := subset_adjoin _ _ (Set.mem_insert x {y})
-- 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
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)
x y : K
hx : Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) x
⊢ Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) y

Tactic:
have hy : y ∈ (adjoin k {x, y}).1 := subset_adjoin _ _ (Set.mem_insert_of_mem x rfl)
-- 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
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)
x y : K
hx : Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) x
hy : Membership.mem (γ := IntermediateField k K) (toIntermediateField (adjoin k {x, y})) y
⊢ toAlgEquivAux g (x + y) = toAlgEquivAux g x + toAlgEquivAux g y

Tactic:
simp only [toAlgEquivAux_eq_liftNormal g x (adjoin k {x, y}) hx,
      toAlgEquivAux_eq_liftNormal g y (adjoin k {x, y}) hy,
      toAlgEquivAux_eq_liftNormal g (x + y) (adjoin k {x, y}) (add_mem hx hy), map_add]

Premises used: map_add, Insert.insert, HAdd.hAdd, InfiniteGalois.toAlgEquivAux_eq_liftNormal, FiniteGaloisIntermediateField.adjoin, AddMemClass.add_mem, Singleton.singleton
-- 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
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)
x : k
⊢ toAlgEquivAux g ((algebraMap k K : (a : k) → K) x) = (algebraMap k K : (a : k) → K) x

Tactic:
simp only [toAlgEquivAux_eq_liftNormal g _ ⊥ (algebraMap_mem _ x), AlgEquiv.commutes]

Premises used: AlgEquiv.commutes, Bot.bot, InfiniteGalois.toAlgEquivAux_eq_liftNormal, algebraMap_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
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)
a :
  (↑((algEquivToLimit k K :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
          (limitToAlgEquiv g)) :
      (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
        (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4)) =
    (↑g :
      (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
        (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
⊢ (algEquivToLimit k K : (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
      (limitToAlgEquiv g) =
    g

Tactic:
apply Subtype.val_injective

Premises used: Subtype.val_injective
-- 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
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)
a :
  ∀ (L : (FiniteGaloisIntermediateField k K)ᵒᵖ),
    (↑((algEquivToLimit k K :
                (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
              (limitToAlgEquiv g)) :
          (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
        L =
      (↑g :
          (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
            (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
        L
⊢ (↑((algEquivToLimit k K :
            (a : Gal(K/k)) → (↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop : Type u_4))
          (limitToAlgEquiv g)) :
      (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
        (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4)) =
    (↑g :
      (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
        (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))

Tactic:
ext L
-- 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
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)ᵒᵖ
a :
  ∀ (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)
⊢ (limitToAlgEquiv g).restrictNormal ↥(unop L).toIntermediateField =
    (↑g :
        (j : (FiniteGaloisIntermediateField k K)ᵒᵖ) →
          (↑((asProfiniteGaloisGroupFunctor k K).obj j).toProfinite.toTop : Type u_4))
      L

Tactic:
ext x
-- 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
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 (α := 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:
AlgEquiv.restrictNormal_commutes (limitToAlgEquiv g) L.unop x

Premises used: Membership.mem, Subtype, AlgEquiv.restrictNormal_commutes, FiniteGaloisIntermediateField.toIntermediateField, InfiniteGalois.limitToAlgEquiv, Opposite.unop