Theorem: Smt.Reconstruct.Prop.congrHAdd (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
α β γ : Type
inst✝ : HAdd α β γ
⊢ ∀ {a₁ a₂ : α} {b₁ b₂ : β}, a₁ = a₂ → b₁ = b₂ → a₁ + b₁ = a₂ + b₂
Tactic:
intros a₁ a₂ b₁ b₂ h₁ h₂
State after:
α β γ : Type
inst✝ : HAdd α β γ
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ a₁ + b₁ = a₂ + b₂

State before:
α β γ : Type
inst✝ : HAdd α β γ
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ a₁ + b₁ = a₂ + b₂
Tactic:
rw [h₁, h₂]
State after:
no goals