[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ fixingSubgroup ⊥ = ⊤
[PROOFSTEP]
ext f
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
⊢ f ∈ fixingSubgroup ⊥ ↔ f ∈ ⊤
[PROOFSTEP]
refine' ⟨fun _ => Subgroup.mem_top _, fun _ => _⟩
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
⊢ f ∈ fixingSubgroup ⊥
[PROOFSTEP]
rintro ⟨x, hx : x ∈ (⊥ : IntermediateField K L)⟩
[GOAL]
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx : x ∈ ⊥
⊢ f • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }
[PROOFSTEP]
rw [IntermediateField.mem_bot] at hx 
[GOAL]
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx✝ : x ∈ ⊥
hx : x ∈ Set.range ↑(algebraMap K L)
⊢ f • ↑{ val := x, property := hx✝ } = ↑{ val := x, property := hx✝ }
[PROOFSTEP]
rcases hx with ⟨y, rfl⟩
[GOAL]
case h.mk.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
y : K
hx : ↑(algebraMap K L) y ∈ ⊥
⊢ f • ↑{ val := ↑(algebraMap K L) y, property := hx } = ↑{ val := ↑(algebraMap K L) y, property := hx }
[PROOFSTEP]
exact f.commutes y
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
⊢ fixingSubgroup E2 ≤ fixingSubgroup E1
[PROOFSTEP]
rintro σ hσ ⟨x, hx⟩
[GOAL]
case mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
σ : L ≃ₐ[K] L
hσ : σ ∈ fixingSubgroup E2
x : L
hx : x ∈ ↑E1
⊢ σ • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }
[PROOFSTEP]
exact hσ ⟨x, h12 hx⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ∀ {x y : Set (L ≃ₐ[K] L)},
    x ∈ (fun g => g.carrier) '' fixedByFinite K L →
      y ∈ (fun g => g.carrier) '' fixedByFinite K L → ∃ z, z ∈ (fun g => g.carrier) '' fixedByFinite K L ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro X Y ⟨H1, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨H2, ⟨E2, h_E2, rfl⟩, rfl⟩
