case empty
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i => if p i then f i else g i) ∅ =
    op (fold op b f (filter p ∅)) (fold op b g (filter (fun i => ¬p i) ∅))

case insert
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
⊢ fold op b (fun i => if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
induction' s using Finset.induction_on with x s hx IH
no goals
case empty
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
⊢ fold op b (fun i => if p i then f i else g i) ∅ =
    op (fold op b f (filter p ∅)) (fold op b g (filter (fun i => ¬p i) ∅))
simp [hb]
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
⊢ op (if p x then f x else g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
⊢ fold op b (fun i => if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
simp only [Finset.fold_insert hx]
case insert.inl
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))

case insert.inr
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
⊢ op (g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
case insert
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
⊢ op (if p x then f x else g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
split_ifs with h
case insert.inl
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
this : ¬x ∈ filter p s
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
case insert.inl
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
have : x ∉ Finset.filter p s := by simp [hx]
no goals
case insert.inl
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
this : ¬x ∈ filter p s
⊢ op (f x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : p x
⊢ ¬x ∈ filter p s
simp [hx]
case insert.inr
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
this : ¬x ∈ filter (fun i => ¬p i) s
⊢ op (g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
case insert.inr
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
⊢ op (g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
no goals
case insert.inr
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
this : ¬x ∈ filter (fun i => ¬p i) s
⊢ op (g x) (fold op b (fun i => if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g (filter (fun i => ¬p i) (insert x s)))
simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.24216
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : ¬x ∈ s
IH :
  fold op b (fun i => if p i then f i else g i) s =
    op (fold op b f (filter p s)) (fold op b g (filter (fun i => ¬p i) s))
h : ¬p x
⊢ ¬x ∈ filter (fun i => ¬p i) s
simp [hx]