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

State before:
⊢ ∀ n ≥ 5, 2 ^ n > n ^ 2
Tactic:
by_induc
State after:
case Base_Case

⊢ 2 ^ 5 > 5 ^ 2

case Induction_Step

⊢ ∀ n ≥ 5, 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2

State before:
case Base_Case

⊢ 2 ^ 5 > 5 ^ 2
Tactic:
decide
State after:
no goals

State before:
case Induction_Step

⊢ ∀ n ≥ 5, 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
fix n : Nat
State after:
case Induction_Step
n : ℕ
⊢ n ≥ 5 → 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2

State before:
case Induction_Step
n : ℕ
⊢ n ≥ 5 → 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
assume h1 : n ≥ 5
State after:
case Induction_Step
n : ℕ
h1 : n ≥ 5
⊢ 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2

State before:
case Induction_Step
n : ℕ
h1 : n ≥ 5
⊢ 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
assume ih : 2 ^ n > n ^ 2
State after:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
⊢ 2 ^ (n + 1) > (n + 1) ^ 2

State before:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
⊢ 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
have h2 : n * n ≥ 5 * n := Nat.mul_le_mul_right n h1
State after:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 ^ (n + 1) > (n + 1) ^ 2

State before:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
show 2 ^ (n + 1) > (n + 1) ^ 2 from
  calc 2 ^ (n + 1)
    _ = 2 * 2 ^ n := by ring
    _ > 2 * n ^ 2 := by linarith
    _ ≥ n ^ 2 + 5 * n := by linarith
    _ > n ^ 2 + 2 * n + 1 := by linarith
    _ = (n + 1) ^ 2 := by ring
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 ^ (n + 1) = 2 * 2 ^ n
Tactic:
ring
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 * 2 ^ n > 2 * n ^ 2
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 * n ^ 2 ≥ n ^ 2 + 5 * n
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ n ^ 2 + 5 * n > n ^ 2 + 2 * n + 1
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ n ^ 2 + 2 * n + 1 = (n + 1) ^ 2
Tactic:
ring
State after:
no goals