awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ T'.rootSet E = T.rootSet E

Tactic:
have h' : T'.rootSet E = T.rootSet E := by simp [Set.ext_iff, Polynomial.mem_rootSet', T']
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
right :
  ∀
    (hT₂ :
      Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
        Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)),
    let T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T;
    ∀ (h' : T'.rootSet E = T.rootSet E), Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤

Tactic:
rw [← lift_inj, lift_adjoin, ← coe_val, hT₂.1.image_rootSet] at hT₂

Premises used: IntermediateField.lift_inj, IntermediateField.coe_val, Polynomial.Splits.image_rootSet, And.left, IntermediateField.lift_adjoin
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq (α := IntermediateField F E) (adjoin F (T.rootSet E)) (lift (F := K) ⊤)
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
right : Eq (α := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (adjoin (↥L) (T'.rootSet E))) ⊤
right₁ : Eq (α := IntermediateField F E) (adjoin F ((↑L : Set E) ∪ T'.rootSet E)) ⊤
right₂ : Eq (α := IntermediateField F E) (adjoin F (↑L : Set E) ⊔ adjoin F (T'.rootSet E)) ⊤
right₃ : L ⊔ adjoin F (T'.rootSet E) = ⊤
right₄ : L ⊔ adjoin F (T.rootSet E) = ⊤
right₅ : L ⊔ lift (F := K) ⊤ = ⊤
right₆ : L ⊔ K = ⊤
right₇ : K ⊔ L = ⊤
right₈ right₉ : Eq.{u_2 + 1} (α := IntermediateField F E) ⊤ ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤

Tactic:
rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]

Premises used: IntermediateField.lift_top, IntermediateField.restrictScalars_eq_top_iff, sup_comm, And.right, IntermediateField.adjoin_union, IntermediateField.adjoin_self, IntermediateField.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
φ : Gal(E/↥L)
x : ↥K
⊢ Eq (α := E)
    ((↑((((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F)) : (a : ↥K) → ↥K)
            x) :
        E) :
      E)
    ((φ : (a : E) → E) (↑x : E) : E)

Tactic:
simp [restrictRestrictAlgEquivMapHom, AlgEquiv.restrictNormalHom_apply]

Premises used: IntermediateField.restrictRestrictAlgEquivMapHom, AlgEquiv.restrictNormalHom_apply
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
⊢ Function.Injective (α := Gal(E/↥L)) (β := Gal(↥K/F))
    (⇑(restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) : (a : Gal(E/↥L)) → Gal(↥K/F))

Tactic:
(injective_iff_map_eq_one _).mpr fun φ hφ ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_one
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
refine :
  ∀ (φ : Gal(E/↥L))
    (hφ :
      Eq (α := Gal(↥K/F)) ((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F))
        (1 : Gal(↥K/F))),
    φ = 1
⊢ Function.Injective (α := Gal(E/↥L)) (β := Gal(↥K/F))
    (⇑(restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) : (a : Gal(E/↥L)) → Gal(↥K/F))

Tactic:
refine (injective_iff_map_eq_one _).mpr fun φ hφ ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_one
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h_1 : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ :
  Eq (α := Gal(↥K/F)) ((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F))
    (1 : Gal(↥K/F))
h :
  Eq (α := Gal(E/F)) ((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F))
    (1 : Gal(E/F))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      ∀ (a : E),
        Eq (α := E)
          ((((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F)) : (a : E) → E) a : E)
          ((1 : (a : E) → E) a : E))
    (a : E), Eq (α := E) ((φ : (a : E) → E) a : E) ((1 : (a : E) → E) a : E)
⊢ φ = 1

Tactic:
rwa [AlgEquiv.ext_iff] at h ⊢

Premises used: AlgEquiv.ext_iff
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ :
  Eq (α := Gal(↥K/F)) ((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F))
    (1 : Gal(↥K/F))
suffices :
  Eq (α := Gal(E/F)) ((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F))
    (1 : Gal(E/F))
⊢ φ = 1

Tactic:
suffices h : MulSemiringAction.toAlgAut Gal(E/L) F E φ = 1 by rwa [AlgEquiv.ext_iff] at h ⊢
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ :
  Eq (α := Gal(↥K/F)) ((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F))
    (1 : Gal(↥K/F))
rw :
  Membership.mem (α := Gal(E/F)) (K.fixingSubgroup ⊓ L.fixingSubgroup)
    ((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F))
⊢ Eq (α := Gal(E/F)) ((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F))
    (1 : Gal(E/F))

Tactic:
rw [← Subgroup.mem_bot, ← fixingSubgroup_top, ← h, fixingSubgroup_sup]

Premises used: IntermediateField.fixingSubgroup_top, Subgroup.mem_bot, IntermediateField.fixingSubgroup_sup
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ :
  Eq (α := Gal(↥K/F)) ((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F))
    (1 : Gal(↥K/F))
⊢ Membership.mem (α := Gal(E/F)) (K.fixingSubgroup ⊓ L.fixingSubgroup)
    ((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F))

Tactic:
⟨fun x ↦ (hφ ▸ restrictRestrictAlgEquivMapHom_apply K L φ x).symm, φ.commutes⟩

Premises used: Set.Mem, setOf, AlgEquiv.commutes, Set.inter, And.intro
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ :
  Eq (α := Gal(↥K/F)) ((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F))
    (1 : Gal(↥K/F))
⊢ Membership.mem (α := Gal(E/F)) (K.fixingSubgroup ⊓ L.fixingSubgroup)
    ((MulSemiringAction.toAlgAut Gal(E/↥L) F E : (a : Gal(E/↥L)) → Gal(E/F)) φ : Gal(E/F))

Tactic:
exact ⟨fun x ↦ (hφ ▸ restrictRestrictAlgEquivMapHom_apply K L φ x).symm, φ.commutes⟩
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
suffices :
  Eq (α := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E))) ⊥
⊢ Function.Surjective (α := Gal(E/↥L)) (β := Gal(↥K/F))
    (⇑(restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) : (a : Gal(E/↥L)) → Gal(↥K/F))

Tactic:
suffices fixedField (restrictRestrictAlgEquivMapHom F K L E).range = ⊥ from
     MonoidHom.range_eq_top.mp <|
      fixingSubgroup_fixedField (restrictRestrictAlgEquivMapHom F K L E).range ▸
        this ▸ fixingSubgroup_bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
⊢ Eq (α := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E))) ⊥

Tactic:
eq_bot_iff.mpr fun ⟨x, hx₁⟩ hx₂ ↦ ?_

Premises used: Iff.mpr, _private.0.IntermediateField.restrictRestrictAlgEquivMapHom_surjective.match_1, Membership.mem, Bot.bot, eq_bot_iff
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
refine :
  ∀ (x : ↥K) (x : E) (hx₁ : x ∈ K)
    (hx₂ :
      Membership.mem (γ := IntermediateField F ↥K)
        (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
        (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)),
    Membership.mem (γ := IntermediateField F ↥K) ⊥ (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
⊢ Eq (α := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E))) ⊥

Tactic:
refine eq_bot_iff.mpr fun ⟨x, hx₁⟩ hx₂ ↦ ?_

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  Membership.mem (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
⊢ Membership.mem (γ := Set E) (Set.range (ι := ↥L) (⇑(algebraMap (↥L) E) : (a : ↥L) → E)) x

Tactic:
mem_bot.mp <| (IsGalois.mem_bot_iff_fixed _).mpr fun φ ↦ ?_

Premises used: Iff.mpr, Set.Mem, Iff.mp, IntermediateField.mem_bot, IsGalois.mem_bot_iff_fixed
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  Membership.mem (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
refine : ∀ (φ : Gal(E/↥L)), (φ : (a : E) → E) x = x
⊢ Membership.mem (γ := Set E) (Set.range (ι := ↥L) (⇑(algebraMap (↥L) E) : (a : ↥L) → E)) x

Tactic:
refine mem_bot.mp <| (IsGalois.mem_bot_iff_fixed _).mpr fun φ ↦ ?_

Premises used: Iff.mpr, Iff.mp, IntermediateField.mem_bot, IsGalois.mem_bot_iff_fixed
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  Membership.mem (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
φ : Gal(E/↥L)
rw :
  (↑((((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F)) : (a : ↥K) → ↥K)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)) :
      E) =
    x
⊢ (φ : (a : E) → E) x = x

Tactic:
rw [← restrictRestrictAlgEquivMapHom_apply K L φ ⟨x, hx₁⟩]

Premises used: IntermediateField.restrictRestrictAlgEquivMapHom_apply, Subtype.mk
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  Membership.mem (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
φ : Gal(E/↥L)
rw :
  ∀
    (hx₂ :
      ∀ (f : Gal(↥K/F)),
        Membership.mem (γ := Subgroup Gal(↥K/F))
            (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)) f →
          (f : (a : ↥K) → ↥K) (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁) =
            Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
    (φ : Gal(E/↥L)),
    (↑((((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F)) : (a : ↥K) → ↥K)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)) :
        E) =
      x
⊢ (↑((((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F)) : (a : ↥K) → ↥K)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)) :
      E) =
    x

Tactic:
rw [mem_fixedField_iff] at hx₂

Premises used: IntermediateField.mem_fixedField_iff
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  ∀ (f : Gal(↥K/F)),
    Membership.mem (γ := Subgroup Gal(↥K/F))
        (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)) f →
      (f : (a : ↥K) → ↥K) (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁) = Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁
φ : Gal(E/↥L)
⊢ (↑((((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F)) : (a : ↥K) → ↥K)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)) :
      E) =
    x

Tactic:
congr_arg ((↑) : K → E) <| hx₂ (restrictRestrictAlgEquivMapHom F K L E φ) ⟨φ, rfl⟩

Premises used: Membership.mem, Subtype, congr_arg, Exists.intro, IntermediateField.restrictRestrictAlgEquivMapHom, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  ∀ (f : Gal(↥K/F)),
    Membership.mem (γ := Subgroup Gal(↥K/F))
        (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)) f →
      (f : (a : ↥K) → ↥K) (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁) = Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁
