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

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

State before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq (k + 1 - k) k fun i => f i) = f k
Tactic:
rewrite [Nat.add_sub_cancel_left]
State after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq 1 k fun i => f i) = f k

State before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ (sum_seq 1 k fun i => f i) = f k
Tactic:
rewrite [sum_seq, sum_seq]
State after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ 0 + f (k + 0) = f k

State before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ 0 + f (k + 0) = f k
Tactic:
rewrite [zero_add, add_zero]
State after:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ f k = f k

State before:
A : Type
inst✝ : AddZeroClass A
k : ℕ
f : ℕ → A
⊢ f k = f k
Tactic:
rfl
State after:
no goals