match ‹a ≃ 0 ∨ b - c ≃ 0› with
| Or.inl (_ : a ≃ 0) =>
  show b ≃ c
  exact absurd ‹a ≃ 0› ‹a ≄ 0›
| Or.inr (_ : b - c ≃ 0) =>
  show b ≃ c
  exact zero_diff_iff_eqv.mp ‹b - c ≃ 0›
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this✝¹ : a * b - a * c ≃ 0
this✝ : a * (b - c) ≃ 0
this : a ≃ 0 ∨ b - c ≃ 0
⊢ b ≃ c
no goals