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

State before:
⊢ ∀ (n : ℕ), Reflexive (cong_mod_n n)
Tactic:
intro n
State after:
n : ℕ
⊢ Reflexive (cong_mod_n n)

State before:
n : ℕ
⊢ Reflexive (cong_mod_n n)
Tactic:
unfold cong_mod_n
State after:
n : ℕ
⊢ Reflexive fun a b => a % n = b % n

State before:
n : ℕ
⊢ Reflexive fun a b => a % n = b % n
Tactic:
unfold Reflexive
State after:
n : ℕ
⊢ ∀ (x : ℕ), (fun a b => a % n = b % n) x x

State before:
n : ℕ
⊢ ∀ (x : ℕ), (fun a b => a % n = b % n) x x
Tactic:
intro a
State after:
n a : ℕ
⊢ a % n = a % n

State before:
n a : ℕ
⊢ a % n = a % n
Tactic:
exact rfl
State after:
no goals