awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ ContinuousInv ℝ≥0∞

Tactic:
⟨OrderIso.invENNReal.continuous⟩

Premises used: OrderIso.invENNReal, OrderIso.continuous, ContinuousInv.mk
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
rsuffices : ∀ (N : Set M) (hN : Minimal (fun (x : Set M) ↦ x ∈ S) N), ∃ (m : M), m * m = m
rsuffices₁ : ∃ (N' : Set M), Minimal (fun (x : Set M) ↦ x ∈ S) N'
⊢ ∃ (m : M), m * m = m

Tactic:
rsuffices ⟨N, hN⟩ : ∃ N', Minimal (· ∈ S) N'
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
obtain : ∀ (N_closed : IsClosed N) (N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N) (m : M) (hm : m ∈ N), ∃ (m : M), m * m = m
⊢ ∃ (m : M), m * m = m

Tactic:
obtain ⟨N_closed, ⟨m, hm⟩, N_mul⟩ := hN.prop

Premises used: Minimal.prop
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
h : m * m = m
⊢ ∃ (m : M), m * m = m

Tactic:
use m
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
ht : (fun (x : M) ↦ x * m) '' N ∈ S
hts : (fun (x : M) ↦ x * m) '' N ⊆ N
⊢ (fun (x : M) ↦ x * m) '' N = N

Tactic:
apply hN.eq_of_subset

Premises used: Minimal.eq_of_subset
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun (x : M) ↦ x * m) '' N ∈ S

Tactic:
⟨(continuous_const_mul m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, ?_⟩

Premises used: Set.Mem, setOf, Continuous.isClosedMap, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
ht :
  ∀ (m_1 : M),
    Membership.mem (γ := Set M) ((fun (x : M) ↦ x * m) '' N) m_1 →
      ∀ (m' : M),
        Membership.mem (γ := Set M) ((fun (x : M) ↦ x * m) '' N) m' →
          Membership.mem (γ := Set M) ((fun (x : M) ↦ x * m) '' N) (m_1 * m')
⊢ (fun (x : M) ↦ x * m) '' N ∈ S

Tactic:
refine ⟨(continuous_const_mul m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, ?_⟩
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
m'' : M
hm'' : m'' ∈ N
m' : M
hm' : m' ∈ N
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x * m) '' N)
    (HMul.hMul (α := M) ((fun (x : M) ↦ x * m) m'') ((fun (x : M) ↦ x * m) m'))

Tactic:
⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩

Premises used: HMul.hMul, Set.Mem, mul_assoc, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
m'' : M
hm'' : m'' ∈ N
m' : M
hm' : m' ∈ N
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ x * m) '' N)
    (HMul.hMul (α := M) ((fun (x : M) ↦ x * m) m'') ((fun (x : M) ↦ x * m) m'))

Tactic:
exact ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun (x : M) ↦ x * m) m' ∈ N

Tactic:
N_mul _ hm' _ hm

Premises used: Set.Mem
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun (x : M) ↦ x * m) m' ∈ N

Tactic:
exact N_mul _ hm' _ hm
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun (x : M) ↦ x * m) '' N = N

Tactic:
have scaling_eq_self : (· * m) '' N = N := by
      apply hN.eq_of_subset
      · refine ⟨(continuous_const_mul m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, ?_⟩
        rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
        exact ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
      · rintro _ ⟨m', hm', rfl⟩
        exact N_mul _ hm' _ hm
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
ht : N ∩ {m' : M | m' * m = m} ∈ S
hts : N ∩ {m' : M | m' * m = m} ⊆ N
⊢ N ∩ {m' : M | m' * m = m} = N

Tactic:
apply hN.eq_of_subset

Premises used: Minimal.eq_of_subset
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
⊢ N ∩ {m' : M | m' * m = m} ∈ S

Tactic:
⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_const_mul m)), ?_, ?_⟩

Premises used: Set.Mem, setOf, T1Space.t1, And.intro, IsClosed.preimage, IsClosed.inter
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
ht : (N ∩ {m' : M | m' * m = m}).Nonempty
ht₁ : ∀ m_1 ∈ N ∩ {m' : M | m' * m = m}, ∀ m' ∈ N ∩ {m' : M | m' * m = m}, m_1 * m' ∈ N ∩ {m' : M | m' * m = m}
⊢ N ∩ {m' : M | m' * m = m} ∈ S

Tactic:
refine ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_const_mul m)), ?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
ht ht₁ ht₂ ht₃ :
  ∀ (hm : Membership.mem (γ := Set M) ((fun (x : M) ↦ x * m) '' N) m)
    (scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N), (N ∩ {m' : M | m' * m = m}).Nonempty
⊢ (N ∩ {m' : M | m' * m = m}).Nonempty

Tactic:
rwa [← scaling_eq_self] at hm
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ 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 = m}

