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

State before:
⊢ Transitive Eq
Tactic:
unfold Transitive
State after:
⊢ ∀ ⦃x y z : ℕ⦄, x = y → y = z → x = z

State before:
⊢ ∀ ⦃x y z : ℕ⦄, x = y → y = z → x = z
Tactic:
intros x y z
State after:
x y z : ℕ
⊢ x = y → y = z → x = z

State before:
x y z : ℕ
⊢ x = y → y = z → x = z
Tactic:
intros hxy hyz
State after:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ x = z

State before:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ x = z
Tactic:
rw [hxy]
State after:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ y = z

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