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

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

⊢ fact 4 > 2 ^ 4

case Induction_Step

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

State before:
case Base_Case

⊢ fact 4 > 2 ^ 4
Tactic:
decide
State after:
no goals

State before:
case Induction_Step

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

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

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

State before:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
⊢ fact (n + 1) > 2 ^ (n + 1)
Tactic:
have h2 : n + 1 > 2 := by linarith
State after:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ fact (n + 1) > 2 ^ (n + 1)

State before:
case Induction_Step
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ fact (n + 1) > 2 ^ (n + 1)
Tactic:
show fact (n + 1) > 2 ^ (n + 1) from
  calc fact (n + 1)
    _ = (n + 1) * fact n := by rfl
    _ > (n + 1) * 2 ^ n := by rel [ih]
    _ > 2 * 2 ^ n := by rel [h2]
    _ = 2 ^ (n + 1) := by ring
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
⊢ n + 1 > 2
Tactic:
linarith
State after:
no goals

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

State before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ (n + 1) * fact n > (n + 1) * 2 ^ n
Tactic:
rel [ih]
State after:
no goals

State before:
n : ℕ
h1 : n ≥ 4
ih : fact n > 2 ^ n
h2 : n + 1 > 2
⊢ (n + 1) * 2 ^ n > 2 * 2 ^ n
Tactic:
rel [h2]
State after:
no goals

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