Theorem: LoVe.ForwardProofs.Exists.one_point (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P t
Tactic:
rw [←hxt]
State after:
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P x

State before:
α : Type
t : α
P : α → Prop
hex : ∃ x, x = t ∧ P x
x : α
hand : x = t ∧ P x
hxt : x = t
hpx : P x
⊢ P x
Tactic:
exact hpx
State after:
no goals

State before:
α : Type
t : α
P : α → Prop
hp : P t
⊢ t = t
Tactic:
rfl
State after:
no goals