case mp =>
  intro (_ : n * m ≃ 1)
  show n ≃ 1 ∧ m ≃ 1
  have : Positive (n * m) :=
    positive_subst (Rel.symm ‹n * m ≃ 1›) one_positive
  have (And.intro (_ : Positive n) (_ : Positive m)) :=
    mul_preserves_positive.mp this
  have : n ≥ 1 := positive_ge.mp ‹Positive n›
  have : n > 1 ∨ n ≃ 1 := ge_split this
  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 : ℕ
⊢ n * m ≃ 1 → n ≃ 1 ∧ m ≃ 1
no goals