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

State before:
⊢ ∀ (n : ℕ), Transitive (cong_mod_n n)
Tactic:
intro n a b c hab hbc
State after:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ cong_mod_n n a c

State before:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ cong_mod_n n a c
Tactic:
unfold cong_mod_n
State after:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ a % n = c % n

State before:
n a b c : ℕ
hab : cong_mod_n n a b
hbc : cong_mod_n n b c
⊢ a % n = c % n
Tactic:
unfold cong_mod_n at hab hbc
State after:
n a b c : ℕ
hab : a % n = b % n
hbc : b % n = c % n
⊢ a % n = c % n

State before:
n a b c : ℕ
hab : a % n = b % n
hbc : b % n = c % n
⊢ a % n = c % n
Tactic:
rw [hab, hbc]
State after:
no goals