α : Type ?u.151922
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.152165
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0
α : Type ?u.151922
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.152165
f : β → α
h : Monotone m ∨ Surjective f
⊢ (fun s => m (f '' s)) ∅ = 0
simp
no goals
α : Type ?u.151922
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type ?u.152165
f : β → α
h : Monotone m ∨ Surjective f
⊢ m ∅ = 0
simp [m_empty]
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ↑(↑(comap f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f '' s)

case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ↑(OuterMeasure.ofFunction (fun s => m (f '' s)) (_ : (fun s => m (f '' s)) ∅ = 0)) s ≤
    ↑(↑(comap f) (OuterMeasure.ofFunction m m_empty)) s
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
⊢ ↑(comap f) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun s => m (f '' s)) (_ : (fun s => m (f '' s)) ∅ = 0)
refine' le_antisymm (le_ofFunction.2 fun s => _) fun s => _
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ↑(OuterMeasure.ofFunction m m_empty) (f '' s) ≤ m (f '' s)
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ↑(↑(comap f) (OuterMeasure.ofFunction m m_empty)) s ≤ m (f '' s)
rw [comap_apply]
no goals
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ↑(OuterMeasure.ofFunction m m_empty) (f '' s) ≤ m (f '' s)
apply ofFunction_le
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n)) ≤
    ⨅ (t : ℕ → Set α) (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ ↑(OuterMeasure.ofFunction (fun s => m (f '' s)) (_ : (fun s => m (f '' s)) ∅ = 0)) s ≤
    ↑(↑(comap f) (OuterMeasure.ofFunction m m_empty)) s
rw [comap_apply, ofFunction_apply, ofFunction_apply]
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
⊢ (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f '' t n)) ≤
    ⨅ (t : ℕ → Set α) (_ : f '' s ⊆ iUnion t), ∑' (n : ℕ), m (t n)
refine' iInf_mono' fun t => ⟨fun k => f ⁻¹' t k, _⟩
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ i, (∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n)) ≤ ∑' (n : ℕ), m (t n)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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)
refine' iInf_mono' fun ht => _
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
⊢ ∃ i, (∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n)) ≤ ∑' (n : ℕ), m (t n)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : f '' s ⊆ iUnion t
⊢ ∃ i, (∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n)) ≤ ∑' (n : ℕ), m (t n)
rw [Set.image_subset_iff, preimage_iUnion] at ht
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : β → α
h : Monotone m ∨ Surjective f
s : Set β
t : ℕ → Set α
ht : s ⊆ ⋃ (i : ℕ), f ⁻¹' t i
⊢ ∃ i, (∑' (n : ℕ), m (f '' (fun k => f ⁻¹' t k) n)) ≤ ∑' (n : ℕ), m (t n)
refine' ⟨ht, ENNReal.tsum_le_tsum fun n => _⟩
case refine'_2.inl
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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)
cases' h with hl hr
no goals
case refine'_2.inl
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
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)
exacts [hl (image_preimage_subset _ _), (congr_arg m (hr.image_preimage (t n))).le]