-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem comap_boundedBy {β} (f : β → α)
    (h : (Monotone fun s : { s : Set α // s.Nonempty } => m s) ∨ Surjective f) :
    comap f (boundedBy m) = boundedBy fun s => m (f '' s)

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

Tactic:
congr with s : 1

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

Proof state:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : s.Nonempty
⊢ m s ≤ (fun s => ⨆ (_ : s.Nonempty), m s) t

Tactic:
have ht : t.Nonempty := hs.mono hst

Result:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : s.Nonempty
ht : t.Nonempty
⊢ m s ≤ (fun s => ⨆ (_ : s.Nonempty), m s) t

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

Tactic:
refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id

Result:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : s.Nonempty
⊢ m s ≤ (fun s => ⨆ (_ : s.Nonempty), m s) t

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ OuterMeasure.ofFunction (fun s => ⨆ (_ : (f '' s).Nonempty), m (f '' s)) ⋯ = boundedBy fun s => m (f '' s)

Tactic:
dsimp only [boundedBy]

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

Proof state:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
H : Monotone fun s => m ↑s
s t : Set α
hst : s ≤ t
hs : s.Nonempty
ht : t.Nonempty
⊢ m s ≤ (fun s => ⨆ (_ : s.Nonempty), m s) t

Tactic:
exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)

Result:
no goals

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

Tactic:
rw [image_nonempty]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s => m ↑s) ∨ Surjective f
⊢ (comap f) (boundedBy m) = boundedBy fun s => m (f '' s)

Tactic:
refine (comap_ofFunction _ ?_).trans ?_

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

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