α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
⊢ ↑(⨅ (i : ι), ↑(map f) (↑(comap f) (m i))) s ≤ ↑(↑(map f) (⨅ (i : ι), ↑(comap f) (m i))) s
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
⊢ ↑(map f) (⨅ (i : ι), ↑(comap f) (m i)) = ⨅ (i : ι), ↑(map f) (↑(comap f) (m i))
refine' (map_iInf_le _ _).antisymm fun s => _
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
⊢ ∀ (i : ℕ → Set α),
    f ⁻¹' s ⊆ iUnion i →
      (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' (f ⁻¹' t n))) ≤
        ∑' (n : ℕ), ⨅ (i_2 : ι), ↑(m i_2) (f '' i n)
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
⊢ ↑(⨅ (i : ι), ↑(map f) (↑(comap f) (m i))) s ≤ ↑(↑(map f) (⨅ (i : ι), ↑(comap f) (m i))) s
simp only [map_apply, comap_apply, iInf_apply, le_iInf_iff]
case refine'_1
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ (n : ℕ), f '' t n ∪ range fᶜ

case refine'_2
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ (∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' (f ⁻¹' (fun n => f '' t n ∪ range fᶜ) n))) ≤
    ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' t n)
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
⊢ ∀ (i : ℕ → Set α),
    f ⁻¹' s ⊆ iUnion i →
      (⨅ (t : ℕ → Set β) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' (f ⁻¹' t n))) ≤
        ∑' (n : ℕ), ⨅ (i_2 : ι), ↑(m i_2) (f '' i n)
refine' fun t ht => iInf_le_of_le (fun n => f '' t n ∪ range fᶜ) (iInf_le_of_le _ _)
case refine'_1
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ f '' (f ⁻¹' s) ⊆ f '' ⋃ (i : ℕ), t i
case refine'_1
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ (n : ℕ), f '' t n ∪ range fᶜ
rw [← iUnion_union, Set.union_comm, ← inter_subset, ← image_iUnion, ←
  image_preimage_eq_inter_range]
no goals
case refine'_1
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
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_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
i : ι
⊢ f '' (f ⁻¹' (fun n => f '' t n ∪ range fᶜ) n) ⊆ f '' t n
case refine'_2
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ (∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' (f ⁻¹' (fun n => f '' t n ∪ range fᶜ) n))) ≤
    ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (f '' t n)
refine' ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono _
case refine'_2
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
i : ι
⊢ f ⁻¹' (f '' t n) ⊆ f ⁻¹' (f '' t n)
case refine'_2
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
i : ι
⊢ f '' (f ⁻¹' (fun n => f '' t n ∪ range fᶜ) n) ⊆ f '' t n
simp
no goals
case refine'_2
α : Type u_3
ι : Sort u_1
β : Type u_2
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
n : ℕ
i : ι
⊢ f ⁻¹' (f '' t n) ⊆ f ⁻¹' (f '' t n)
exact subset_refl _