-- Mathlib/Topology/Algebra/Monoid.lean
lemma GroupWithZero.isOpen_singleton_zero [GroupWithZero M] [TopologicalSpace M]
    [ContinuousMul M] [CompactSpace M] [T1Space M] :
    IsOpen {(0 : M)}

Proof state:
case pos
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen {0}

Tactic:
obtain ⟨x, hx, hxW⟩ := H

Result:
case pos.intro.intro
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ IsOpen {0}

Proof state:
case intro.intro.intro.intro.intro
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
⊢ IsOpen {0}

Tactic:
by_cases H : ∃ x ≠ 0, x ∈ W

Result:
case pos
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen {0}

case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen {0}

Proof state:
case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
hW : {0} ∈ 𝓝 0
hW' : univ * {0} ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ {0}
⊢ IsOpen {0}

Tactic:
simpa [isOpen_iff_mem_nhds]

Result:
no goals

Proof state:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ {0} ⊆ W

Tactic:
simpa using mem_of_mem_nhds hW

Result:
no goals

Proof state:
case pos.intro.intro
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ IsOpen {0}

Tactic:
cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))

Result:
no goals

Proof state:
case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ IsOpen {0}

Tactic:
obtain rfl : W = {0} := subset_antisymm
  (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)

Result:
case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
hW : {0} ∈ 𝓝 0
hW' : univ * {0} ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ {0}
⊢ IsOpen {0}

Proof state:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
x : M
hx : x ≠ 0
hxW : x ∈ W
⊢ 1 ∈ univ * W

Tactic:
simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW

Result:
no goals

Proof state:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ W
⊢ W ⊆ {0}

Tactic:
simpa [not_imp_not] using H

Result:
no goals

Proof state:
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
⊢ IsOpen {0}

Tactic:
obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one

Result:
case intro.intro.intro
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
⊢ IsOpen {0}

Proof state:
case intro.intro.intro
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
⊢ IsOpen {0}

Tactic:
obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)

Result:
case intro.intro.intro.intro.intro
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen U
h0U : 0 ∈ U
h1U : 1 ∉ U
W : Set M
hW : W ∈ 𝓝 0
hW' : univ * W ⊆ U
⊢ IsOpen {0}