α : Type u_2
β✝ : Type ?u.226327
γ : Type ?u.226330
δ : Type ?u.226333
ι : Type ?u.226336
R : Type ?u.226339
R' : Type ?u.226342
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s : Set α
⊢ ↑↑μ (f '' s) ≤
    ↑↑(OuterMeasure.toMeasure (↑(OuterMeasure.comap f) ↑μ)
            (_ :
              ∀ (s : Set α),
                MeasurableSet s →
                  ∀ (t : Set α),
                    ↑(↑(OuterMeasure.comap f) ↑μ) t =
                      ↑(↑(OuterMeasure.comap f) ↑μ) (t ∩ s) + ↑(↑(OuterMeasure.comap f) ↑μ) (t \ s)))
      s
α : Type u_2
β✝ : Type ?u.226327
γ : Type ?u.226330
δ : Type ?u.226333
ι : Type ?u.226336
R : Type ?u.226339
R' : Type ?u.226342
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s : Set α
⊢ ↑↑μ (f '' s) ≤ ↑↑(comap f μ) s
rw [comap, dif_pos (And.intro hfi hf)]
no goals
α : Type u_2
β✝ : Type ?u.226327
γ : Type ?u.226330
δ : Type ?u.226333
ι : Type ?u.226336
R : Type ?u.226339
R' : Type ?u.226342
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s : Set α
⊢ ↑↑μ (f '' s) ≤
    ↑↑(OuterMeasure.toMeasure (↑(OuterMeasure.comap f) ↑μ)
            (_ :
              ∀ (s : Set α),
                MeasurableSet s →
                  ∀ (t : Set α),
                    ↑(↑(OuterMeasure.comap f) ↑μ) t =
                      ↑(↑(OuterMeasure.comap f) ↑μ) (t ∩ s) + ↑(↑(OuterMeasure.comap f) ↑μ) (t \ s)))
      s
exact le_toMeasure_apply _ _ _