match this with
| Or.inl (_ : q > r) =>
  have : p > r := gt_trans ‹p > q› ‹q > r›
  exact this
| Or.inr (_ : q ≃ r) =>
  have : p > r := lt_substL_eqv ‹q ≃ r› ‹p > q›
  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 : q > r ∨ q ≃ r
⊢ p > r
no goals