no goals
α : Type u
β : Type v
γ : Type w
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂
simp [tendsto_def, Function.graph, rtendsto_def, Rel.core, Set.preimage]