case refine'_1
α : Type u_2
β✝ : Type ?u.585371
γ : Type ?u.585374
δ : Type ?u.585377
ι : Type ?u.585380
R : Type ?u.585383
R' : Type ?u.585386
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : AddGroup β
f g : α → β
h : f - g =ᶠ[ae μ] 0
x : α
hx : (f - g) x = OfNat.ofNat 0 x
⊢ f x = g x

case refine'_2
α : Type u_2
β✝ : Type ?u.585371
γ : Type ?u.585374
δ : Type ?u.585377
ι : Type ?u.585380
R : Type ?u.585383
R' : Type ?u.585386
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : AddGroup β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ (f - g) x = OfNat.ofNat 0 x
α : Type u_2
β✝ : Type ?u.585371
γ : Type ?u.585374
δ : Type ?u.585377
ι : Type ?u.585380
R : Type ?u.585383
R' : Type ?u.585386
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : AddGroup β
f g : α → β
⊢ f - g =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] g
refine' ⟨fun h => h.mono fun x hx => _, fun h => h.mono fun x hx => _⟩
no goals
case refine'_1
α : Type u_2
β✝ : Type ?u.585371
γ : Type ?u.585374
δ : Type ?u.585377
ι : Type ?u.585380
R : Type ?u.585383
R' : Type ?u.585386
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : AddGroup β
f g : α → β
h : f - g =ᶠ[ae μ] 0
x : α
hx : (f - g) x = OfNat.ofNat 0 x
⊢ f x = g x
rwa [Pi.sub_apply, Pi.zero_apply, sub_eq_zero] at hx
no goals
case refine'_2
α : Type u_2
β✝ : Type ?u.585371
γ : Type ?u.585374
δ : Type ?u.585377
ι : Type ?u.585380
R : Type ?u.585383
R' : Type ?u.585386
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
β : Type u_1
inst✝ : AddGroup β
f g : α → β
h : f =ᶠ[ae μ] g
x : α
hx : f x = g x
⊢ (f - g) x = OfNat.ofNat 0 x
rwa [Pi.sub_apply, Pi.zero_apply, sub_eq_zero]