α : Type u
β : Type v
γ : Type w
δ : Type ?u.185063
ι : Sort x
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
x✝ : α
a✝¹ : g x✝ = g' x✝
a✝ : f x✝ = f' x✝
⊢ (fun x => (f x, g x)) x✝ = (fun x => (f' x, g' x)) x✝
α : Type u
β : Type v
γ : Type w
δ : Type ?u.185063
ι : Sort x
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
⊢ ∀ (x : α), g x = g' x → f x = f' x → (fun x => (f x, g x)) x = (fun x => (f' x, g' x)) x
intros
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.185063
ι : Sort x
l : Filter α
f f' : α → β
hf : f =ᶠ[l] f'
g g' : α → γ
hg : g =ᶠ[l] g'
x✝ : α
a✝¹ : g x✝ = g' x✝
a✝ : f x✝ = f' x✝
⊢ (fun x => (f x, g x)) x✝ = (fun x => (f' x, g' x)) x✝
simp only [*]