Tactic:
⟨N_mul _ mem'' _ mem', ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
ht : Membership.mem (γ := Set M) {m' : M | m' * m = m} (m'' * m')
⊢ m'' * m' ∈ N ∩ {m' : M | m' * m = m}

Tactic:
refine ⟨N_mul _ mem'' _ mem', ?_⟩
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
ht : m'' * m' * m = m
ht₁ : m'' * (m' * m) = m
ht₂ : m'' * m = m
ht₃ ht₄ : m = m
⊢ Membership.mem (γ := Set M) {m' : M | m' * m = m} (m'' * m')

Tactic:
rw [Set.mem_setOf_eq, mul_assoc, eq', eq'']

Premises used: mul_assoc, Set.mem_setOf_eq
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
⊢ N ∩ {m' : M | m' * m = m} ⊆ N

Tactic:
apply Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
⊢ N ∩ {m' : M | m' * m = m} = N

Tactic:
have absorbing_eq_self : N ∩ { m' | m' * m = m } = N := by
      apply hN.eq_of_subset
      · refine ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_const_mul 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
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' : M | m' * m = m} = N
⊢ m ∈ N ∩ {m' : M | m' * m = m}

Tactic:
rw [← absorbing_eq_self] at hm
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' : M | m' * m = m} = N
hm₁ : m ∈ N ∩ {m' : M | m' * m = m}
⊢ (fun (x : M) ↦ x * m) '' N = N

Tactic:
rw [← absorbing_eq_self] at hm
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' : M | m' * m = m} = N
hm₁ : m ∈ N ∩ {m' : M | m' * m = m}
scaling_eq_self₁ : (fun (x : M) ↦ x * m) '' N = N
⊢ N ∩ {m' : M | m' * m = m} = N

Tactic:
rw [← absorbing_eq_self] at hm
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' : M | m' * m = m}
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' : M | m' * m = m} = N
⊢ m * m = m

Tactic:
hm.2

Premises used: Set.Mem, setOf, And.right
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
N : Set M
hN : Minimal (fun (x : Set M) ↦ x ∈ S) N
N_closed : IsClosed N
N_mul : ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' : M | m' * m = m}
scaling_eq_self : (fun (x : M) ↦ x * m) '' N = N
absorbing_eq_self : N ∩ {m' : M | m' * m = m} = N
⊢ m * m = m

Tactic:
exact hm.2

Premises used: And.right
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
⊢ ∃ (N' : Set M), Minimal (fun (x : Set M) ↦ x ∈ S) N'

Tactic:
zorn_superset _ fun c hcs hc => ?_

Premises used: zorn_superset
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
refine : ∀ (c : Set (Set M)) (hcs : c ⊆ S) (hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c), ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s
⊢ ∃ (N' : Set M), Minimal (fun (x : Set M) ↦ x ∈ S) N'

Tactic:
refine zorn_superset _ fun c hcs hc => ?_

Premises used: zorn_superset
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
⊢ ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s

Tactic:
⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, ?_, fun m hm m' hm' => ?_⟩, fun s hs =>
      Set.sInter_subset_of_mem hs⟩

Premises used: Set.sInter_subset_of_mem, And.left, And.intro, isClosed_sInter, Exists.intro, Set.sInter
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
refine_1 : (⋂₀ c).Nonempty
refine_2 : ∀ (m : M) (hm : m ∈ ⋂₀ c) (m' : M) (hm' : m' ∈ ⋂₀ c), m * m' ∈ ⋂₀ c
⊢ ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s

Tactic:
refine
    ⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, ?_, fun m hm m' hm' => ?_⟩, fun s hs =>
      Set.sInter_subset_of_mem hs⟩
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
refine_1 : ∀ (hcs : ∅ ⊆ S) (hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) ∅), Set.Nonempty.{u_1} (α := M) (⋂₀ ∅)
refine_1₁ : ∀ (hcnemp : c.Nonempty), (⋂₀ c).Nonempty
⊢ (⋂₀ c).Nonempty

Tactic:
obtain rfl | hcnemp := c.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) ∅
refine_1 : Set.Nonempty.{u_1} (α := M) Set.univ
⊢ Set.Nonempty.{u_1} (α := M) (⋂₀ ∅)

Tactic:
rw [Set.sInter_empty]

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) ∅
⊢ Set.Nonempty.{u_1} (α := M) Set.univ

Tactic:
apply Set.univ_nonempty

Premises used: Set.univ_nonempty
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ Set.Nonempty.{u_1} (α := M) (⋂ (i : (↑c : Type u_1)), (↑i : Set M))

Tactic:
@IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, Subtype.val
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
h : ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)
refine_1 : Directed (ι := (↑c : Type u_1)) (fun (x1 x2 : Set M) ↦ x1 ⊇ x2) (Subtype.val (p := fun (x : Set M) ↦ x ∈ c))
refine_1₁ : ∀ (i : (↑c : Type u_1)), (↑i : Set M).Nonempty
refine_1₂ : ∀ (i : (↑c : Type u_1)), IsCompact (↑i : Set M)
refine_1₃ : ∀ (i : (↑c : Type u_1)), IsClosed (↑i : Set M)
⊢ (⋂₀ c).Nonempty

Tactic:
convert!
      @IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ _ _ hcnemp.coe_sort
        ((↑) : c → Set M) ?_ ?_ ?_ ?_

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, Subtype.val
-- Module: Mathlib.Topology.Algebra.Semigroup
Goal:
M : Type u_1
inst : Nonempty M
inst_1 : Semigroup M
inst_2 : TopologicalSpace M
inst_3 : CompactSpace M
inst_4 : T2Space M
continuous_const_mul : ∀ (r : M), Continuous (Y := M) fun (x : M) ↦ x * r
S : Set (Set M) := {N : Set M | IsClosed N ∧ N.Nonempty ∧ ∀ m ∈ N, ∀ m' ∈ N, m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun (x1 x2 : Set M) ↦ x1 ⊆ x2) c
hcnemp : c.Nonempty
⊢ ⋂₀ c = ⋂ (i : (↑c : Type u_1)), (↑i : Set M)

Tactic:
Set.sInter_eq_iInter

Premises used: Set.sInter_eq_iInter