case hc
α : Type u_2
β✝ : Type ?u.221666
γ : Type ?u.221669
δ : Type ?u.221672
ι : Type ?u.221675
R : Type ?u.221678
R' : Type ?u.221681
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

case hc
α : Type u_2
β✝ : Type ?u.221666
γ : Type ?u.221669
δ : Type ?u.221672
ι : Type ?u.221675
R : Type ?u.221678
R' : Type ?u.221681
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
α : Type u_2
β✝ : Type ?u.221666
γ : Type ?u.221669
δ : Type ?u.221672
ι : Type ?u.221675
R : Type ?u.221678
R' : Type ?u.221681
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ ↑↑(↑(comapₗ f) μ) s = ↑↑μ (f '' s)
rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply]
no goals
case hc
α : Type u_2
β✝ : Type ?u.221666
γ : Type ?u.221669
δ : Type ?u.221672
ι : Type ?u.221675
R : Type ?u.221678
R' : Type ?u.221681
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)

case hc
α : Type u_2
β✝ : Type ?u.221666
γ : Type ?u.221669
δ : Type ?u.221672
ι : Type ?u.221675
R : Type ?u.221678
R' : Type ?u.221681
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
μ : Measure β
hs : MeasurableSet s
⊢ Injective f ∧ ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
exact ⟨hfi, hf⟩