no goals
α✝ : Type ?u.236514
β✝ : Type ?u.236517
γ : Type ?u.236520
ι : Type ?u.236523
inst✝² : Countable ι
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(OfNat.ofNat 0 n)) < ⊤
simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero', measure_empty,
  WithTop.zero_lt_top, forall_const]