α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
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 μ] g
have h_ss : sᶜ ⊆ { a : α | ite (a ∈ s) (f a) (g a) = g a } := fun x hx => by
  simp [(Set.mem_compl_iff _ _).mp hx]
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] g
refine' measure_mono_null _ hs_zero
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ s
conv_rhs => rw [← compl_compl s]
no goals
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
h_ss : sᶜ ⊆ {a | (if a ∈ s then f a else g a) = g a}
⊢ {x | (fun x => (fun x => if x ∈ s then f x else g x) x = g x) x}ᶜ ⊆ sᶜᶜ
rwa [Set.compl_subset_compl]
no goals
α : Type u_2
β : Type ?u.717923
γ✝ : Type ?u.717926
δ : Type ?u.717929
ι : Type ?u.717932
R : Type ?u.717935
R' : Type ?u.717938
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ✝
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
γ : Type u_1
f g : α → γ
s : Set α
hs_zero : ↑↑μ s = 0
x : α
hx : x ∈ sᶜ
⊢ x ∈ {a | (if a ∈ s then f a else g a) = g a}
simp [(Set.mem_compl_iff _ _).mp hx]