α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
⊢ ↑(OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty) s ≤ ↑(↑(map f) (OuterMeasure.ofFunction m m_empty)) s
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
⊢ ↑(map f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty
refine' (map_ofFunction_le _).antisymm fun s => _
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
⊢ ∀ (i : ℕ → Set α),
    f ⁻¹' s ⊆ iUnion i → (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) ≤ ∑' (n : ℕ), m (i n)
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
⊢ ↑(OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty) s ≤ ↑(↑(map f) (OuterMeasure.ofFunction m m_empty)) s
simp only [ofFunction_apply, map_apply, le_iInf_iff]
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) ≤ ∑' (n : ℕ), m (t n)
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
⊢ ∀ (i : ℕ → Set α),
    f ⁻¹' s ⊆ iUnion i → (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) ≤ ∑' (n : ℕ), m (i n)
intro t ht
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ (n : ℕ), range fᶜ ∪ f '' t n

case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ (∑' (n : ℕ), m (f ⁻¹' (fun n => range fᶜ ∪ f '' t n) n)) ≤ ∑' (n : ℕ), m (t n)
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n)) ≤ ∑' (n : ℕ), m (t n)
refine' iInf_le_of_le (fun n => range fᶜ ∪ f '' t n) (iInf_le_of_le _ _)
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ f '' (f ⁻¹' s) ⊆ f '' ⋃ (i : ℕ), t i
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ (n : ℕ), range fᶜ ∪ f '' t n
rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]
no goals
case refine'_1
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ f '' (f ⁻¹' s) ⊆ f '' ⋃ (i : ℕ), t i
exact image_subset _ ht
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
⊢ m (f ⁻¹' (fun n => range fᶜ ∪ f '' t n) n) = m (t n)
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ (∑' (n : ℕ), m (f ⁻¹' (fun n => range fᶜ ∪ f '' t n) n)) ≤ ∑' (n : ℕ), m (t n)
refine' ENNReal.tsum_le_tsum fun n => le_of_eq _
no goals
case refine'_2
α : Type u_2
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_1
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
⊢ m (f ⁻¹' (fun n => range fᶜ ∪ f '' t n) n) = m (t n)
simp [hf.preimage_image]