Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leR (Lean4Axiomatic/Rational/Impl/Generic/MinMax.lean)

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ Ordered.min p q ≤ q
Tactic:
show (if decide (p < q) then p else q) ≤ q
State after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≤ q

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

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ (if true = true then p else q) ≤ q
Tactic:
show p ≤ q
State after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ p ≤ q

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
⊢ p ≤ q
Tactic:
have : p < q := ofBoolUsing_eq_true eq
State after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this : p < q
⊢ p ≤ q

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this : p < q
⊢ p ≤ q
Tactic:
have : p ≤ q := le_cases.mpr (Or.inl this)
State after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this✝ : p < q
this : p ≤ q
⊢ p ≤ q

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = true
this✝ : p < q
this : p ≤ q
⊢ p ≤ q
Tactic:
exact this
State after:
no goals

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ (if false = true then p else q) ≤ q
Tactic:
show q ≤ q
State after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ q ≤ q

State before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
eq : decide (p < q) = false
⊢ q ≤ q
Tactic:
exact le_refl
State after:
no goals