match tri with
| AA.OneOfThree.first (_ : n < m) =>
  have : compare n m = Ordering.lt := compare_lt.mpr ‹n < m›
  have : n + k < m + k := lt_substL_add ‹n < m›
  have : compare (n + k) (m + k) = Ordering.lt := compare_lt.mpr this
  calc
    compare n m
      = _ := ‹compare n m = Ordering.lt›
    Ordering.lt
      = _ := by rw [‹compare (n + k) (m + k) = Ordering.lt›]
    compare (n + k) (m + k)
      = _ := rfl
| AA.OneOfThree.second (_ : n ≃ m) =>
  have : compare n m = Ordering.eq := compare_eq.mpr ‹n ≃ m›
  have : n + k ≃ m + k := AA.substL ‹n ≃ m›
  have : compare (n + k) (m + k) = Ordering.eq :=
    compare_eq.mpr ‹n + k ≃ m + k›
  calc
    compare n m
      = _ := ‹compare n m = Ordering.eq›
    Ordering.eq
      = _ := Eq.symm ‹compare (n + k) (m + k) = Ordering.eq›
    compare (n + k) (m + k)
      = _ := rfl
| AA.OneOfThree.third (_ : n > m) =>
  have : compare n m = Ordering.gt := compare_gt.mpr ‹n > m›
  have : n + k > m + k := lt_substL_add ‹n > m›
  have : compare (n + k) (m + k) = Ordering.gt :=
    compare_gt.mpr ‹n + k > m + k›
  calc
    compare n m
      = _ := ‹compare n m = Ordering.gt›
    Ordering.gt
      = _ := Eq.symm ‹compare (n + k) (m + k) = Ordering.gt›
    compare (n + k) (m + k)
      = _ := rfl
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
n m k : ℕ
tri : AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ compare n m = compare (n + k) (m + k)
no goals