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

State before:
u v n : ℕ
h1 : u < n
h2 : v < n
⊢ maps_below n (swap u v)
Tactic:
define
State after:
u v n : ℕ
h1 : u < n
h2 : v < n
⊢ ∀ i < n, swap u v i < n

State before:
u v n : ℕ
h1 : u < n
h2 : v < n
⊢ ∀ i < n, swap u v i < n
Tactic:
fix i : Nat
State after:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
⊢ i < n → swap u v i < n

State before:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
⊢ i < n → swap u v i < n
Tactic:
assume h3 : i < n
State after:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
⊢ swap u v i < n

State before:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
⊢ swap u v i < n
Tactic:
have h4 : swap u v i = v ∨ swap u v i = u ∨ swap u v i = i := swap_values u v i
State after:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n

State before:
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v ∨ swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n
Tactic:
by_cases on h4
State after:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ swap u v i < n

case Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n

State before:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ swap u v i < n
Tactic:
rewrite [h4]
State after:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ v < n

State before:
case Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = v
⊢ v < n
Tactic:
show v < n from h2
State after:
no goals

State before:
case Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u ∨ swap u v i = i
⊢ swap u v i < n
Tactic:
by_cases on h4
State after:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ swap u v i < n

case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ swap u v i < n

State before:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ swap u v i < n
Tactic:
rewrite [h4]
State after:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ u < n

State before:
case Case_2.Case_1
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = u
⊢ u < n
Tactic:
show u < n from h1
State after:
no goals

State before:
case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ swap u v i < n
Tactic:
rewrite [h4]
State after:
case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ i < n

State before:
case Case_2.Case_2
u v n : ℕ
h1 : u < n
h2 : v < n
i : ℕ
h3 : i < n
h4 : swap u v i = i
⊢ i < n
Tactic:
show i < n from h3
State after:
no goals