Theorem: HTPI.fzn_fnz (HTPILib/Chap8Part2.lean)

State before:
⊢ fzn ∘ fnz = id
Tactic:
apply funext
State after:
case h

⊢ ∀ (x : ℕ), (fzn ∘ fnz) x = id x

State before:
case h

⊢ ∀ (x : ℕ), (fzn ∘ fnz) x = id x
Tactic:
fix n : Nat
State after:
case h
n : ℕ
⊢ (fzn ∘ fnz) n = id n

State before:
case h
n : ℕ
⊢ (fzn ∘ fnz) n = id n
Tactic:
rewrite [comp_def]
State after:
case h
n : ℕ
⊢ fzn (fnz n) = id n

State before:
case h
n : ℕ
⊢ fzn (fnz n) = id n
Tactic:
have h1 : nat_even n ∨ nat_odd n := Exercise_6_1_16a1 n
State after:
case h
n : ℕ
h1 : nat_even n ∨ nat_odd n
⊢ fzn (fnz n) = id n

State before:
case h
n : ℕ
h1 : nat_even n ∨ nat_odd n
⊢ fzn (fnz n) = id n
Tactic:
by_cases on h1
State after:
case h.Case_1
n : ℕ
h1 : nat_even n
⊢ fzn (fnz n) = id n

case h.Case_2
n : ℕ
h1 : nat_odd n
⊢ fzn (fnz n) = id n

State before:
case h.Case_1
n : ℕ
h1 : nat_even n
⊢ fzn (fnz n) = id n
Tactic:
obtain (k : Nat) (h2 : n = 2 * k) from h1
State after:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ fzn (fnz n) = id n

State before:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ fzn (fnz n) = id n
Tactic:
rewrite [h2, fnz_even, fzn_nat]
State after:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ 2 * k = id (2 * k)

State before:
case h.Case_1
n : ℕ
h1 : nat_even n
k : ℕ
h2 : n = 2 * k
⊢ 2 * k = id (2 * k)
Tactic:
rfl
State after:
no goals

State before:
case h.Case_2
n : ℕ
h1 : nat_odd n
⊢ fzn (fnz n) = id n
Tactic:
obtain (k : Nat) (h2 : n = 2 * k + 1) from h1
State after:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ fzn (fnz n) = id n

State before:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ fzn (fnz n) = id n
Tactic:
rewrite [h2, fnz_odd, fzn_neg_succ_nat]
State after:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ 2 * k + 1 = id (2 * k + 1)

State before:
case h.Case_2
n : ℕ
h1 : nat_odd n
k : ℕ
h2 : n = 2 * k + 1
⊢ 2 * k + 1 = id (2 * k + 1)
Tactic:
rfl
State after:
no goals