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:
rewrite [h₂]
State after:
a b c d : Int
h₁ : a < b
h₂ : c = d
⊢ a + d < b + d

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