α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
x : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r : ∀ (b : β), foldr f b t₁ = foldr f b t₂
b : β
⊢ f x (foldr f b t₁) = f x (foldr f b t₂)
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
x : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r : ∀ (b : β), foldr f b t₁ = foldr f b t₂
b : β
⊢ foldr f b (x :: t₁) = foldr f b (x :: t₂)
simp
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
x : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r : ∀ (b : β), foldr f b t₁ = foldr f b t₂
b : β
⊢ f x (foldr f b t₁) = f x (foldr f b t₂)
rw [r b]
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r : ∀ (b : β), foldr f b t₁ = foldr f b t₂
b : β
⊢ f y (f x (foldr f b t₁)) = f x (f y (foldr f b t₂))
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r : ∀ (b : β), foldr f b t₁ = foldr f b t₂
b : β
⊢ foldr f b (y :: x :: t₁) = foldr f b (x :: y :: t₂)
simp
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r : ∀ (b : β), foldr f b t₁ = foldr f b t₂
b : β
⊢ f y (f x (foldr f b t₁)) = f x (f y (foldr f b t₂))
rw [lcomm, r b]