α : Type u_1
β : Type u_2
γ : Type ?u.134478
f : β → α → β
H : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun x y => f y x) (_ : ∀ (_x _y : α) (_z : β), f (f _z _y) _x = f (f _z _x) _y) x s)
α : Type u_1
β : Type u_2
γ : Type ?u.134478
f : β → α → β
H : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldl f H x s)
rw [foldl_swap]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.134478
f : β → α → β
H : RightCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f b a)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr (fun x y => f y x) (_ : ∀ (_x _y : α) (_z : β), f (f _z _y) _x = f (f _z _x) _y) x s)
exact foldr_induction' (fun x y => f y x) (fun x y z => (H _ _ _).symm) x q p s hpqf px q_s