Theorem: HTPI.swap_fst (HTPILib/Chap7.lean)

State before:
u v : ℕ
⊢ swap u v u = v
Tactic:
define : swap u v u
State after:
u v : ℕ
⊢ (if u = u then v else if u = v then u else u) = v

State before:
u v : ℕ
⊢ (if u = u then v else if u = v then u else u) = v
Tactic:
have h : u = u := by rfl
State after:
u v : ℕ
h : u = u
⊢ (if u = u then v else if u = v then u else u) = v

State before:
u v : ℕ
h : u = u
⊢ (if u = u then v else if u = v then u else u) = v
Tactic:
rewrite [if_pos h]
State after:
u v : ℕ
h : u = u
⊢ v = v

State before:
u v : ℕ
h : u = u
⊢ v = v
Tactic:
rfl
State after:
no goals

State before:
u v : ℕ
⊢ u = u
Tactic:
rfl
State after:
no goals