α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
⊢ ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid
letI := Classical.decEq β
case refine'_1
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x in ∅, slice (f x) i hid = slice (∑ x in ∅, f x) i hid

case refine'_2
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s →
      ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid →
        ∑ x in insert a s, slice (f x) i hid = slice (∑ x in insert a s, f x) i hid
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid
refine' Finset.induction_on s _ _
no goals
case refine'_1
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x in ∅, slice (f x) i hid = slice (∑ x in ∅, f x) i hid
simp [slice_zero]
case refine'_2
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : ¬a✝ ∈ s✝
ih : ∑ x in s✝, slice (f x) i hid = slice (∑ x in s✝, f x) i hid
⊢ ∑ x in insert a✝ s✝, slice (f x) i hid = slice (∑ x in insert a✝ s✝, f x) i hid
case refine'_2
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s →
      ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid →
        ∑ x in insert a s, slice (f x) i hid = slice (∑ x in insert a s, f x) i hid
intro _ _ h_not_in ih
no goals
case refine'_2
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : ¬a✝ ∈ s✝
ih : ∑ x in s✝, slice (f x) i hid = slice (∑ x in s✝, f x) i hid
⊢ ∑ x in insert a✝ s✝, slice (f x) i hid = slice (∑ x in insert a✝ s✝, f x) i hid
rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]