M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ m, m * m = m
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
⊢ ∃ m, m * m = m
let S : Set (Set M) :=
  { N | IsClosed N ∧ N.Nonempty ∧ ∀ (m) (_ : m ∈ N) (m') (_ : m' ∈ N), m * m' ∈ N }
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ N, N ∈ S ∧ ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N

case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∃ m, m * m = m
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ m, m * m = m
obtain ⟨N, ⟨N_closed, ⟨m, hm⟩, N_mul⟩, N_minimal⟩ : ∃ N ∈ S, ∀ N' ∈ S, N' ⊆ N → N' = N
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∃ m, m * m = m

M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ N, N ∈ S ∧ ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ N, N ∈ S ∧ ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N

case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∃ m, m * m = m
rotate_left
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set M), s ∈ c → lb ⊆ s
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ N, N ∈ S ∧ ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
refine' zorn_superset _ fun c hcs hc => _
case refine'_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Set.Nonempty (⋂₀ c)

case refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ m * m' ∈ ⋂₀ c
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set M), s ∈ c → lb ⊆ s
refine'
  ⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, _, fun m hm m' hm' => _⟩, fun s hs =>
    Set.sInter_subset_of_mem hs⟩
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ m * m = m
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∃ m, m * m = m
use m
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' | m' * m = m}
scaling_eq_self : (fun x => x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
rw [← absorbing_eq_self] at hm
no goals
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' | m' * m = m}
scaling_eq_self : (fun x => x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
exact hm.2
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N ∈ S

case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N ⊆ N
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N = N
apply N_minimal
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∀ (m_1 : M), m_1 ∈ (fun x => x * m) '' N → ∀ (m' : M), m' ∈ (fun x => x * m) '' N → m_1 * m' ∈ (fun x => x * m) '' N
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N ∈ S
refine' ⟨(continuous_mul_left m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, _⟩
case a.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
m'' : M
hm'' : m'' ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x => x * m) m'' * (fun x => x * m) m' ∈ (fun x => x * m) '' N
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∀ (m_1 : M), m_1 ∈ (fun x => x * m) '' N → ∀ (m' : M), m' ∈ (fun x => x * m) '' N → m_1 * m' ∈ (fun x => x * m) '' N
rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
no goals
case a.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
m'' : M
hm'' : m'' ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x => x * m) m'' * (fun x => x * m) m' ∈ (fun x => x * m) '' N
refine' ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
case a.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x => x * m) m' ∈ N
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N ⊆ N
rintro _ ⟨m', hm', rfl⟩
no goals
case a.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x => x * m) m' ∈ N
exact N_mul _ hm' _ hm
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ∈ S

case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ⊆ N
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} = N
apply N_minimal
no goals
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ⊆ N
apply Set.inter_subset_left
case a.refine'_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ Set.Nonempty (N ∩ {m' | m' * m = m})

case a.refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ ∀ (m_1 : M), m_1 ∈ N ∩ {m' | m' * m = m} → ∀ (m' : M), m' ∈ N ∩ {m' | m' * m = m} → m_1 * m' ∈ N ∩ {m' | m' * m = m}
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ∈ S
refine' ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_mul_left m)), _, _⟩
no goals
case a.refine'_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ Set.Nonempty (N ∩ {m' | m' * m = m})
rwa [← scaling_eq_self] at hm
case a.refine'_2.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ N ∩ {m' | m' * m = m}
case a.refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ ∀ (m_1 : M), m_1 ∈ N ∩ {m' | m' * m = m} → ∀ (m' : M), m' ∈ N ∩ {m' | m' * m = m} → m_1 * m' ∈ N ∩ {m' | m' * m = m}
rintro m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩
case a.refine'_2.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ {m' | m' * m = m}
case a.refine'_2.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ N ∩ {m' | m' * m = m}
refine' ⟨N_mul _ mem'' _ mem', _⟩
no goals
case a.refine'_2.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ {m' | m' * m = m}
rw [Set.mem_setOf_eq, mul_assoc, eq', eq'']
case refine'_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ Set.Nonempty (⋂₀ ∅)

case refine'_1.inr
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ Set.Nonempty (⋂₀ c)
case refine'_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Set.Nonempty (⋂₀ c)
obtain rfl | hcnemp := c.eq_empty_or_nonempty
case h.e'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ⋂₀ c = ⋂ (i : ↑c), ↑i

case refine'_1.inr.convert_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ Directed (fun x x_1 => x ⊇ x_1) Subtype.val

case refine'_1.inr.convert_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), Set.Nonempty ↑i

case refine'_1.inr.convert_3
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), IsCompact ↑i

case refine'_1.inr.convert_4
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), IsClosed ↑i
case refine'_1.inr
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ Set.Nonempty (⋂₀ c)
convert
  @IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ _ _ hcnemp.coe_sort
    ((↑) : c → Set M) ?_ ?_ ?_ ?_
no goals
case refine'_1.inr.convert_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), Set.Nonempty ↑i

case refine'_1.inr.convert_3
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), IsCompact ↑i

case refine'_1.inr.convert_4
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), IsClosed ↑i
exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1]
case refine'_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ Set.Nonempty Set.univ
case refine'_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ Set.Nonempty (⋂₀ ∅)
rw [Set.sInter_empty]
no goals
case refine'_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ Set.Nonempty Set.univ
apply Set.univ_nonempty
case h.e'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ⋂₀ c = ⋂ (i : ↑c), ↑i
case h.e'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ⋂₀ c = ⋂ (i : ↑c), ↑i
simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq]
no goals
case h.e'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ⋂₀ c = ⋂ (i : ↑c), ↑i
exact Set.sInter_eq_iInter
no goals
case refine'_1.inr.convert_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ Directed (fun x x_1 => x ⊇ x_1) Subtype.val
refine' DirectedOn.directed_val (IsChain.directedOn hc.symm)
case refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ ∀ (t : Set M), t ∈ c → m * m' ∈ t
case refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ m * m' ∈ ⋂₀ c
rw [Set.mem_sInter]
no goals
case refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ ∀ (t : Set M), t ∈ c → m * m' ∈ t
exact fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht)