Theorem: LoVe.Nat.Eq_symm_manual (LoVe/Lectures/LoVe08_Metaprogramming_Demo.lean)

State before:
x y : ℕ
h : x = y
⊢ y = x
Tactic:
apply symm
State after:
case a
x y : ℕ
h : x = y
⊢ x = y

State before:
case a
x y : ℕ
h : x = y
⊢ x = y
Tactic:
hypothesis
State after:
no goals