no goals
X : Type ?u.14903
α : Type u_3
α' : Type ?u.14909
β : Type u_2
γ : Type u_1
δ : Type ?u.14918
M : Type ?u.14921
E : Type ?u.14924
R : Type ?u.14927
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f
simp_rw [hasCompactMulSupport_def, mulSupport_comp_eq g (@hg) f]