case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
hu : u ~[l] const α c
⊢ Tendsto u l (𝓝 c)
rcases em <| c = 0 with rfl | h
no goals
case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)
exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds
no goals
case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)
exact (isEquivalent_const_iff_tendsto h).mp hu