case zero =>
  intro n₂
  show 0 ≃ n₂ → 0 * m ≃ n₂ * m
  apply cases_on (motive := λ y => 0 ≃ y → 0 * m ≃ y * m)
  case zero =>
    intro (_ : 0 ≃ (0 : ℕ))
    show 0 * m ≃ 0 * m
    exact Rel.refl
  case step =>
    intro n₂ (_ : 0 ≃ step n₂)
    exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 * m ≃ y * m
no goals