case inl
α : Type u
β : Type v
γ : Type w
⊢ Tendsto (↑(AddSubgroup.subtype (zmultiples 0))) cofinite (cocompact ℝ)

case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Tendsto (↑(AddSubgroup.subtype (zmultiples a))) cofinite (cocompact ℝ)
α : Type u
β : Type v
γ : Type w
a : ℝ
⊢ Tendsto (↑(AddSubgroup.subtype (zmultiples a))) cofinite (cocompact ℝ)
rcases eq_or_ne a 0 with rfl | ha
case inl
α : Type u
β : Type v
γ : Type w
⊢ Tendsto ↑(AddSubgroup.subtype ⊥) ⊥ (cocompact ℝ)
case inl
α : Type u
β : Type v
γ : Type w
⊢ Tendsto (↑(AddSubgroup.subtype (zmultiples 0))) cofinite (cocompact ℝ)
rw [zmultiples_zero_eq_bot, cofinite_eq_bot]
no goals
case inl
α : Type u
β : Type v
γ : Type w
⊢ Tendsto ↑(AddSubgroup.subtype ⊥) ⊥ (cocompact ℝ)
exact tendsto_bot