[GOAL]
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
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ ∃ z,
    z ∈ (fun g => g.carrier) '' fixedByFinite K L ∧
      z ⊆
        (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∩
          (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
use(IntermediateField.fixingSubgroup (E1 ⊔ E2)).carrier
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ∈
      (fun g => g.carrier) '' fixedByFinite K L ∧
    (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∩
        (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
refine' ⟨⟨_, ⟨_, finiteDimensional_sup E1 E2 h_E1 h_E2, rfl⟩, rfl⟩, _⟩
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
    (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∩
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
rw [Set.subset_inter_iff]
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∧
    (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
exact ⟨IntermediateField.fixingSubgroup.antimono le_sup_left, IntermediateField.fixingSubgroup.antimono le_sup_right⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
U : Set (L ≃ₐ[K] L)
hU : U ∈ (galBasis K L).sets
⊢ U * U ⊆ U
[PROOFSTEP]
rcases hU with ⟨H, _, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup (L ≃ₐ[K] L)
left✝ : H ∈ fixedByFinite K L
⊢ (fun g => g.carrier) H * (fun g => g.carrier) H ⊆ (fun g => g.carrier) H
[PROOFSTEP]
rintro x ⟨a, b, haH, hbH, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup (L ≃ₐ[K] L)
left✝ : H ∈ fixedByFinite K L
a b : L ≃ₐ[K] L
haH : a ∈ (fun g => g.carrier) H
hbH : b ∈ (fun g => g.carrier) H
⊢ (fun x x_1 => x * x_1) a b ∈ (fun g => g.carrier) H
[PROOFSTEP]
exact H.mul_mem haH hbH
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
U : Set (L ≃ₐ[K] L)
hU : U ∈ (galBasis K L).sets
⊢ U ⊆ (fun x => x⁻¹) ⁻¹' U
[PROOFSTEP]
rcases hU with ⟨H, _, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup (L ≃ₐ[K] L)
left✝ : H ∈ fixedByFinite K L
⊢ (fun g => g.carrier) H ⊆ (fun x => x⁻¹) ⁻¹' (fun g => g.carrier) H
[PROOFSTEP]
exact fun _ => H.inv_mem'
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ∀ (x₀ : L ≃ₐ[K] L) {U : Set (L ≃ₐ[K] L)},
    U ∈ (galBasis K L).sets → ∃ V, V ∈ (galBasis K L).sets ∧ V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
[PROOFSTEP]
rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
⊢ ∃ V,
    V ∈ (galBasis K L).sets ∧ V ⊆ (fun x => σ * x * σ⁻¹) ⁻¹' (fun g => g.carrier) (IntermediateField.fixingSubgroup E)
[PROOFSTEP]
let F : IntermediateField K L := E.map σ.symm.toAlgHom
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
⊢ ∃ V,
    V ∈ (galBasis K L).sets ∧ V ⊆ (fun x => σ * x * σ⁻¹) ⁻¹' (fun g => g.carrier) (IntermediateField.fixingSubgroup E)
[PROOFSTEP]
refine' ⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, _, rfl⟩, rfl⟩, fun g hg => _⟩⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
⊢ F ∈ finiteExts K L
[PROOFSTEP]
have : FiniteDimensional K E := hE
[GOAL]
case intro.intro.intro.intro.refine'_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
this : FiniteDimensional K { x // x ∈ E }
⊢ F ∈ finiteExts K L
[PROOFSTEP]
apply im_finiteDimensional σ.symm
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
⊢ g ∈ (fun x => σ * x * σ⁻¹) ⁻¹' (fun g => g.carrier) (IntermediateField.fixingSubgroup E)
[PROOFSTEP]
change σ * g * σ⁻¹ ∈ E.fixingSubgroup
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
⊢ σ * g * σ⁻¹ ∈ IntermediateField.fixingSubgroup E
[PROOFSTEP]
rw [IntermediateField.mem_fixingSubgroup_iff]
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
⊢ ∀ (x : L), x ∈ E → ↑(σ * g * σ⁻¹) x = x
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑(σ * g * σ⁻¹) x = x
[PROOFSTEP]
change σ (g (σ⁻¹ x)) = x
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑σ (↑g (↑σ⁻¹ x)) = x
[PROOFSTEP]
have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp; rw [← AlgEquiv.invFun_eq_symm]; rfl⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑↑↑(AlgEquiv.symm σ) x = ↑σ⁻¹ x
[PROOFSTEP]
dsimp
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑(AlgEquiv.symm σ) x = ↑σ⁻¹ x
[PROOFSTEP]
rw [← AlgEquiv.invFun_eq_symm]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ Equiv.invFun σ.toEquiv x = ↑σ⁻¹ x
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
⊢ ↑σ (↑g (↑σ⁻¹ x)) = x
[PROOFSTEP]
have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x :=
  by
  rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg 
  exact hg (σ⁻¹ x) h_in_F
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
⊢ ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
[PROOFSTEP]
rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg 
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : ∀ (x : L), x ∈ F → ↑g x = x
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
⊢ ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
[PROOFSTEP]
exact hg (σ⁻¹ x) h_in_F
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
h_g_fix : ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
⊢ ↑σ (↑g (↑σ⁻¹ x)) = x
[PROOFSTEP]
rw [h_g_fix]
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
h_g_fix : ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
⊢ ↑σ (↑σ⁻¹ x) = x
[PROOFSTEP]
change σ (σ⁻¹ x) = x
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
h_g_fix : ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
⊢ ↑σ (↑σ⁻¹ x) = x
[PROOFSTEP]
exact AlgEquiv.apply_symm_apply σ x
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K { x // x ∈ E }
⊢ IsOpen ↑(fixingSubgroup E)
[PROOFSTEP]
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L := ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K { x // x ∈ E }
h_basis : (fixingSubgroup E).toSubmonoid.toSubsemigroup.carrier ∈ galGroupBasis K L
⊢ IsOpen ↑(fixingSubgroup E)
[PROOFSTEP]
have h_nhd := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K { x // x ∈ E }
h_basis : (fixingSubgroup E).toSubmonoid.toSubsemigroup.carrier ∈ galGroupBasis K L
h_nhd : (fixingSubgroup E).toSubmonoid.toSubsemigroup.carrier ∈ 𝓝 1
⊢ IsOpen ↑(fixingSubgroup E)
[PROOFSTEP]
exact Subgroup.isOpen_of_mem_nhds _ h_nhd
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let φ := f⁻¹ * g
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
cases' FunLike.exists_ne hfg with x hx
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
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
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ↑φ x ≠ x
[PROOFSTEP]
apply ne_of_apply_ne f
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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) ≠ ↑f x
[PROOFSTEP]
change f (f.symm (g x)) ≠ f x
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 (↑(AlgEquiv.symm f) (↑g x)) ≠ ↑f x
[PROOFSTEP]
rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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
[PROOFSTEP]
exact hx
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let E : IntermediateField K L := IntermediateField.adjoin K { x }
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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⟯
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let h_findim : FiniteDimensional K E := IntermediateField.adjoin.finiteDimensional (h_int x)
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let H := E.fixingSubgroup
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
have h_basis : (H : Set (L ≃ₐ[K] L)) ∈ galGroupBasis K L := ⟨H, ⟨E, ⟨h_findim, rfl⟩⟩, rfl⟩
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
have h_nhd := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
h_nhd : ↑H ∈ 𝓝 1
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
rw [mem_nhds_iff] at h_nhd 
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
h_nhd : ∃ t, t ⊆ ↑H ∧ IsOpen t ∧ 1 ∈ t
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
rcases h_nhd with ⟨W, hWH, hW_open, hW_1⟩
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
refine'
  ⟨leftCoset f W, leftCoset g W,
    ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, _⟩⟩
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ Disjoint (leftCoset f W) (leftCoset g W)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ ∀ ⦃a : L ≃ₐ[K] L⦄, a ∈ leftCoset f W → ¬a ∈ leftCoset g W
[PROOFSTEP]
rintro σ ⟨w1, hw1, h⟩ ⟨w2, hw2, rfl⟩
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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
[PROOFSTEP]
rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h 
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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
[PROOFSTEP]
have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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
[PROOFSTEP]
rw [h] at h_in_H 
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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 : f⁻¹ * g ∈ H
⊢ False
[PROOFSTEP]
change φ ∈ E.fixingSubgroup at h_in_H 
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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 : φ ∈ IntermediateField.fixingSubgroup E
⊢ False
[PROOFSTEP]
rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H 
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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 : L), x ∈ E → ↑φ x = x
⊢ False
[PROOFSTEP]
specialize h_in_H x
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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
[PROOFSTEP]
have hxE : x ∈ E := by
  apply IntermediateField.subset_adjoin
  apply Set.mem_singleton
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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 ∈ E
[PROOFSTEP]
apply IntermediateField.subset_adjoin
[GOAL]
case a
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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}
[PROOFSTEP]
apply Set.mem_singleton
[GOAL]
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
h_int : 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 { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
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
[PROOFSTEP]
exact hφx (h_in_H hxE)
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
⊢ IsTotallyDisconnected Set.univ
[PROOFSTEP]
apply isTotallyDisconnected_of_clopen_set
[GOAL]
case hX
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
⊢ Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
intro σ τ h_diff
[GOAL]
case hX
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne.def, inv_mul_eq_one]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
⊢ σ⁻¹ * τ ≠ 1
[PROOFSTEP]
rwa [Ne.def, inv_mul_eq_one]
[GOAL]
case hX
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
rcases FunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
let E := IntermediateField.adjoin K ({ x } : Set L)
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
haveI := IntermediateField.adjoin.finiteDimensional (h_int x)
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K { x_1 // x_1 ∈ K⟮x⟯ }
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
refine'
  ⟨leftCoset σ E.fixingSubgroup, ⟨E.fixingSubgroup_isOpen.leftCoset σ, E.fixingSubgroup_isClosed.leftCoset σ⟩,
    ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, _⟩
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K { x_1 // x_1 ∈ K⟮x⟯ }
⊢ ¬τ ∈ leftCoset σ ↑(IntermediateField.fixingSubgroup E)
[PROOFSTEP]
simp only [mem_leftCoset_iff, SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff, not_forall]
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K { x_1 // x_1 ∈ K⟮x⟯ }
⊢ ∃ x_1 x, ¬↑(σ⁻¹ * τ) x_1 = x_1
[PROOFSTEP]
exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
