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

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
⊢ Sum i from k to n + 1, f i = (Sum i from k to n, f i) + f (n + 1)
Tactic:
define : Sum i from k to (n + 1), f i
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
obtain j h1 from Nat.le.dest h
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
have h2 : n + 1 + 1 - k = n + 1 - k + 1 := by
  rewrite [←h1, add_assoc, add_assoc, Nat.add_sub_cancel_left,
    add_assoc, Nat.add_sub_cancel_left, add_assoc]
  rfl
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
have h3 : f (n + 1) = f (k + (n + 1 - k)) := by
  rewrite [←h1, add_assoc, Nat.add_sub_cancel_left]
  rfl
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 + 1 - k) k fun i => f i) = (Sum i from k to n, f i) + f (n + 1)
Tactic:
rewrite [h2, h3]
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 - k + 1) k fun i => f i) = (Sum i from k to n, f i) + f (k + (n + 1 - k))

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
h3 : f (n + 1) = f (k + (n + 1 - k))
⊢ (sum_seq (n + 1 - k + 1) k fun i => f i) = (Sum i from k to n, f i) + f (k + (n + 1 - k))
Tactic:
rfl
State after:
no goals

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ n + 1 + 1 - k = n + 1 - k + 1
Tactic:
rewrite [←h1, add_assoc, add_assoc, Nat.add_sub_cancel_left,
  add_assoc, Nat.add_sub_cancel_left, add_assoc]
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ j + (1 + 1) = j + (1 + 1)

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
⊢ j + (1 + 1) = j + (1 + 1)
Tactic:
rfl
State after:
no goals

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ f (n + 1) = f (k + (n + 1 - k))
Tactic:
rewrite [←h1, add_assoc, Nat.add_sub_cancel_left]
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ f (k + (j + 1)) = f (k + (j + 1))

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : k ≤ n
j : ℕ
h1 : k + j = n
h2 : n + 1 + 1 - k = n + 1 - k + 1
⊢ f (k + (j + 1)) = f (k + (j + 1))
Tactic:
rfl
State after:
no goals