Theorem: C02S04.aux (MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean)

State before:
a b c d : ℝ
⊢ min a b + c ≤ min (a + c) (b + c)
Tactic:
apply le_min
State after:
case h₁
a b c d : ℝ
⊢ min a b + c ≤ a + c

case h₂
a b c d : ℝ
⊢ min a b + c ≤ b + c

State before:
case h₂
a b c d : ℝ
⊢ min a b + c ≤ b + c
Tactic:
apply add_le_add_right
State after:
case h₂.bc
a b c d : ℝ
⊢ min a b ≤ b

State before:
case h₂.bc
a b c d : ℝ
⊢ min a b ≤ b
Tactic:
apply min_le_right
State after:
no goals

State before:
case h₁
a b c d : ℝ
⊢ min a b + c ≤ a + c
Tactic:
apply add_le_add_right
State after:
case h₁.bc
a b c d : ℝ
⊢ min a b ≤ a

State before:
case h₁.bc
a b c d : ℝ
⊢ min a b ≤ a
Tactic:
apply min_le_left
State after:
no goals