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

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

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

State before:
n : ℕ
⊢ Equivalence fun a b => a % n = b % n
Tactic:
exact Equivalence.mk 
  (by intro x; rfl)
  (by intros x y h; rw [h]) 
  (by intros x y z hxy hyz; rw [hxy, hyz])
State after:
no goals

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

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

State before:
n : ℕ
⊢ ∀ {x y : ℕ}, x % n = y % n → y % n = x % n
Tactic:
intros x y h
State after:
n x y : ℕ
h : x % n = y % n
⊢ y % n = x % n

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

State before:
n : ℕ
⊢ ∀ {x y z : ℕ}, x % n = y % n → y % n = z % n → x % n = z % n
Tactic:
intros x y z hxy hyz
State after:
n x y z : ℕ
hxy : x % n = y % n
hyz : y % n = z % n
⊢ x % n = z % n

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