α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ ∀ (s : Multiset α), (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
s : Multiset α
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
q_s : ∀ (a : α), a ∈ s → q a
⊢ p (foldr f H x s)
revert s
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → q a) → p (foldr f H x s)) → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → q a_2) → p (foldr f H x (a ::ₘ s))
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ ∀ (s : Multiset α), (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
refine' Multiset.induction (by simp [px]) _
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (foldr f H x (a ::ₘ s))
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ((∀ (a : α), a ∈ s → q a) → p (foldr f H x s)) → (∀ (a_2 : α), a_2 ∈ a ::ₘ s → q a_2) → p (foldr f H x (a ::ₘ s))
intro a s hs hsa
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (f a (foldr f H x s))
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (foldr f H x (a ::ₘ s))
rw [foldr_cons]
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
hps : ∀ (x : α), x ∈ s → q x
⊢ p (f a (foldr f H x s))
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (f a (foldr f H x s))
have hps : ∀ x : α, x ∈ s → q x := fun x hxs => hsa x (mem_cons_of_mem hxs)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → q a) → p (foldr f H x s)
hsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
hps : ∀ (x : α), x ∈ s → q x
⊢ p (f a (foldr f H x s))
exact hpqf a (foldr f H x s) (hsa a (mem_cons_self a s)) (hs hps)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.132443
f : α → β → β
H : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
⊢ (∀ (a : α), a ∈ 0 → q a) → p (foldr f H x 0)
simp [px]