-- Mathlib/Algebra/Group/Submonoid/Basic.lean
/-- The `Submonoid.closure` of a set is the union of `{1}` and its `Subsemigroup.closure`. -/
lemma closure_eq_one_union (s : Set M) :
    closure s = {(1 : M)} ∪ (Subsemigroup.closure s : Set M)

Proof state:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x = 1

Tactic:
simpa using hx

Result:
no goals

Proof state:
case a.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x ∈ {1} ∪ ↑(Subsemigroup.closure s)
hy : hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)
⊢ x * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
simp only [singleton_union, mem_insert_iff, SetLike.mem_coe] at hx hy

Result:
case a.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x = 1 ∨ x ∈ Subsemigroup.closure s
hy : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
⊢ x * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Proof state:
case a.mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x = 1 ∨ x ∈ Subsemigroup.closure s
hy : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
⊢ x * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy

Result:
case a.mul.intro.inl.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ 1 * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.intro.inl.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x hx✝ : M
hy✝¹ : hx✝ ∈ closure s
hy✝ : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ 1 * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.intro.inr.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
y : x ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ x * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.intro.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝¹ : M
y : x ∈ closure s
hy✝¹ : hx✝¹ ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hy✝ : hx✝¹ = 1 ∨ hx✝¹ ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝¹ ∈ Subsemigroup.closure s
⊢ x * hx✝¹ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Proof state:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ≤ ↑(closure s)

Tactic:
rintro x (hx | hx)

Result:
case a.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x ∈ ↑(closure s)

case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)

Proof state:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ≤ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
intro x hx

Result:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Proof state:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) = {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
apply le_antisymm

Result:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ≤ {1} ∪ ↑(Subsemigroup.closure s)

case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ {1} ∪ ↑(Subsemigroup.closure s) ≤ ↑(closure s)

Proof state:
case a.mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
hx : x ∈ s
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
exact Or.inr <| Subsemigroup.subset_closure hx

Result:
no goals

Proof state:
case a.mul.intro.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝¹ : M
y : x ∈ closure s
hy✝¹ : hx✝¹ ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hy✝ : hx✝¹ = 1 ∨ hx✝¹ ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝¹ ∈ Subsemigroup.closure s
⊢ x * hx✝¹ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
simp_all

Result:
case a.mul.intro.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ x * hx✝ = 1 ∨ x * hx✝ ∈ Subsemigroup.closure s

Proof state:
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ 1 ∈ {1}

Tactic:
simp

Result:
no goals

Proof state:
case a.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x ∈ ↑(closure s)

Tactic:
exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)

Result:
no goals

Proof state:
case a.mul.intro.inl.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ 1 * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.intro.inl.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x hx✝ : M
hy✝¹ : hx✝ ∈ closure s
hy✝ : hx✝ = 1 ∨ hx✝ ∈ Subsemigroup.closure s
y : 1 ∈ closure s
hx : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ 1 * hx✝ ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.intro.inr.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
y : x ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy✝ : 1 ∈ closure s
hy : 1 = 1 ∨ 1 ∈ Subsemigroup.closure s
⊢ x * 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

case a.mul.intro.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝¹ : M
y : x ∈ closure s
hy✝¹ : hx✝¹ ∈ closure s
hx✝ : x = 1 ∨ x ∈ Subsemigroup.closure s
hy✝ : hx✝¹ = 1 ∨ hx✝¹ ∈ Subsemigroup.closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝¹ ∈ Subsemigroup.closure s
⊢ x * hx✝¹ ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
all_goals simp_all

Result:
case a.mul.intro.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ x * hx✝ = 1 ∨ x * hx✝ ∈ Subsemigroup.closure s

Proof state:
case a.mul.intro.inr.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x hx✝ : M
y : x ∈ closure s
hy✝ : hx✝ ∈ closure s
hx : x ∈ Subsemigroup.closure s
hy : hx✝ ∈ Subsemigroup.closure s
⊢ x * hx✝ = 1 ∨ x * hx✝ ∈ Subsemigroup.closure s

Tactic:
exact Or.inr <| mul_mem hx hy

Result:
no goals

Proof state:
case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)

Tactic:
exact Subsemigroup.closure_le.mpr subset_closure hx

Result:
no goals

Proof state:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
induction hx using closure_induction with
| mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
| one => exact Or.inl <| by simp
| mul x hx y hy hx hy =>
  simp only [singleton_union, mem_insert_iff, SetLike.mem_coe] at hx hy
  obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
  all_goals simp_all
  exact Or.inr <| mul_mem hx hy

Result:
no goals

Proof state:
case a.one
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
exact Or.inl <| by simp

Result:
no goals