Theorem: eq_nat_is_symm (Instructor/Lectures/grad/sets_relations.lean)

State before:
⊢ Symmetric Eq
Tactic:
unfold Symmetric
State after:
⊢ ∀ ⦃x y : ℕ⦄, x = y → y = x

State before:
⊢ ∀ ⦃x y : ℕ⦄, x = y → y = x
Tactic:
intro x y
State after:
x y : ℕ
⊢ x = y → y = x

State before:
x y : ℕ
⊢ x = y → y = x
Tactic:
intro hxy
State after:
x y : ℕ
hxy : x = y
⊢ y = x

State before:
x y : ℕ
hxy : x = y
⊢ y = x
Tactic:
rw [hxy]
State after:
no goals