case step =>
  intro n₁ (ih : ∀ y, n₁ ≃ y → n₁ * m ≃ y * m) n₂
  show step n₁ ≃ n₂ → step n₁ * m ≃ n₂ * m
  apply cases_on (motive := λ y => step n₁ ≃ y → step n₁ * m ≃ y * m)
  case zero =>
    intro (_ : step n₁ ≃ 0)
    exact absurd ‹step n₁ ≃ 0› step_neqv_zero
  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 : ℕ
⊢ ∀ (m_1 : ℕ), (∀ (y : ℕ), m_1 ≃ y → m_1 * m ≃ y * m) → ∀ (y : ℕ), step m_1 ≃ y → step m_1 * m ≃ y * m
no goals