match this with
| Or.inl (_ : max p q ≃ p) =>
  have : q ≤ max p q := max_leR
  have : q ≤ p := le_substR_eqv ‹max p q ≃ p› ‹q ≤ max p q›
  have : p ≃ q := le_antisymm ‹p ≤ q› ‹q ≤ p›
  have : max p q ≃ q := eqv_trans ‹max p q ≃ p› ‹p ≃ q›
  exact this
| Or.inr (_ : max p q ≃ q) =>
  have := ‹max p q ≃ 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 ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
this : Ordered.max p q ≃ p ∨ Ordered.max p q ≃ q
⊢ Ordered.max p q ≃ q
no goals