case mp =>
  intro (_ : min p q ≃ p)
  show p ≤ q
  have : min p q ≤ q := min_leR
  have : p ≤ q := le_substL_eqv ‹min p q ≃ p› ‹min 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 : ℚ
⊢ Ordered.min p q ≃ p → p ≤ q
no goals