α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ (sᶜ) = 0
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f
change s ∈ μ.ae at hs_zero
case h
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
⊢ ∀ (a : α), a ∈ s → (if a ∈ s then f a else g a) = f a
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f
filter_upwards [hs_zero]
case h
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ (if a✝¹ ∈ s then f a✝¹ else g a✝¹) = f a✝¹
case h
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
⊢ ∀ (a : α), a ∈ s → (if a ∈ s then f a else g a) = f a
intros
case h
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ f a✝¹ = f a✝¹
case h
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ (if a✝¹ ∈ s then f a✝¹ else g a✝¹) = f a✝¹
split_ifs
no goals
case h
α : Type u_2
β : Type ?u.720764
γ✝ : Type ?u.720767
δ : Type ?u.720770
ι : Type ?u.720773
R : Type ?u.720776
R' : Type ?u.720779
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ f a✝¹ = f a✝¹
rfl