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

State before:
u : ℕ
⊢ swap u u = id
Tactic:
apply funext
State after:
case h
u : ℕ
⊢ ∀ (x : ℕ), swap u u x = id x

State before:
case h
u : ℕ
⊢ ∀ (x : ℕ), swap u u x = id x
Tactic:
fix x : Nat
State after:
case h
u x : ℕ
⊢ swap u u x = id x

State before:
case h
u x : ℕ
⊢ swap u u x = id x
Tactic:
by_cases h1 : x = u
State after:
case pos
u x : ℕ
h1 : x = u
⊢ swap u u x = id x

case neg
u x : ℕ
h1 : ¬x = u
⊢ swap u u x = id x

State before:
case pos
u x : ℕ
h1 : x = u
⊢ swap u u x = id x
Tactic:
rewrite [h1, swap_fst]
State after:
case pos
u x : ℕ
h1 : x = u
⊢ u = id u

State before:
case pos
u x : ℕ
h1 : x = u
⊢ u = id u
Tactic:
rfl
State after:
no goals

State before:
case neg
u x : ℕ
h1 : ¬x = u
⊢ swap u u x = id x
Tactic:
rewrite [swap_other h1 h1]
State after:
case neg
u x : ℕ
h1 : ¬x = u
⊢ x = id x

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