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

State before:
u v n : ℕ
⊢ ∀ i < n, swap u v (swap u v i) = i
Tactic:
fix i : Nat
State after:
u v n i : ℕ
⊢ i < n → swap u v (swap u v i) = i

State before:
u v n i : ℕ
⊢ i < n → swap u v (swap u v i) = i
Tactic:
assume h : i < n
State after:
u v n i : ℕ
h : i < n
⊢ swap u v (swap u v i) = i

State before:
u v n i : ℕ
h : i < n
⊢ swap u v (swap u v i) = i
Tactic:
by_cases h1 : i = u
State after:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ swap u v (swap u v i) = i

case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
⊢ swap u v (swap u v i) = i

State before:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ swap u v (swap u v i) = i
Tactic:
rewrite [h1, swap_fst, swap_snd]
State after:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ u = u

State before:
case pos
u v n i : ℕ
h : i < n
h1 : i = u
⊢ u = u
Tactic:
rfl
State after:
no goals

State before:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
⊢ swap u v (swap u v i) = i
Tactic:
by_cases h2 : i = v
State after:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ swap u v (swap u v i) = i

case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v (swap u v i) = i

State before:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ swap u v (swap u v i) = i
Tactic:
rewrite [h2, swap_snd, swap_fst]
State after:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ v = v

State before:
case pos
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : i = v
⊢ v = v
Tactic:
rfl
State after:
no goals

State before:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v (swap u v i) = i
Tactic:
rewrite [swap_other h1 h2, swap_other h1 h2]
State after:
case neg
u v n i : ℕ
h : i < n
h1 : ¬i = u
h2 : ¬i = v
⊢ i = i

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