[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
h : ¬a ∈ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)
[PROOFSTEP]
dsimp only [fold]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
h : ¬a ∈ s
⊢ Multiset.fold op b (Multiset.map f (cons a s h).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
[PROOFSTEP]
rw [cons_val, Multiset.map_cons, fold_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
unfold fold
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
[PROOFSTEP]
rw [insert_val, ndinsert_of_not_mem h, Multiset.map_cons, fold_cons_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ ↑g) s
[PROOFSTEP]
simp only [fold, map, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
H : ∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
[PROOFSTEP]
simp only [fold, image_val_of_injOn H, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
H : ∀ (x : α), x ∈ s → f x = g x
⊢ fold op b f s = fold op b g s
[PROOFSTEP]
rw [fold, fold, map_congr rfl H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f✝ : α → β
b : β
s : Finset α
a : α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)
[PROOFSTEP]
simp only [fold, fold_distrib]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x => c) s = if s = ∅ then b else op b c
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hx IH generalizing hd
· simp
· simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
  split_ifs
  · rw [hc.comm]
  · exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
⊢ fold op b (fun x => c) s = if s = ∅ then b else op b c
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH generalizing hd
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
hd✝ : Decidable (s = ∅)
c : β
h : op c (op b c) = op b c
hd : Decidable (∅ = ∅)
⊢ fold op b (fun x => c) ∅ = if ∅ = ∅ then b else op b c
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ fold op b (fun x => c) (insert x s) = if insert x s = ∅ then b else op b c
[PROOFSTEP]
simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
⊢ op c (if s = ∅ then b else op b c) = op b c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c
[PROOFSTEP]
rw [hc.comm]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
hd✝ : Decidable (s✝ = ∅)
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : ¬x ∈ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x => c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x => m (f x)) s = m (fold op b f s)
[PROOFSTEP]
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)
[PROOFSTEP]
unfold fold
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
[PROOFSTEP]
rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add, hc.comm, fold_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
rw [← insert_erase h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : a ∈ s
⊢ fold op b f (insert a (insert a (erase s a))) = op (f a) (fold op b f (insert a (erase s a)))
[PROOFSTEP]
simp [← ha.assoc, hi.idempotent]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : IsIdempotent β op
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
[PROOFSTEP]
apply fold_insert h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
hi : IsIdempotent β op
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
[PROOFSTEP]
induction' s using Finset.cons_induction with x xs hx ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
⊢ fold op b f (image g ∅) = fold op b (f ∘ g) ∅
[PROOFSTEP]
rw [fold_empty, image_empty, fold_empty]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
[PROOFSTEP]
haveI := Classical.decEq γ
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)
[PROOFSTEP]
rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
hi : IsIdempotent β op
x : γ
xs : Finset γ
hx : ¬x ∈ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
classical
induction' s using Finset.induction_on with x s hx IH
· simp [hb]
· simp only [Finset.fold_insert hx]
  split_ifs with h
  · have : x ∉ Finset.filter p s := by simp [hx]
    simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
  · have : x ∉ Finset.filter (fun i => ¬p i) s := by simp [hx]
    simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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))
[PROOFSTEP]
induction' s using Finset.induction_on with x s hx IH
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
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) ∅))
[PROOFSTEP]
simp [hb]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
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)))
[PROOFSTEP]
simp only [Finset.fold_insert hx]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
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)))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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)))
[PROOFSTEP]
have : x ∉ Finset.filter p s := by simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp [hx]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
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)))
[PROOFSTEP]
simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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)))
[PROOFSTEP]
have : x ∉ Finset.filter (fun i => ¬p i) s := by simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
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
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
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)))
[PROOFSTEP]
simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha IH
· simp
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
apply and_congr Iff.rfl
constructor
· rintro ⟨h₁, h₂⟩
  intro b hb
  rw [Finset.mem_insert] at hb 
  rcases hb with (rfl | hb) <;> solve_by_elim
· intro h
  constructor
  · exact h a (Finset.mem_insert_self _ _)
  · exact fun b hb => h b <| Finset.mem_insert_of_mem hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha IH
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∧ ∀ (x : α), x ∈ ∅ → r c (f x)
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)) ↔ r c b ∧ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
apply and_congr Iff.rfl
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)) ↔ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)) → ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case insert.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
⊢ ∀ (x : α), x ∈ insert a s → r c (f x)
[PROOFSTEP]
intro b hb
[GOAL]
case insert.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
hb : b ∈ insert a s
⊢ r c (f b)
[PROOFSTEP]
rw [Finset.mem_insert] at hb 
[GOAL]
case insert.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
hb : b = a ∨ b ∈ s
⊢ r c (f b)
[PROOFSTEP]
rcases hb with (rfl | hb)
[GOAL]
case insert.mp.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
s : Finset α
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
ha : ¬b ∈ s
h₁ : r c (f b)
⊢ r c (f b)
[PROOFSTEP]
solve_by_elim
[GOAL]
case insert.mp.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b✝ : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b✝ f s) ↔ r c b✝ ∧ ∀ (x : α), x ∈ s → r c (f x)
h₁ : r c (f a)
h₂ : ∀ (x : α), x ∈ s → r c (f x)
b : α
hb : b ∈ s
⊢ r c (f b)
[PROOFSTEP]
solve_by_elim
[GOAL]
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
⊢ (∀ (x : α), x ∈ insert a s → r c (f x)) → r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
intro h
[GOAL]
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h : ∀ (x : α), x ∈ insert a s → r c (f x)
⊢ r c (f a) ∧ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
constructor
[GOAL]
case insert.mpr.left
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h : ∀ (x : α), x ∈ insert a s → r c (f x)
⊢ r c (f a)
[PROOFSTEP]
exact h a (Finset.mem_insert_self _ _)
[GOAL]
case insert.mpr.right
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ (x : α), x ∈ s → r c (f x)
h : ∀ (x : α), x ∈ insert a s → r c (f x)
⊢ ∀ (x : α), x ∈ s → r c (f x)
[PROOFSTEP]
exact fun b hb => h b <| Finset.mem_insert_of_mem hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s ha IH
· simp
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
apply or_congr Iff.rfl
constructor
· rintro (h₁ | ⟨x, hx, h₂⟩)
  · use a
    simp [h₁]
  · refine' ⟨x, by simp [hx], h₂⟩
