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

State before:
k : ℕ
⊢ fnz (2 * k) = ↑k
Tactic:
have h1 : 2 ∣ 2 * k := by
  apply Exists.intro k
  rfl
  done
State after:
k : ℕ
h1 : 2 ∣ 2 * k
⊢ fnz (2 * k) = ↑k

State before:
k : ℕ
h1 : 2 ∣ 2 * k
⊢ fnz (2 * k) = ↑k
Tactic:
have h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2)
  else -↑((2 * k + 1) / 2) := by rfl
State after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2) else -↑((2 * k + 1) / 2)
⊢ fnz (2 * k) = ↑k

State before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2) else -↑((2 * k + 1) / 2)
⊢ fnz (2 * k) = ↑k
Tactic:
rewrite [if_pos h1] at h2
State after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
⊢ fnz (2 * k) = ↑k

State before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
⊢ fnz (2 * k) = ↑k
Tactic:
have h3 : 0 < 2 := by linarith
State after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k

State before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k
Tactic:
rewrite [Nat.mul_div_cancel_left k h3] at h2
State after:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑k
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k

State before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑k
h3 : 0 < 2
⊢ fnz (2 * k) = ↑k
Tactic:
show fnz (2 * k) = ↑k from h2
State after:
no goals

State before:
k : ℕ
⊢ 2 ∣ 2 * k
Tactic:
apply Exists.intro k
State after:
k : ℕ
⊢ 2 * k = 2 * k

State before:
k : ℕ
⊢ 2 * k = 2 * k
Tactic:
rfl
State after:
no goals

State before:
k : ℕ
h1 : 2 ∣ 2 * k
⊢ fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2) else -↑((2 * k + 1) / 2)
Tactic:
rfl
State after:
no goals

State before:
k : ℕ
h1 : 2 ∣ 2 * k
h2 : fnz (2 * k) = ↑(2 * k / 2)
⊢ 0 < 2
Tactic:
linarith
State after:
no goals