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

State before:
P Q : Prop
⊢ P → P = Q → Q
Tactic:
intros h₁ h₂
State after:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ Q

State before:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ Q
Tactic:
rewrite [← h₂]
State after:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ P

State before:
P Q : Prop
h₁ : P
h₂ : P = Q
⊢ P
Tactic:
exact h₁
State after:
no goals