-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem closure_smul₀ {E} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E]
    [ContinuousConstSMul G₀ E] (c : G₀) (s : Set E) : closure (c • s) = c • closure s

Proof state:
case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure 0 = 0

Tactic:
exact closure_singleton

Result:
no goals

Proof state:
case inl.inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure (0 • ∅) = 0 • closure ∅

Tactic:
simp

Result:
no goals

Proof state:
case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure (c • s) = c • closure s

Tactic:
exact closure_smul₀' hc s

Result:
no goals

Proof state:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
⊢ closure (0 • s) = 0 • closure s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Result:
case inl.inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure (0 • ∅) = 0 • closure ∅

case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure (0 • s) = 0 • closure s

Proof state:
case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure (0 • s) = 0 • closure s

Tactic:
rw [zero_smul_set hs, zero_smul_set hs.closure]

Result:
case inl.inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : s.Nonempty
⊢ closure 0 = 0

Proof state:
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
⊢ closure (c • s) = c • closure s

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Result:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
⊢ closure (0 • s) = 0 • closure s

case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure (c • s) = c • closure s