case h
F : Type ?u.2925
ι : Type ?u.2928
α : Type u_1
β : Type u_2
γ : Type ?u.2937
f : α → β → β
op : α → α → α
h : LeftCommutative f
b : β
a✝ : List α
⊢ noncommFoldr f (Quotient.mk (List.isSetoid α) a✝)
      (_ :
        ∀ (x : α),
          x ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} →
            ∀ (y : α), y ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} → x ≠ y → ∀ (b : β), f x (f y b) = f y (f x b))
      b =
    foldr f h b (Quotient.mk (List.isSetoid α) a✝)
F : Type ?u.2925
ι : Type ?u.2928
α : Type u_1
β : Type u_2
γ : Type ?u.2937
f : α → β → β
op : α → α → α
s : Multiset α
h : LeftCommutative f
b : β
⊢ noncommFoldr f s
      (_ : ∀ (x : α), x ∈ {x | x ∈ s} → ∀ (y : α), y ∈ {x | x ∈ s} → x ≠ y → ∀ (b : β), f x (f y b) = f y (f x b)) b =
    foldr f h b s
induction s using Quotient.inductionOn
no goals
case h
F : Type ?u.2925
ι : Type ?u.2928
α : Type u_1
β : Type u_2
γ : Type ?u.2937
f : α → β → β
op : α → α → α
h : LeftCommutative f
b : β
a✝ : List α
⊢ noncommFoldr f (Quotient.mk (List.isSetoid α) a✝)
      (_ :
        ∀ (x : α),
          x ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} →
            ∀ (y : α), y ∈ {x | x ∈ Quotient.mk (List.isSetoid α) a✝} → x ≠ y → ∀ (b : β), f x (f y b) = f y (f x b))
      b =
    foldr f h b (Quotient.mk (List.isSetoid α) a✝)
simp