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
⊢ b + c ≤ b + d

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