· rintro ⟨x, hx, h⟩
  exact (mem_insert.mp hx).imp (fun hx => by rwa [hx] at h ) (fun hx => ⟨x, hx, h⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
induction' s using Finset.induction_on with a s ha IH
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∨ ∃ x, x ∈ ∅ ∧ r c (f x)
[PROOFSTEP]
simp
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
apply or_congr Iff.rfl
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) → ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
rintro (h₁ | ⟨x, hx, h₂⟩)
[GOAL]
case insert.mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ a ∈ insert a s ∧ r c (f a)
[PROOFSTEP]
simp [h₁]
[GOAL]
case insert.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
[PROOFSTEP]
refine' ⟨x, by simp [hx], h₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ x ∈ insert a s
[PROOFSTEP]
simp [hx]
[GOAL]
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (∃ x, x ∈ insert a s ∧ r c (f x)) → r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
rintro ⟨x, hx, h⟩
[GOAL]
case insert.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ insert a s
h : r c (f x)
⊢ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
[PROOFSTEP]
exact (mem_insert.mp hx).imp (fun hx => by rwa [hx] at h ) (fun hx => ⟨x, hx, h⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx✝ : x ∈ insert a s
h : r c (f x)
hx : x = a
⊢ r c (f a)
[PROOFSTEP]
rwa [hx] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
s : Finset α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
[PROOFSTEP]
induction' s using Finset.induction_on with a s has ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton ∅ = ∅
[PROOFSTEP]
simp only [fold_empty]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
inst✝ : DecidableEq α
a : α
s : Finset α
has : ¬a ∈ s
ih : fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
⊢ fold (fun x x_1 => x ∪ x_1) ∅ singleton (insert a s) = insert a s
[PROOFSTEP]
rw [fold_insert has, ih, insert_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
[PROOFSTEP]
show _ ≥ _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold min b f s ↔ b ≤ c ∨ ∃ x, x ∈ s ∧ f x ≤ c
[PROOFSTEP]
apply fold_op_rel_iff_or
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ min y z ↔ x ≥ y ∨ x ≥ z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ min y z ↔ x ≥ y ∨ x ≥ z
[PROOFSTEP]
show _ ≤ _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z ≤ x ↔ x ≥ y ∨ x ≥ z
[PROOFSTEP]
exact min_le_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s < c ↔ b < c ∨ ∃ x, x ∈ s ∧ f x < c
[PROOFSTEP]
show _ > _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c > fold min b f s ↔ b < c ∨ ∃ x, x ∈ s ∧ f x < c
[PROOFSTEP]
apply fold_op_rel_iff_or
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > min y z ↔ x > y ∨ x > z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x > min y z ↔ x > y ∨ x > z
[PROOFSTEP]
show _ < _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z < x ↔ x > y ∨ x > z
[PROOFSTEP]
exact min_lt_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ (x : α), x ∈ s → f x ≤ c
[PROOFSTEP]
show _ ≥ _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ (x : α), x ∈ s → f x ≤ c
[PROOFSTEP]
apply fold_op_rel_iff_and
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ max y z ↔ x ≥ y ∧ x ≥ z
[PROOFSTEP]
show _ ≤ _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z ≤ x ↔ x ≥ y ∧ x ≥ z
[PROOFSTEP]
exact max_le_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s < c ↔ b < c ∧ ∀ (x : α), x ∈ s → f x < c
[PROOFSTEP]
show _ > _ ↔ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ c > fold max b f s ↔ b < c ∧ ∀ (x : α), x ∈ s → f x < c
[PROOFSTEP]
apply fold_op_rel_iff_and
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x > max y z ↔ x > y ∧ x > z
[PROOFSTEP]
intro x y z
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ x > max y z ↔ x > y ∧ x > z
[PROOFSTEP]
show _ < _ ↔ _
[GOAL]
case hr
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : LinearOrder β
c x y z : β
⊢ max y z < x ↔ x > y ∧ x > z
[PROOFSTEP]
exact max_lt_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
s : Finset α
⊢ fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
[PROOFSTEP]
classical induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
s : Finset α
⊢ fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
[PROOFSTEP]
induction' s using Finset.induction_on with a s _ ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
⊢ fold max ⊥ (fun x => ↑(f x) + n) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + n
[PROOFSTEP]
simp [*, max_add_add_right]
[GOAL]
case insert
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝¹ : α
inst✝² : LinearOrder β
c : β
inst✝¹ : Add β
inst✝ : CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : WithBot β
a : α
s : Finset α
a✝ : ¬a ∈ s
ih : fold max ⊥ (fun x => ↑(f x) + n) s = fold max ⊥ (WithBot.some ∘ f) s + n
⊢ fold max ⊥ (fun x => ↑(f x) + n) (insert a s) = fold max ⊥ (WithBot.some ∘ f) (insert a s) + n
[PROOFSTEP]
simp [*, max_add_add_right]
