-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem map_ofFunction {β} {f : α → β} (hf : Injective f) :
    map f (OuterMeasure.ofFunction m m_empty) =
      OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty

Proof state:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ s ⊆ ⋃ n, (range f)ᶜ ∪ f '' t n

Tactic:
rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]

Result:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ f '' (f ⁻¹' s) ⊆ f '' ⋃ i, t i

Proof state:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ f '' (f ⁻¹' s) ⊆ f '' ⋃ i, t i

Tactic:
exact image_subset _ ht

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
⊢ ∀ (i : ℕ → Set α), f ⁻¹' s ⊆ iUnion i → ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (i n)

Tactic:
intro t ht

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (t n)

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
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)

Tactic:
refine ENNReal.tsum_le_tsum fun n => le_of_eq ?_

Result:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
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)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
t : ℕ → Set α
ht : f ⁻¹' s ⊆ iUnion t
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (t n)

Tactic:
refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)

Result:
case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
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_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
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)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
⊢ (OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty) s ≤ ((map f) (OuterMeasure.ofFunction m m_empty)) s

Tactic:
simp only [ofFunction_apply, map_apply, le_iInf_iff]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
⊢ ∀ (i : ℕ → Set α), f ⁻¹' s ⊆ iUnion i → ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (i n)

Proof state:
case refine_2
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
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)

Tactic:
simp [hf.preimage_image]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
⊢ (map f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty

Tactic:
refine (map_ofFunction_le _).antisymm fun s => ?_

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
β : Type u_2
f : α → β
hf : Injective f
s : Set β
⊢ (OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty) s ≤ ((map f) (OuterMeasure.ofFunction m m_empty)) s