Theorem: Smt.Reconstruct.Int.sum_ub₄ (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d : Int
h₁ : a ≤ b
h₂ : c < d
⊢ a + c < b + d
Tactic:
have r₁ : a + c < a + d := Int.add_lt_add_left h₂ a
State after:
a b c d : Int
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d

State before:
a b c d : Int
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
⊢ a + c < b + d
Tactic:
have r₂ : a + d ≤ b + d := Int.add_le_add_right h₁ d
State after:
a b c d : Int
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d ≤ b + d
⊢ a + c < b + d

State before:
a b c d : Int
h₁ : a ≤ b
h₂ : c < d
r₁ : a + c < a + d
r₂ : a + d ≤ b + d
⊢ a + c < b + d
Tactic:
exact Int.lt_of_lt_of_le r₁ r₂
State after:
no goals