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

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

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
⊢ (sum_seq (n + 1 - k) k fun i => f i) = 0
Tactic:
have h2 : n + 1 - k = 0 := Nat.sub_eq_zero_of_le h
State after:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
h2 : n + 1 - k = 0
⊢ (sum_seq (n + 1 - k) k fun i => f i) = 0

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

State before:
A : Type
inst✝ : AddZeroClass A
k n : ℕ
f : ℕ → A
h : n < k
h2 : n + 1 - k = 0
⊢ (sum_seq 0 k fun i => f i) = 0
Tactic:
rfl
State after:
no goals