Theorem: LoVe.BackwardProofs.Exists_double_iden (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
⊢ ∃ n, double n = n
Tactic:
apply Exists.intro 0
State after:
⊢ double 0 = 0

State before:
⊢ double 0 = 0
Tactic:
rfl
State after:
no goals