Theorem: Smt.Reconstruct.Arith.sumBounds₂ (Smt/Reconstruct/Arith/SumBounds/Lemmas.lean)

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
⊢ a < b → c ≤ d → a + c < b + d
Tactic:
intros h₁ h₂
State after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
⊢ a + c < b + d

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
⊢ a + c < b + d
Tactic:
have r₁: a + c ≤ a + d := add_le_add_left h₂ a
State after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c < b + d

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
⊢ a + c < b + d
Tactic:
have r₂: a + d < b + d := add_lt_add_right h₁ d
State after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d < b + d
⊢ a + c < b + d

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a < b
h₂ : c ≤ d
r₁ : a + c ≤ a + d
r₂ : a + d < b + d
⊢ a + c < b + d
Tactic:
exact lt_of_le_of_lt r₁ r₂
State after:
no goals