awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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) = ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₄ : L ⊔ adjoin F (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]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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) = ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₅ : L ⊔ lift (F := K) ⊤ = ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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) ⊤ = ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₆ : L ⊔ K = ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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 = ⊤
⊢ Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
have right₈ : Eq.{u_2 + 1} (α := IntermediateField F E) ⊤ ⊤
Tactic: rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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))
have 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
Tactic: refine (injective_iff_map_eq_one _).mpr fun φ hφ ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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))
⊢ φ = 1
have 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)
Tactic: rwa [AlgEquiv.ext_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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))
⊢ φ = 1
have 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))
Tactic: suffices h : MulSemiringAction.toAlgAut Gal(E/L) F E φ = 1 by rwa [AlgEquiv.ext_iff] at h ⊢
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← Subgroup.mem_bot, ← fixingSubgroup_top, ← h, fixingSubgroup_sup]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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 = ⊥
⊢ Function.Surjective (α := Gal(E/↥L)) (β := Gal(↥K/F))
    (⇑(restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) : (a : Gal(E/↥L)) → Gal(↥K/F))
have suffices : Eq (α := IntermediateField F ↥K)
  (fixedField (MonoidHom.range (G := Gal(E/↥L)) (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E))) ⊥
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
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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))) ⊥
have 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₁)
Tactic: refine eq_bot_iff.mpr fun ⟨x, hx₁⟩ hx₂ ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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
have refine : ∀ (φ : Gal(E/↥L)), (φ : (a : E) → E) x = x
Tactic: refine mem_bot.mp <| (IsGalois.mem_bot_iff_fixed _).mpr fun φ ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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)
⊢ (φ : (a : E) → E) x = x
have 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
Tactic: rw [← restrictRestrictAlgEquivMapHom_apply K L φ ⟨x, hx₁⟩]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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)
⊢ (↑((((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
have 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
Tactic: rw [mem_fixedField_iff] at hx₂
Cleared hypotheses: hx₂, φ
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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 (γ := IntermediateField F ↥K) ⊥ (Subtype.mk (p := fun (x : E) ↦ x ∈ K) x hx₁)
have 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)
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⟩
Cleared hypotheses: x, hx₁, hx₂
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
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 (α := ↥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)
have 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)
Tactic: obtain ⟨z, rfl⟩ : y ∈ (⊥ : IntermediateField F E) := h ▸ mem_inf.mpr ⟨hx₁, hy⟩
Cleared hypotheses: y, hy, hx₁, hx₂
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
⊢ IsCyclic.{u_2} Gal(K/F)
have this : Fintype.card.{u_2} Gal(K/F) ≤ 2
Tactic: have := finrank_eq_two F K ▸ AlgEquiv.card_le
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (hypothesis)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
this : Fintype.card.{u_2} Gal(K/F) ≤ 2
⊢ IsCyclic.{u_2} Gal(K/F)
have this₁ : Nat.card.{u_2} Gal(K/F) ≤ 2
Tactic: rw [← Nat.card_eq_fintype_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
this : Nat.card.{u_2} Gal(K/F) ≤ 2
⊢ IsCyclic.{u_2} Gal(K/F)
have 0 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 0) (this : LE.le (α := ℕ) 0 2), IsCyclic.{u_2} Gal(K/F)
Tactic: interval_cases h : Nat.card Gal(K/F)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
this : Nat.card.{u_2} Gal(K/F) ≤ 2
0 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 0) (this : LE.le (α := ℕ) 0 2), IsCyclic.{u_2} Gal(K/F)
⊢ IsCyclic.{u_2} Gal(K/F)
have 1 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 1) (this : LE.le (α := ℕ) 1 2), IsCyclic.{u_2} Gal(K/F)
Tactic: interval_cases h : Nat.card Gal(K/F)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Basic (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : IsQuadraticExtension F K
this : Nat.card.{u_2} Gal(K/F) ≤ 2
0 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 0) (this : LE.le (α := ℕ) 0 2), IsCyclic.{u_2} Gal(K/F)
1 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 1) (this : LE.le (α := ℕ) 1 2), IsCyclic.{u_2} Gal(K/F)
⊢ IsCyclic.{u_2} Gal(K/F)
have 2 : ∀ (h : Nat.card.{u_2} Gal(K/F) = 2) (this : LE.le (α := ℕ) 2 2), IsCyclic.{u_2} Gal(K/F)
Tactic: interval_cases h : Nat.card Gal(K/F)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.GaloisClosure (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ Eq (α := FiniteGaloisIntermediateField k K) (adjoin k ((⇑f : (a : K) → K) '' s)) (adjoin k s)
have a : Eq (α := IntermediateField k K) (toIntermediateField (adjoin k ((⇑f : (a : K) → K) '' s)))
  (toIntermediateField (adjoin k s))
Tactic: apply val_injective
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.GaloisClosure (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ Eq (α := IntermediateField k K) (normalClosure k (↥(IntermediateField.adjoin k ((⇑f : (a : K) → K) '' s))) K)
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)
have a : Eq (α := IntermediateField k K) (normalClosure k (↥(map f (IntermediateField.adjoin k s))) K)
  (normalClosure k (↥(IntermediateField.adjoin k s)) K)
Tactic: rw [← IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.GaloisClosure (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
f : K →ₐ[k] K
s : Set K
inst_4 : Finite.{u_2 + 1} (↑s : Type u_2)
a :
  Eq (α := IntermediateField k K) (normalClosure k (↥(map f (IntermediateField.adjoin k s))) K)
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)
⊢ Eq (α := IntermediateField k K) (normalClosure k (↥(IntermediateField.adjoin k ((⇑f : (a : K) → K) '' s))) K)
    (normalClosure k (↥(IntermediateField.adjoin k s)) K)
have a₁ : Eq (α := IntermediateField k K) (normalClosure k (↥(IntermediateField.adjoin k s)) K)
  (normalClosure k (↥(IntermediateField.adjoin k s)) K)
Tactic: rw [← IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
⊢ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∈ nhds σ
have apply : ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t
Tactic: apply mem_nhds_iff.mpr
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
⊢ ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t
have rcases : ∀ (y : K) (yL : y ∈ (↑L : Set K)) (ne : y ∉ fun (a : K) ↦ σ • a = a),
  ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t
Tactic: rcases Set.not_subset.mp ((mem_fixingSubgroup_iff Gal(K/k)).not.mp h) with ⟨y, yL, ne⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
⊢ ∃ t ⊆ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ, IsOpen t ∧ σ ∈ t
have h₁ : σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
    (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∧
  IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
    σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
Tactic: use σ • ((adjoin k {y}).1.fixingSubgroup : Set Gal(K/k))
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
⊢ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
      (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∧
    IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
      σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
have h₁ : σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
  (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Galois.Infinite (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
L : IntermediateField k K
inst_3 : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
y : K
yL : y ∈ (↑L : Set K)
ne : y ∉ fun (a : K) ↦ σ • a = a
h₁ :
  σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
    (↑L.fixingSubgroup : Set Gal(K/k))ᶜ
⊢ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k)) ⊆
      (↑L.fixingSubgroup : Set Gal(K/k))ᶜ ∧
    IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
      σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
have h₂ : IsOpen (σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))) ∧
  σ ∈ σ • (↑(IntermediateField.fixingSubgroup (toIntermediateField (adjoin k {y}))) : Set Gal(K/k))
Tactic: constructor