-- Mathlib/FieldTheory/KrullTopology.lean
theorem krullTopology_t2 {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Algebra.IsIntegral K L] : T2Space (L ≃ₐ[K] L) :=
  { t2 := fun f g hfg => by
      let φ := f⁻¹ * g
      obtain ⟨x, hx⟩ := DFunLike.exists_ne hfg
      have hφx : φ x ≠ x

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
⊢ (fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

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

Result:
case intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
⊢ (fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : (fun x => f • x) w1 = (fun x => g • x) w2
⊢ False

Tactic:
dsimp at h

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : f * w1 = g * w2
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
⊢ False

Tactic:
have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : w1 * w2⁻¹ ∈ H
⊢ False

Proof state:
case a
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → φ x = x
⊢ x ∈ {x}

Tactic:
apply Set.mem_singleton

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → φ x = x
hxE : x ∈ E
⊢ False

Tactic:
exact hφx (h_in_H hxE)

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
⊢ f (f.symm (g x)) ≠ f x

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

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
⊢ f x ≠ g x

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : ∀ x ∈ E, φ x = x
⊢ False

Tactic:
specialize h_in_H x

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup (L ≃ₐ[K] L) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → φ x = x
⊢ False