case mpr =>
  intro (And.intro (_ : n ≃ 1) (_ : m ≃ 1))
  show n * m ≃ 1
  calc
    n * m ≃ _ := AA.substL ‹n ≃ 1›
    1 * m ≃ _ := AA.identL
    m     ≃ _ := ‹m ≃ 1›
    1     ≃ _ := Rel.refl
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 1 ∧ m ≃ 1 → n * m ≃ 1
no goals