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
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
let M' := { m // m ∈ s }
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
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
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 _ _ _) }
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
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
haveI : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
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
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
haveI : Nonempty M' := nonempty_subtype.mpr snemp
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
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
obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this
no goals
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
exact ⟨m, hm, Subtype.ext_iff.mp idem⟩