α : Type u_1
β : Type u_2
γ : Type ?u.225222
δ : Type ?u.225225
ι : Type ?u.225228
R : Type ?u.225231
R' : Type ?u.225234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
hs : NullMeasurableSet 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 =
    ↑↑μ (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.225222
δ : Type ?u.225225
ι : Type ?u.225228
R : Type ?u.225231
R' : Type ?u.225234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
hs : NullMeasurableSet s
⊢ ↑↑(comap f μ) s = ↑↑μ (f '' s)
rw [comap, dif_pos (And.intro hfi hf)] at hs⊢
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.225222
δ : Type ?u.225225
ι : Type ?u.225228
R : Type ?u.225231
R' : Type ?u.225234
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
hs : NullMeasurableSet 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 =
    ↑↑μ (f '' s)
rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply]