Theorem: HTPI.Like_Example_6_1_2 (HTPILib/Chap6.lean)

State before:
⊢ ∀ (n : ℕ), 3 ∣ n ^ 3 + 2 * n
Tactic:
by_induc
State after:
case Base_Case

⊢ 3 ∣ 0 ^ 3 + 2 * 0

case Induction_Step

⊢ ∀ (n : ℕ), 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

State before:
case Base_Case

⊢ 3 ∣ 0 ^ 3 + 2 * 0
Tactic:
define
State after:
case Base_Case

⊢ ∃ c, 0 ^ 3 + 2 * 0 = 3 * c

State before:
case Base_Case

⊢ ∃ c, 0 ^ 3 + 2 * 0 = 3 * c
Tactic:
apply Exists.intro 0
State after:
case Base_Case

⊢ 0 ^ 3 + 2 * 0 = 3 * 0

State before:
case Base_Case

⊢ 0 ^ 3 + 2 * 0 = 3 * 0
Tactic:
rfl
State after:
no goals

State before:
case Induction_Step

⊢ ∀ (n : ℕ), 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
fix n : Nat
State after:
case Induction_Step
n : ℕ
⊢ 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

State before:
case Induction_Step
n : ℕ
⊢ 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
assume ih : 3 ∣ n ^ 3 + 2 * n
State after:
case Induction_Step
n : ℕ
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

State before:
case Induction_Step
n : ℕ
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
define at ih
State after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

State before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
obtain (k : Nat) (h1 : n ^ 3 + 2 * n = 3 * k) from ih
State after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)

State before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
define
State after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ ∃ c, (n + 1) ^ 3 + 2 * (n + 1) = 3 * c

State before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ ∃ c, (n + 1) ^ 3 + 2 * (n + 1) = 3 * c
Tactic:
apply Exists.intro (k + n ^ 2 + n + 1)
State after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1)

State before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1)
Tactic:
show (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1) from
  calc (n + 1) ^ 3 + 2 * (n + 1)
    _ = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 := by ring
    _ = 3 * k + 3 * n ^ 2 + 3 * n + 3 := by rw [h1]
    _ = 3 * (k + n ^ 2 + n + 1) := by ring
State after:
no goals

State before:
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ (n + 1) ^ 3 + 2 * (n + 1) = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3
Tactic:
ring
State after:
no goals

State before:
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 = 3 * k + 3 * n ^ 2 + 3 * n + 3
Tactic:
rw [h1]
State after:
no goals

State before:
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ 3 * k + 3 * n ^ 2 + 3 * n + 3 = 3 * (k + n ^ 2 + n + 1)
Tactic:
ring
State after:
no goals