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

State before:
⊢ Reflexive Eq
Tactic:
unfold Reflexive
State after:
⊢ ∀ (x : ℕ), x = x

State before:
⊢ ∀ (x : ℕ), x = x
Tactic:
intro x
State after:
x : ℕ
⊢ x = x

State before:
x : ℕ
⊢ x = x
Tactic:
exact rfl
State after:
no goals