match this with
| Or.inl (_ : n > 1) =>
  have : 1 < n * m := calc
    1     ≤ _ := positive_ge.mp ‹Positive m›
    m     ≃ _ := Rel.symm AA.identL
    1 * m < _ := subst_mul_lt ‹Positive m› ‹1 < n›
    n * m ≃ _ := Rel.refl
  have two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
    AA.TwoOfThree.twoAndThree ‹n * m ≃ 1› ‹n * m > 1›
  have notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
    (trichotomy (n * m) 1).atMostOne
  exact absurd two notTwo
| Or.inr (_ : n ≃ 1) =>
  have : m ≃ 1 := calc
    m     ≃ _ := Rel.symm AA.identL
    1 * m ≃ _ := AA.substL (Rel.symm ‹n ≃ 1›)
    n * m ≃ _ := ‹n * m ≃ 1›
    1     ≃ _ := Rel.refl
  exact And.intro ‹n ≃ 1› ‹m ≃ 1›
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝¹ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝ : n ≥ 1
this : n > 1 ∨ n ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1
no goals