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

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

State before:
n : ℕ
⊢ Symmetric (cong_mod_n n)
Tactic:
unfold Symmetric
State after:
n : ℕ
⊢ ∀ ⦃x y : ℕ⦄, cong_mod_n n x y → cong_mod_n n y x

State before:
n : ℕ
⊢ ∀ ⦃x y : ℕ⦄, cong_mod_n n x y → cong_mod_n n y x
Tactic:
intros x y
State after:
n x y : ℕ
⊢ cong_mod_n n x y → cong_mod_n n y x

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

State before:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ cong_mod_n n y x
Tactic:
unfold cong_mod_n
State after:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ y % n = x % n

State before:
n x y : ℕ
hxy : cong_mod_n n x y
⊢ y % n = x % n
Tactic:
unfold cong_mod_n at hxy
State after:
n x y : ℕ
hxy : x % n = y % n
⊢ y % n = x % n

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