awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
⊢ IsClosed (↑E.fixingSubgroup : Set Gal(L/K))

Tactic:
OpenSubgroup.isClosed ⟨E.fixingSubgroup, E.fixingSubgroup_isOpen⟩

Premises used: IntermediateField.fixingSubgroup, OpenSubgroup.mk, IntermediateField.fixingSubgroup_isOpen, OpenSubgroup.isClosed
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
obtain :
  ∀ (x : L) (hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)),
    (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
      f g
⊢ (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g

Tactic:
obtain ⟨x, hx⟩ := DFunLike.exists_ne hfg

Premises used: DFunLike.exists_ne
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
apply : Ne (α := L) ((f : (a : L) → L) ((φ : (a : L) → L) x : L) : L) ((f : (a : L) → L) x : L)
⊢ (φ : (a : L) → L) x ≠ x

Tactic:
apply ne_of_apply_ne f

Premises used: ne_of_apply_ne, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
change :
  Ne (α := L) ((f : (a : L) → L) ((f.symm : (a : L) → L) ((g : (a : L) → L) x : L) : L) : L) ((f : (a : L) → L) x : L)
⊢ Ne (α := L) ((f : (a : L) → L) ((φ : (a : L) → L) x : L) : L) ((f : (a : L) → L) x : L)

Tactic:
change f (f.symm (g x)) ≠ f x

Premises used: AlgEquiv.symm, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx rw : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
⊢ Ne (α := L) ((f : (a : L) → L) ((f.symm : (a : L) → L) ((g : (a : L) → L) x : L) : L) : L) ((f : (a : L) → L) x : L)

Tactic:
rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]

Premises used: AlgEquiv.apply_symm_apply, ne_comm, DFunLike.coe
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
⊢ Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)

Tactic:
hx
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
⊢ Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)

Tactic:
exact hx
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
⊢ (φ : (a : L) → L) x ≠ x

Tactic:
have hφx : φ x ≠ x := by
        apply ne_of_apply_ne f
        change f (f.symm (g x)) ≠ f x
        rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
        exact hx
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
⊢ Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))

Tactic:
have h_basis : (H : Set Gal(L/K)) ∈ galGroupBasis K L := ⟨H, ⟨E, ⟨h_findim, rfl⟩⟩, rfl⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
⊢ Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) (↑H : Set Gal(L/K))

Tactic:
have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
h_nhds : Membership.mem (γ := Filter Gal(L/K)) (𝓝 1) (↑H : Set Gal(L/K))
⊢ ∃ t ⊆ (↑H : Set Gal(L/K)), IsOpen t ∧ 1 ∈ t

Tactic:
rw [mem_nhds_iff] at h_nhds

