-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem comap_ofFunction {β} (f : β → α) (h : Monotone m ∨ Surjective f) :
    comap f (OuterMeasure.ofFunction m m_empty) =
      OuterMeasure.ofFunction (fun s => m (f '' s)) (by simp; simp [m_empty])

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
⊢ ⨅ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n) ≤
    ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)

Tactic:
refine iInf_mono' fun ht => ?_

Result:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
rw [Set.image_subset_iff, preimage_iUnion] at ht

Result:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.27838
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0

Tactic:
simp [m_empty]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty) (f '' s) ≤ m (f '' s)

Tactic:
apply ofFunction_le

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.27838
f : β → α
h : Monotone m ∨ Surjective f
⊢ (fun s => m (f '' s)) ∅ = 0

Tactic:
simp

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.27838
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0

Proof state:
case refine_2.inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hl : Monotone m
⊢ m (f '' (fun k => f ⁻¹' t k) n) ≤ m (t n)

case refine_2.inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hr : Surjective f
⊢ m (f '' (fun k => f ⁻¹' t k) n) ≤ m (t n)

Tactic:
exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
⊢ ∃ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
refine ⟨ht, ENNReal.tsum_le_tsum fun n => ?_⟩

Result:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
⊢ m (f '' (fun k => f ⁻¹' t k) n) ≤ m (t n)

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n) ≤ ⨅ t, ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)

Tactic:
refine iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, ?_⟩

Result:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
⊢ ⨅ (_ : s ⊆ ⋃ k, f ⁻¹' t k), ∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n) ≤
    ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
⊢ m (f '' (fun k => f ⁻¹' t k) n) ≤ m (t n)

Tactic:
rcases h with hl | hr

Result:
case refine_2.inl
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hl : Monotone m
⊢ m (f '' (fun k => f ⁻¹' t k) n) ≤ m (t n)

case refine_2.inr
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hr : Surjective f
⊢ m (f '' (fun k => f ⁻¹' t k) n) ≤ m (t n)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
⊢ (comap f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯

Tactic:
refine le_antisymm (le_ofFunction.2 fun s => ?_) fun s => ?_

Result:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ((comap f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f '' s)

case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯) s ≤ ((comap f) (OuterMeasure.ofFunction m m_empty)) s

Proof state:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ((comap f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f '' s)

Tactic:
rw [comap_apply]

Result:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction m m_empty) (f '' s) ≤ m (f '' s)

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯) s ≤ ((comap f) (OuterMeasure.ofFunction m m_empty)) s

Tactic:
rw [comap_apply, ofFunction_apply, ofFunction_apply]

Result:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n) ≤ ⨅ t, ⨅ (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)