[GOAL]
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
[PROOFSTEP]
let S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ (m) (_ : m ∈ N) (m') (_ : m' ∈ N), m * m' ∈ N}
[GOAL]
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
[PROOFSTEP]
obtain ⟨N, ⟨N_closed, ⟨m, hm⟩, N_mul⟩, N_minimal⟩ : ∃ N ∈ S, ∀ N' ∈ S, N' ⊆ N → N' = N
[GOAL]
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
[PROOFSTEP]
rotate_left
  -- Porting note: restore to `rsuffices`
[GOAL]
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
[PROOFSTEP]
use m
[GOAL]
case h
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
[PROOFSTEP]
have scaling_eq_self : (· * m) '' N = N := by
  apply N_minimal
  · refine' ⟨(continuous_mul_left m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, _⟩
    rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
    refine' ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
  · rintro _ ⟨m', hm', rfl⟩
    exact N_mul _ hm' _ hm
[GOAL]
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
[PROOFSTEP]
apply N_minimal
[GOAL]
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
[PROOFSTEP]
refine' ⟨(continuous_mul_left m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, _⟩
[GOAL]
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
[PROOFSTEP]
rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
[GOAL]
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
[PROOFSTEP]
rintro _ ⟨m', hm', rfl⟩
[GOAL]
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
[PROOFSTEP]
exact N_mul _ hm' _ hm
[GOAL]
case h
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 = m
[PROOFSTEP]
have absorbing_eq_self : N ∩ {m' | m' * m = m} = N :=
  by
  apply N_minimal
  · refine' ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_mul_left m)), _, _⟩
    · rwa [← scaling_eq_self] at hm 
    · rintro m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩
      refine' ⟨N_mul _ mem'' _ mem', _⟩
      rw [Set.mem_setOf_eq, mul_assoc, eq', eq'']
  apply Set.inter_subset_left
[GOAL]
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
[PROOFSTEP]
apply N_minimal
[GOAL]
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
[PROOFSTEP]
refine' ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_mul_left m)), _, _⟩
[GOAL]
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})
[PROOFSTEP]
rwa [← scaling_eq_self] at hm 
[GOAL]
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}
[PROOFSTEP]
rintro m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩
[GOAL]
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}
[PROOFSTEP]
refine' ⟨N_mul _ mem'' _ mem', _⟩
[GOAL]
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}
[PROOFSTEP]
rw [Set.mem_setOf_eq, mul_assoc, eq', eq'']
[GOAL]
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
[PROOFSTEP]
apply Set.inter_subset_left
[GOAL]
case h
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
[PROOFSTEP]
rw [← absorbing_eq_self] at hm 
[GOAL]
case h
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
[PROOFSTEP]
exact hm.2
[GOAL]
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
[PROOFSTEP]
refine' zorn_superset _ fun c hcs hc => _
[GOAL]
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
[PROOFSTEP]
refine'
  ⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, _, fun m hm m' hm' => _⟩, fun s hs => Set.sInter_subset_of_mem hs⟩
[GOAL]
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)
[PROOFSTEP]
obtain rfl | hcnemp := c.eq_empty_or_nonempty
[GOAL]
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 (⋂₀ ∅)
[PROOFSTEP]
rw [Set.sInter_empty]
[GOAL]
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
[PROOFSTEP]
apply Set.univ_nonempty
[GOAL]
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)
[PROOFSTEP]
convert
  @IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ _ _ hcnemp.coe_sort ((↑) : c → Set M) ?_ ?_ ?_ ?_
[GOAL]
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
[PROOFSTEP]
exact Set.sInter_eq_iInter
[GOAL]
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
[PROOFSTEP]
refine' DirectedOn.directed_val (IsChain.directedOn hc.symm)
[GOAL]
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
[PROOFSTEP]
exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1]
[GOAL]
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
[PROOFSTEP]
rw [Set.mem_sInter]
[GOAL]
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
[PROOFSTEP]
exact fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht)
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
let M' := { m // m ∈ s }
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
letI : Semigroup M' :=
  { mul := fun p q => ⟨p.1 * q.1, s_add _ p.2 _ q.2⟩
    mul_assoc := fun p q r => Subtype.eq (mul_assoc _ _ _) }
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
haveI : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝ : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this : CompactSpace M'
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
haveI : Nonempty M' := nonempty_subtype.mpr snemp
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝¹ : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this✝ : CompactSpace M'
this : Nonempty M'
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
have : ∀ p : M', Continuous (· * p) := fun p => ((continuous_mul_left p.1).comp continuous_subtype_val).subtype_mk _
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝² : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x => x * p
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this
[GOAL]
case intro.mk
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝² : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x => x * p
m : M
hm : m ∈ s
idem : { val := m, property := hm } * { val := m, property := hm } = { val := m, property := hm }
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
exact ⟨m, hm, Subtype.ext_iff.mp idem⟩