Premises used: mem_nhds_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
h_nhds : ∃ t ⊆ (↑H : Set Gal(L/K)), IsOpen t ∧ 1 ∈ t
rcases :
  ∀ (W : Set Gal(L/K)) (hWH : W ⊆ (↑H : Set Gal(L/K))) (hW_open : IsOpen W) (hW_1 : 1 ∈ W),
    (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
      f g
⊢ (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g

Tactic:
rcases h_nhds with ⟨W, hWH, hW_open, hW_1⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g

Tactic:
⟨f • W, g • W,
        ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, ?_⟩⟩

Premises used: IsOpen.leftCoset, And.intro, Exists.intro, HSMul.hSMul, mul_one, OfNat.ofNat
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
refine : Disjoint (f • W) (g • W)
⊢ (fun (x y : Gal(L/K)) ↦ ∃ (u : Set Gal(L/K)) (v : Set Gal(L/K)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f
    g

Tactic:
refine ⟨f • W, g • W,
        ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, ?_⟩⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
rw : ∀ ⦃a : Gal(L/K)⦄, a ∈ f • W → a ∉ g • W
⊢ Disjoint (f • W) (g • W)

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : f * w1 = g * w2
⊢ w1 * w2⁻¹ = f⁻¹ * g

Tactic:
rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h

Premises used: mul_assoc, eq_inv_mul_iff_mul_eq, mul_inv_eq_iff_eq_mul, Iff.symm
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
⊢ w1 * w2⁻¹ ∈ H

Tactic:
have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : w1 * w2⁻¹ ∈ H
⊢ f⁻¹ * g ∈ H

Tactic:
rw [h] at h_in_H
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : f⁻¹ * g ∈ H
⊢ φ ∈ E.fixingSubgroup

Tactic:
change φ ∈ E.fixingSubgroup at h_in_H

Premises used: IntermediateField.fixingSubgroup
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : φ ∈ E.fixingSubgroup
⊢ ∀ x ∈ E, (φ : (a : L) → L) x = x

Tactic:
rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H

Premises used: IntermediateField.mem_fixingSubgroup_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : ∀ x ∈ E, (φ : (a : L) → L) x = x
⊢ x ∈ E → (φ : (a : L) → L) x = x

Tactic:
specialize h_in_H x
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
a : Membership.mem (γ := Set L) {x} x
⊢ x ∈ E

Tactic:
apply IntermediateField.subset_adjoin

Premises used: IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
⊢ Membership.mem (γ := Set L) {x} x

Tactic:
apply Set.mem_singleton

Premises used: Set.mem_singleton
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
⊢ x ∈ E

Tactic:
have hxE : x ∈ E := by
        apply IntermediateField.subset_adjoin
        apply Set.mem_singleton
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
hxE : x ∈ E
⊢ False

Tactic:
hφx (h_in_H hxE)
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : Ne (α := L) ((f : (a : L) → L) x : L) ((g : (a : L) → L) x : L)
hφx : (φ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional.{u_1, u_2} K ↥E := ⋯
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : Membership.mem (γ := GroupFilterBasis Gal(L/K)) (galGroupBasis K L) (↑H : Set Gal(L/K))
W : Set Gal(L/K)
hWH : W ⊆ (↑H : Set Gal(L/K))
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → (φ : (a : L) → L) x = x
hxE : x ∈ E
⊢ False

Tactic:
exact hφx (h_in_H hxE)
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
rw : Pairwise fun (x1 x2 : Gal(L/K)) ↦ ∃ (U : Set Gal(L/K)), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
⊢ TotallySeparatedSpace.{u_2} Gal(L/K)

Tactic:
rw [totallySeparatedSpace_iff_exists_isClopen]

Premises used: totallySeparatedSpace_iff_exists_isClopen
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
rwa : ¬σ⁻¹ * τ = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ¬σ = τ
⊢ σ⁻¹ * τ ≠ 1

Tactic:
rwa [Ne, inv_mul_eq_one]

Premises used: Ne, inv_mul_eq_one
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
⊢ σ⁻¹ * τ ≠ 1

Tactic:
have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
rcases : ∀ (x : L) (hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x), ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ

Tactic:
rcases DFunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩

Premises used: DFunLike.exists_ne
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯

Tactic:
haveI := IntermediateField.adjoin.finiteDimensional
    (Algebra.IsIntegral.isIntegral (R := K) x)
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ

Tactic:
⟨σ • E.fixingSubgroup,
    ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩,
    ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩

Premises used: IntermediateField.fixingSubgroup, IsOpen.leftCoset, IsClosed.leftCoset, IntermediateField.fixingSubgroup_isClosed, SetLike.coe, And.intro, Exists.intro, Submonoid.one_mem', IntermediateField.fixingSubgroup_isOpen, HSMul.hSMul, mul_one, OfNat.ofNat, Subgroup.toSubmonoid
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
refine : τ ∈ (σ • (↑E.fixingSubgroup : Set Gal(L/K)))ᶜ
⊢ ∃ (U : Set Gal(L/K)), IsClopen U ∧ σ ∈ U ∧ τ ∈ Uᶜ

Tactic:
refine ⟨σ • E.fixingSubgroup,
    ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩,
    ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
simp : ∃ (x : L) (_ : x ∈ E), ¬(σ⁻¹ * τ : (a : L) → L) x = x
⊢ τ ∈ (σ • (↑E.fixingSubgroup : Set Gal(L/K)))ᶜ

Tactic:
simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe,
    IntermediateField.mem_fixingSubgroup_iff, not_forall]

Premises used: mem_leftCoset_iff, SetLike.mem_coe, Classical.not_forall, IntermediateField.mem_fixingSubgroup_iff, Set.mem_compl_iff
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ ∃ (x : L) (_ : x ∈ E), ¬(σ⁻¹ * τ : (a : L) → L) x = x

Tactic:
⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩

Premises used: IntermediateField.mem_adjoin_simple_self, Exists.intro
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
σ τ : Gal(L/K)
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : (σ⁻¹ * τ : (a : L) → L) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional.{u_1, u_2} K ↥K⟮x⟯
⊢ ∃ (x : L) (_ : x ∈ E), ¬(σ⁻¹ * τ : (a : L) → L) x = x

Tactic:
exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
⊢ IsTotallySeparated.{u_2} (α := Gal(L/K)) Set.univ

Tactic:
(totallySeparatedSpace_iff _).mp inferInstance

Premises used: inferInstance, totallySeparatedSpace_iff, Iff.mp
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
rw : IsOpen (X := Gal(L/K)) {1}
⊢ DiscreteTopology.{u_2} Gal(L/K)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_one]

Premises used: discreteTopology_iff_isOpen_singleton_one