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

State before:
α : Type
t : α
P : α → Prop
hall : ∀ (x : α), x = t → P x
⊢ P t
Tactic:
apply hall t
State after:
α : Type
t : α
P : α → Prop
hall : ∀ (x : α), x = t → P x
⊢ t = t

State before:
α : Type
t : α
P : α → Prop
hall : ∀ (x : α), x = t → P x
⊢ t = t
Tactic:
rfl
State after:
no goals

State before:
α : Type
t : α
P : α → Prop
hp : P t
x : α
heq : x = t
⊢ P x
Tactic:
rw [heq]
State after:
α : Type
t : α
P : α → Prop
hp : P t
x : α
heq : x = t
⊢ P t

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