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

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

State before:
u v : ℕ
⊢ (if v = u then v else if v = v then u else v) = u
Tactic:
by_cases h1 : v = u
State after:
case pos
u v : ℕ
h1 : v = u
⊢ (if v = u then v else if v = v then u else v) = u

case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = u then v else if v = v then u else v) = u

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

State before:
case pos
u v : ℕ
h1 : v = u
⊢ v = u
Tactic:
show v = u from h1
State after:
no goals

State before:
case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = u then v else if v = v then u else v) = u
Tactic:
rewrite [if_neg h1]
State after:
case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = v then u else v) = u

State before:
case neg
u v : ℕ
h1 : ¬v = u
⊢ (if v = v then u else v) = u
Tactic:
have h2 : v = v := by rfl
State after:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ (if v = v then u else v) = u

State before:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ (if v = v then u else v) = u
Tactic:
rewrite [if_pos h2]
State after:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ u = u

State before:
case neg
u v : ℕ
h1 : ¬v = u
h2 : v = v
⊢ u = u
Tactic:
rfl
State after:
no goals

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