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

State before:
u v i : ℕ
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Tactic:
by_cases h1 : i = u
State after:
case pos
u v i : ℕ
h1 : i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i

case neg
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i

State before:
case pos
u v i : ℕ
h1 : i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inl
State after:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v i = v

State before:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v i = v
Tactic:
rewrite [h1]
State after:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v u = v

State before:
case pos.h
u v i : ℕ
h1 : i = u
⊢ swap u v u = v
Tactic:
show swap u v u = v from swap_fst u v
State after:
no goals

State before:
case neg
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inr
State after:
case neg.h
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = u ∨ swap u v i = i

State before:
case neg.h
u v i : ℕ
h1 : ¬i = u
⊢ swap u v i = u ∨ swap u v i = i
Tactic:
by_cases h2 : i = v
State after:
case pos
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u ∨ swap u v i = i

case neg
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = u ∨ swap u v i = i

State before:
case pos
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inl
State after:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u

State before:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v i = u
Tactic:
rewrite [h2]
State after:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v v = u

State before:
case pos.h
u v i : ℕ
h1 : ¬i = u
h2 : i = v
⊢ swap u v v = u
Tactic:
show swap u v v = u from swap_snd u v
State after:
no goals

State before:
case neg
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = u ∨ swap u v i = i
Tactic:
apply Or.inr
State after:
case neg.h
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = i

State before:
case neg.h
u v i : ℕ
h1 : ¬i = u
h2 : ¬i = v
⊢ swap u v i = i
Tactic:
show swap u v i = i from swap_other h1 h2
State after:
no goals