no goals
α : Type u
β : Type v
γ : Type ?u.207058
δ : Type ?u.207061
ε : Type ?u.207064
ζ : Type ?u.207067
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.207078
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f✝ : α → (i : ι) → π i
inst✝ : DecidableEq ι
l : Filter β
f : β → (i : ι) → π i
x : (i : ι) → π i
hf : Tendsto f l (𝓝 x)
i : ι
g : β → π i
xi : π i
hg : Tendsto g l (𝓝 xi)
j : ι
⊢ Tendsto (fun i_1 => Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))
rcases eq_or_ne j i with (rfl | hj) <;> simp [*, hf.apply]