case inl
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_1
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
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s✝ : Set β
E : Type u_1
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
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s✝ : Set β
E : Type u_1
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
rcases eq_or_ne c 0 with (rfl | hc)
case inl.inl
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
E : Type u_1
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure (0 • ∅) = 0 • closure ∅

case inl.inr
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_1
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : Set.Nonempty s
⊢ closure (0 • s) = 0 • closure s
case inl
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_1
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
rcases eq_empty_or_nonempty s with (rfl | hs)
no goals
case inl.inl
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s : Set β
E : Type u_1
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ closure (0 • ∅) = 0 • closure ∅
simp
case inl.inr
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_1
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : Set.Nonempty s
⊢ closure 0 = 0
case inl.inr
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_1
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : Set.Nonempty s
⊢ closure (0 • s) = 0 • closure s
rw [zero_smul_set hs, zero_smul_set hs.closure]
no goals
case inl.inr
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c : G₀
s✝ : Set β
E : Type u_1
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
hs : Set.Nonempty s
⊢ closure 0 = 0
exact closure_singleton
no goals
case inr
M : Type ?u.97023
α : Type ?u.97026
β : Type ?u.97029
G₀ : Type u_2
inst✝⁹ : TopologicalSpace α
inst✝⁸ : GroupWithZero G₀
inst✝⁷ : MulAction G₀ α
inst✝⁶ : ContinuousConstSMul G₀ α
inst✝⁵ : TopologicalSpace β
f : β → α
b : β
c✝ : G₀
s✝ : Set β
E : Type u_1
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
exact ((Homeomorph.smulOfNeZero c hc).image_closure s).symm