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

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

State before:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ (if i = u then v else if i = v then u else i) = i
Tactic:
rewrite [if_neg h1, if_neg h2]
State after:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ i = i

State before:
u v i : ℕ
h1 : i ≠ u
h2 : i ≠ v
⊢ i = i
Tactic:
rfl
State after:
no goals