case h
α : Type u_1
β : Type ?u.27073
γ : Type ?u.27076
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤
hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤
hfg : (fun x => ENNReal.toReal (f x)) =ᶠ[l] fun x => ENNReal.toReal (g x)
a✝¹ : α
hfx : f a✝¹ ≠ ⊤
hgx : g a✝¹ ≠ ⊤
a✝ : ENNReal.toReal (f a✝¹) = ENNReal.toReal (g a✝¹)
⊢ f a✝¹ = g a✝¹
α : Type u_1
β : Type ?u.27073
γ : Type ?u.27076
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤
hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤
hfg : (fun x => ENNReal.toReal (f x)) =ᶠ[l] fun x => ENNReal.toReal (g x)
⊢ f =ᶠ[l] g
filter_upwards [hfi, hgi, hfg]with _ hfx hgx _
no goals
case h
α : Type u_1
β : Type ?u.27073
γ : Type ?u.27076
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤
hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤
hfg : (fun x => ENNReal.toReal (f x)) =ᶠ[l] fun x => ENNReal.toReal (g x)
a✝¹ : α
hfx : f a✝¹ ≠ ⊤
hgx : g a✝¹ ≠ ⊤
a✝ : ENNReal.toReal (f a✝¹) = ENNReal.toReal (g a✝¹)
⊢ f a✝¹ = g a✝¹
rwa [← ENNReal.toReal_eq_toReal hfx hgx]