φ : Gal(E/↥L)
⊢ (↑((((restrictRestrictAlgEquivMapHom F (↥K) (↥L) E : (a : Gal(E/↥L)) → Gal(↥K/F)) φ : Gal(↥K/F)) : (a : ↥K) → ↥K)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)) :
      E) =
    x

Tactic:
exact congr_arg ((↑) : K → E) <| hx₂ (restrictRestrictAlgEquivMapHom F K L E φ) ⟨φ, rfl⟩

Premises used: Membership.mem, Subtype, congr_arg, Exists.intro, IntermediateField.restrictRestrictAlgEquivMapHom, Subtype.val, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x_1 : ↥K
x : E
hx₁ : x ∈ K
hx₂ :
  Membership.mem (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
obtain :
  ∀ (y : E) (hy : y ∈ L)
    (hx₁ :
      Membership.mem (α := E) K ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy) : E))
    (hx₂ :
      Membership.mem (α := ↥K) (γ := IntermediateField F ↥K)
        (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
        (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
            ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy)) hx₁ :
          ↥K)),
    Membership.mem (α := ↥K) (γ := IntermediateField F ↥K) ⊥
      (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
          ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy)) hx₁ :
        ↥K)
⊢ Membership.mem (γ := IntermediateField F ↥K) ⊥ (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)

