match And.intro ‹p < q ∨ p ≃ q› ‹q < r ∨ q ≃ r› with
| (And.intro (Or.inl (_ : p < q)) (Or.inl (_ : q < r))) =>
  have : p < r := lt_trans ‹p < q› ‹q < r›
  have : p ≤ r := le_cases.mpr (Or.inl this)
  exact this
| (And.intro (Or.inl (_ : p < q)) (Or.inr (_ : q ≃ r))) =>
  have : p < r := trans_lt_eqv_lt ‹p < q› ‹q ≃ r›
  have : p ≤ r := le_cases.mpr (Or.inl this)
  exact this
| (And.intro (Or.inr (_ : p ≃ q)) (Or.inl (_ : q < r))) =>
  have : p < r := trans_eqv_lt_lt ‹p ≃ q› ‹q < r›
  have : p ≤ r := le_cases.mpr (Or.inl this)
  exact this
| (And.intro (Or.inr (_ : p ≃ q)) (Or.inr (_ : q ≃ r))) =>
  have : p ≃ r := eqv_trans ‹p ≃ q› ‹q ≃ r›
  have : p ≤ r := le_cases.mpr (Or.inr this)
  exact this
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Order ℚ
p q r : ℚ
x✝¹ : p ≤ q
x✝ : q ≤ r
this✝ : p < q ∨ p ≃ q
this : q < r ∨ q ≃ r
⊢ p ≤ r
no goals