Theorem: HTPI.induc_from (HTPILib/HTPIDefs.lean)

State before:
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ n ≥ k, P n
Tactic:
apply @Nat.rec
State after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ Nat.zero ≥ k → P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)

State before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ Nat.zero ≥ k → P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
assume h3
State after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)

State before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
have h4 : k = 0 := Nat.eq_zero_of_le_zero h3
State after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)

State before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
rewrite [h4] at h1
State after:
case zero
P : ℕ → Prop
k : ℕ
h1 : P 0
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)

State before:
case zero
P : ℕ → Prop
k : ℕ
h1 : P 0
h2 : ∀ n ≥ k, P n → P (n + 1)
h3 : Nat.zero ≥ k
h4 : k = 0
⊢ P Nat.zero

case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
exact h1
State after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)

State before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
⊢ ∀ (n : ℕ), (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
fix n
State after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
⊢ (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)

State before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
⊢ (n ≥ k → P n) → Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
assume h3
State after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
⊢ Nat.succ n ≥ k → P (Nat.succ n)

State before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
⊢ Nat.succ n ≥ k → P (Nat.succ n)
Tactic:
assume h4
State after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
⊢ P (Nat.succ n)

State before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
⊢ P (Nat.succ n)
Tactic:
have h5 : k < n + 1 ∨ k = n + 1 := LE.le.lt_or_eq_dec h4
State after:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1 ∨ k = n + 1
⊢ P (Nat.succ n)

State before:
case succ
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1 ∨ k = n + 1
⊢ P (Nat.succ n)
Tactic:
by_cases on h5
State after:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)

State before:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
have h6 : k ≤ n := Nat.le_of_lt_succ h5
State after:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)

State before:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
have h7 := h3 h6
State after:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
h7 : P n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)

State before:
case succ.Case_1
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k < n + 1
h6 : k ≤ n
h7 : P n
⊢ P (Nat.succ n)

case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
exact h2 n h6 h7
State after:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)

State before:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h1 : P k
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
rewrite [h5] at h1
State after:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h1 : P (n + 1)
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)

State before:
case succ.Case_2
P : ℕ → Prop
k : ℕ
h2 : ∀ n ≥ k, P n → P (n + 1)
n : ℕ
h1 : P (n + 1)
h3 : n ≥ k → P n
h4 : Nat.succ n ≥ k
h5 : k = n + 1
⊢ P (Nat.succ n)
Tactic:
exact h1
State after:
no goals