case mpr =>
  intro (_ : p ≤ q)
  show min p q ≃ p
  have : min p q ≃ p ∨ min p q ≃ q := min_cases
  match this with
  | Or.inl (_ : min p q ≃ p) =>
    have := ‹min p q ≃ p›
    exact this
  | Or.inr (_ : min p q ≃ q) =>
    have : min p q ≤ p := min_leL
    have : q ≤ p := le_substL_eqv ‹min p q ≃ q› ‹min p q ≤ p›
    have : q ≃ p := le_antisymm ‹q ≤ p› ‹p ≤ q›
    have : min p q ≃ p := eqv_trans ‹min p q ≃ q› ‹q ≃ p›
    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 : ℚ
⊢ p ≤ q → Ordered.min p q ≃ p
no goals