match eq : decide (p > q) with
| true =>
  show q ≤ (if true then p else q)
  show q ≤ p
  have : p > q := ofBoolUsing_eq_true eq
  have : q ≤ p := le_cases.mpr (Or.inl ‹q < p›)
  exact this
| false =>
  show q ≤ (if false then p else q)
  show q ≤ q
  exact le_refl
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≤ if decide (p > q) = true then p else q
no goals