case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ (Monotone fun s => ⨆ (_ : Set.Nonempty s), m s) ∨ Surjective f

case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty (f '' s)), m (f '' s))
      (_ : (fun s => ⨆ (_ : Set.Nonempty (f '' s)), m (f '' s)) ∅ = 0) =
    boundedBy fun s => m (f '' s)
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ ↑(comap f) (boundedBy m) = boundedBy fun s => m (f '' s)
refine' (comap_ofFunction _ _).trans _
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : Set.Nonempty s
⊢ m s ≤ (fun s => ⨆ (_ : Set.Nonempty s), m s) t
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ (Monotone fun s => ⨆ (_ : Set.Nonempty s), m s) ∨ Surjective f
refine' h.imp (fun H s t hst => iSup_le fun hs => _) id
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ m s ≤ (fun s => ⨆ (_ : Set.Nonempty s), m s) t
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : Set.Nonempty s
⊢ m s ≤ (fun s => ⨆ (_ : Set.Nonempty s), m s) t
have ht : t.Nonempty := hs.mono hst
no goals
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : Set.Nonempty s
ht : Set.Nonempty t
⊢ m s ≤ (fun s => ⨆ (_ : Set.Nonempty s), m s) t
exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty (f '' s)), m (f '' s))
      (_ : (⨆ (_ : Set.Nonempty (f '' ∅)), m (f '' ∅)) = 0) =
    OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty s), m (f '' s)) (_ : (⨆ (_ : Set.Nonempty ∅), m (f '' ∅)) = 0)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty (f '' s)), m (f '' s))
      (_ : (fun s => ⨆ (_ : Set.Nonempty (f '' s)), m (f '' s)) ∅ = 0) =
    boundedBy fun s => m (f '' s)
dsimp only [boundedBy]
case refine'_2.e_m.h
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
s : Set β
⊢ (⨆ (_ : Set.Nonempty (f '' s)), m (f '' s)) = ⨆ (_ : Set.Nonempty s), m (f '' s)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty (f '' s)), m (f '' s))
      (_ : (⨆ (_ : Set.Nonempty (f '' ∅)), m (f '' ∅)) = 0) =
    OuterMeasure.ofFunction (fun s => ⨆ (_ : Set.Nonempty s), m (f '' s)) (_ : (⨆ (_ : Set.Nonempty ∅), m (f '' ∅)) = 0)
congr with s : 1
no goals
case refine'_2.e_m.h
α : Type u_2
m : Set α → ℝ≥0∞
β : Type u_1
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
s : Set β
⊢ (⨆ (_ : Set.Nonempty (f '' s)), m (f '' s)) = ⨆ (_ : Set.Nonempty s), m (f '' s)
rw [nonempty_image_iff]