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:
rewrite [h₁, h₂]
State after:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c = d
⊢ b + d ≤ b + d

State before:
α : Type
inst✝ : LinearOrderedRing α
a b c d : α
h₁ : a = b
h₂ : c = d
⊢ b + d ≤ b + d
Tactic:
exact le_refl (b + d)
State after:
no goals