case mpr =>
  intro (_ : p ≃ 0 ∨ q ≃ 0)
  show p * q ≃ 0
  match ‹p ≃ 0 ∨ q ≃ 0› with
  | Or.inl (_ : p ≃ 0) => calc
    p * q ≃ _ := mul_substL ‹p ≃ 0›
    0 * q ≃ _ := mul_absorbL
    0     ≃ _ := eqv_refl
  | Or.inr (_ : q ≃ 0) => calc
    p * q ≃ _ := mul_substR ‹q ≃ 0›
    p * 0 ≃ _ := mul_absorbR
    0     ≃ _ := eqv_refl
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
⊢ p ≃ 0 ∨ q ≃ 0 → p * q ≃ 0
no goals