α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ NullMeasurableSet (f '' s)
refine' ⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), measurableSet_toMeasurable _ _, _⟩
case refine'_1
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s

case refine'_2
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s)
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ f '' s =ᶠ[ae μ] toMeasurable μ (f '' toMeasurable (comap f μ) s)
refine' EventuallyEq.trans _ (NullMeasurableSet.toMeasurable_ae_eq _).symm
case refine'_2
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s)

case refine'_1
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
case refine'_1
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s

case refine'_2
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s)
swap
case refine'_1
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
h : toMeasurable (comap f μ) s =ᶠ[ae (comap f μ)] s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
case refine'_1
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
have h : toMeasurable (comap f μ) s =ᵐ[comap f μ] s :=
  @NullMeasurableSet.toMeasurable_ae_eq _ _ (μ.comap f : Measure α) s hs
no goals
case refine'_1
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
h : toMeasurable (comap f μ) s =ᶠ[ae (comap f μ)] s
⊢ f '' s =ᶠ[ae μ] f '' toMeasurable (comap f μ) s
exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm
no goals
case refine'_2
α : Type u_2
β✝ : Type ?u.251522
γ : Type ?u.251525
δ : Type ?u.251528
ι : Type ?u.251531
R : Type ?u.251534
R' : Type ?u.251537
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 α
hs : NullMeasurableSet s
⊢ NullMeasurableSet (f '' toMeasurable (comap f μ) s)
exact hf _ (measurableSet_toMeasurable _ _)