α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ OuterMeasure.ofFunction (c • fun s => ⨆ (_ : Set.Nonempty s), m s) (_ : (c • ⨆ (_ : Set.Nonempty ∅), m ∅) = 0) =
    OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty s), (c • m) s) (_ : (⨆ (_ : Set.Nonempty ∅), (c • m) ∅) = 0)
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c • boundedBy m = boundedBy (c • m)
simp only [boundedBy , smul_ofFunction hc]
case e_m.h
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ (c • fun s => ⨆ (_ : Set.Nonempty s), m s) s = ⨆ (_ : Set.Nonempty s), (c • m) s
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ OuterMeasure.ofFunction (c • fun s => ⨆ (_ : Set.Nonempty s), m s) (_ : (c • ⨆ (_ : Set.Nonempty ∅), m ∅) = 0) =
    OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty s), (c • m) s) (_ : (⨆ (_ : Set.Nonempty ∅), (c • m) ∅) = 0)
congr 1 with s : 1
no goals
case e_m.h
α : Type u_1
m : Set α → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ (c • fun s => ⨆ (_ : Set.Nonempty s), m s) s = ⨆ (_ : Set.Nonempty s), (c • m) s
rcases s.eq_empty_or_nonempty with (rfl | hs) <;> simp [*]