Theorem: IsNilpotent.finset_sum (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
s : Finset β
hf : ∀ b ∈ s, IsNilpotent (f b)
⊢ IsNilpotent (s.sum f)
Tactic:
classical
induction s using Finset.induction_on with
  | empty => simp only [Finset.sum_empty, IsNilpotent.zero]
  | @insert b s hb hs =>
    rw [Finset.sum_insert hb]
    apply IsNilpotent.add
    exact hf b (s.mem_insert_self b)
    exact hs (fun b hb ↦ hf b (by exact Finset.mem_insert_of_mem hb))
State after:
no goals

State before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
s : Finset β
hf : ∀ b ∈ s, IsNilpotent (f b)
⊢ IsNilpotent (s.sum f)
Tactic:
induction s using Finset.induction_on with
  | empty => simp only [Finset.sum_empty, IsNilpotent.zero]
  | @insert b s hb hs =>
    rw [Finset.sum_insert hb]
    apply IsNilpotent.add
    exact hf b (s.mem_insert_self b)
    exact hs (fun b hb ↦ hf b (by exact Finset.mem_insert_of_mem hb))
State after:
no goals

State before:
case empty
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
hf : ∀ b ∈ ∅, IsNilpotent (f b)
⊢ IsNilpotent (∅.sum f)
Tactic:
simp only [Finset.sum_empty, IsNilpotent.zero]
State after:
no goals

State before:
case insert
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent ((insert b s).sum f)
Tactic:
rw [Finset.sum_insert hb]
State after:
case insert
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b + ∑ x ∈ s, f x)

State before:
case insert
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b + ∑ x ∈ s, f x)
Tactic:
apply IsNilpotent.add
State after:
case insert.ha
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b)

case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)

State before:
case insert.ha
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (f b)

case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)
Tactic:
exact hf b (s.mem_insert_self b)
State after:
case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)

State before:
case insert.hb
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b : β
s : Finset β
hb : b ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b_1 ∈ insert b s, IsNilpotent (f b_1)
⊢ IsNilpotent (∑ x ∈ s, f x)
Tactic:
exact hs (fun b hb ↦ hf b (by exact Finset.mem_insert_of_mem hb))
State after:
no goals

State before:
α : Type u_1
inst✝ : CommSemiring α
β : Type u_2
f : β → α
b✝ : β
s : Finset β
hb✝ : b✝ ∉ s
hs : (∀ b ∈ s, IsNilpotent (f b)) → IsNilpotent (s.sum f)
hf : ∀ b ∈ insert b✝ s, IsNilpotent (f b)
b : β
hb : b ∈ s
⊢ b ∈ insert b✝ s
Tactic:
exact Finset.mem_insert_of_mem hb
State after:
no goals