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

State before:
⊢ ∀ x > -1, ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Tactic:
fix x : Real
State after:
x : ℝ
⊢ x > -1 → ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x

State before:
x : ℝ
⊢ x > -1 → ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Tactic:
assume h1 : x > -1
State after:
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x

State before:
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x
Tactic:
by_induc
State after:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + ↑0 * x

case Induction_Step
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x

State before:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + ↑0 * x
Tactic:
rewrite [Nat.cast_zero]
State after:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + 0 * x

State before:
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥ 1 + 0 * x
Tactic:
linarith
State after:
no goals

State before:
case Induction_Step
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ), (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Tactic:
fix n : Nat
State after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
⊢ (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x

State before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
⊢ (1 + x) ^ n ≥ 1 + ↑n * x → (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Tactic:
assume ih : (1 + x) ^ n ≥ 1 + n * x
State after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x

State before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + ↑(n + 1) * x
Tactic:
rewrite [Nat.cast_succ]
State after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x

State before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
have h2 : 0 ≤ 1 + x := by linarith
State after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x

State before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
have h3 : x ^ 2 ≥ 0 := sq_nonneg x
State after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x

State before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
have h4 : n * x ^ 2 ≥ 0 :=
  calc n * x ^ 2
    _ ≥ n * 0 := by rel [h3]
    _ = 0 := by ring
State after:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x

State before:
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) ≥ 1 + (↑n + 1) * x
Tactic:
show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
  calc (1 + x) ^ (n + 1)
    _ = (1 + x) * (1 + x) ^ n := by rfl
    _ ≥ (1 + x) * (1 + n * x) := by rel [ih]
    _ = 1 + x + n * x + n * x ^ 2 := by ring
    _ ≥ 1 + x + n * x + 0 := by rel [h4]
    _ = 1 + (n + 1) * x := by ring
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
⊢ 0 ≤ 1 + x
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ ↑n * x ^ 2 ≥ ↑n * 0
Tactic:
rel [h3]
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
⊢ ↑n * 0 = 0
Tactic:
ring
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) ^ (n + 1) = (1 + x) * (1 + x) ^ n
Tactic:
rfl
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) * (1 + x) ^ n ≥ (1 + x) * (1 + ↑n * x)
Tactic:
rel [ih]
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ (1 + x) * (1 + ↑n * x) = 1 + x + ↑n * x + ↑n * x ^ 2
Tactic:
ring
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ 1 + x + ↑n * x + ↑n * x ^ 2 ≥ 1 + x + ↑n * x + 0
Tactic:
rel [h4]
State after:
no goals

State before:
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥ 1 + ↑n * x
h2 : 0 ≤ 1 + x
h3 : x ^ 2 ≥ 0
h4 : ↑n * x ^ 2 ≥ 0
⊢ 1 + x + ↑n * x + 0 = 1 + (↑n + 1) * x
Tactic:
ring
State after:
no goals