Tactic:
obtain ⟨⟨y, hy⟩, rfl⟩ : x ∈ Set.range (algebraMap L E) := by
    refine mem_bot.mp <| (IsGalois.mem_bot_iff_fixed _).mpr fun φ ↦ ?_
    rw [← restrictRestrictAlgEquivMapHom_apply K L φ ⟨x, hx₁⟩]
    rw [mem_fixedField_iff] at hx₂
    exact congr_arg ((↑) : K → E) <| hx₂ (restrictRestrictAlgEquivMapHom F K L E φ) ⟨φ, rfl⟩

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Set.range, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x : ↥K
y : E
hy : y ∈ L
hx₁ : Membership.mem (α := E) K ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy) : E)
hx₂ :
  Membership.mem (α := ↥K) (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy)) hx₁ :
      ↥K)
⊢ Membership.mem (γ := IntermediateField F E) ⊥ y

Tactic:
h ▸ mem_inf.mpr ⟨hx₁, hy⟩

Premises used: Iff.mpr, Eq.rec, IntermediateField.mem_inf, And.intro
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x : ↥K
y : E
hy : y ∈ L
hx₁ : Membership.mem (α := E) K ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy) : E)
hx₂ :
  Membership.mem (α := ↥K) (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy)) hx₁ :
      ↥K)
obtain :
  ∀ (z : F) (hy : Membership.mem (α := E) L ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E))
    (hx₁ :
      Membership.mem (α := E) K
        ((algebraMap (↥L) E : (a : ↥L) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L) :
          E))
    (hx₂ :
      Membership.mem (α := ↥K) (γ := IntermediateField F ↥K)
        (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
        (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
            ((algebraMap (↥L) E : (a : ↥L) → E)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L))
            hx₁ :
          ↥K)),
    Membership.mem (α := ↥K) (γ := IntermediateField F ↥K) ⊥
      (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
          ((algebraMap (↥L) E : (a : ↥L) → E)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L))
          hx₁ :
        ↥K)
⊢ Membership.mem (α := ↥K) (γ := IntermediateField F ↥K) ⊥
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E) (Subtype.mk (p := fun (x : E) ↦ x ∈ L) y hy)) hx₁ :
      ↥K)

Tactic:
obtain ⟨z, rfl⟩ : y ∈ (⊥ : IntermediateField F E) := h ▸ mem_inf.mpr ⟨hx₁, hy⟩

Premises used: Bot.bot, rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : Normal.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
inst_5 : FiniteDimensional (↥L) E
inst_6 : IsGalois (↥L) E
h : K ⊓ L = ⊥
x : ↥K
z : F
hy : Membership.mem (α := E) L ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z : E)
hx₁ :
  Membership.mem (α := E) K
    ((algebraMap (↥L) E : (a : ↥L) → E)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L) :
      E)
hx₂ :
  Membership.mem (α := ↥K) (γ := IntermediateField F ↥K)
    (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E)))
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L))
        hx₁ :
      ↥K)
⊢ Membership.mem (α := ↥K) (γ := IntermediateField F ↥K) ⊥
    (Subtype.mk (p := fun (x : E) ↦ x ∈ K)
        ((algebraMap (↥L) E : (a : ↥L) → E)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ L) ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) z) hy : ↥L))
        hx₁ :
      ↥K)

Tactic:
mem_bot.mp ⟨z, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Iff.mp, Set.range, IntermediateField.mem_bot, rfl