case step =>
  intro n₂ (_ : step n₁ ≃ step n₂)
  show step n₁ * m ≃ step n₂ * m
  have : n₁ ≃ n₂ := AA.inject ‹step n₁ ≃ step n₂›
  have : n₁ * m ≃ n₂ * m := ih n₂ ‹n₁ ≃ n₂›
  calc
    step n₁ * m  ≃ _ := step_mul
    (n₁ * m) + m ≃ _ := AA.substL ‹n₁ * m ≃ n₂ * m›
    (n₂ * m) + m ≃ _ := Rel.symm step_mul
    step n₂ * m  ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂ : ℕ
⊢ ∀ (m_1 : ℕ), step n₁ ≃ step m_1 → step n₁ * m ≃ step m_1 * m
no goals