α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : β → α → β
l₁ l₂ : List α
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r :
  (∀ (x : α), x ∈ t₁ → ∀ (y : α), y ∈ t₁ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (b : β), foldl f b t₁ = foldl f b t₂
H : ∀ (x_1 : α), x_1 ∈ y :: x :: t₁ → ∀ (y_1 : α), y_1 ∈ y :: x :: t₁ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
b : β
⊢ foldl f (f (f b y) x) t₁ = foldl f (f (f b x) y) t₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : β → α → β
l₁ l₂ : List α
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r :
  (∀ (x : α), x ∈ t₁ → ∀ (y : α), y ∈ t₁ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (b : β), foldl f b t₁ = foldl f b t₂
H : ∀ (x_1 : α), x_1 ∈ y :: x :: t₁ → ∀ (y_1 : α), y_1 ∈ y :: x :: t₁ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
b : β
⊢ foldl f b (y :: x :: t₁) = foldl f b (x :: y :: t₂)
simp only [foldl]
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : β → α → β
l₁ l₂ : List α
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r :
  (∀ (x : α), x ∈ t₁ → ∀ (y : α), y ∈ t₁ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (b : β), foldl f b t₁ = foldl f b t₂
H : ∀ (x_1 : α), x_1 ∈ y :: x :: t₁ → ∀ (y_1 : α), y_1 ∈ y :: x :: t₁ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
b : β
⊢ foldl f (f (f b y) x) t₁ = foldl f (f (f b y) x) t₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : β → α → β
l₁ l₂ : List α
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r :
  (∀ (x : α), x ∈ t₁ → ∀ (y : α), y ∈ t₁ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (b : β), foldl f b t₁ = foldl f b t₂
H : ∀ (x_1 : α), x_1 ∈ y :: x :: t₁ → ∀ (y_1 : α), y_1 ∈ y :: x :: t₁ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
b : β
⊢ foldl f (f (f b y) x) t₁ = foldl f (f (f b x) y) t₂
rw [H x (.tail _ <| .head _) y (.head _)]
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : β → α → β
l₁ l₂ : List α
p : l₁ ~ l₂
x y : α
t₁ t₂ : List α
_p : t₁ ~ t₂
r :
  (∀ (x : α), x ∈ t₁ → ∀ (y : α), y ∈ t₁ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (b : β), foldl f b t₁ = foldl f b t₂
H : ∀ (x_1 : α), x_1 ∈ y :: x :: t₁ → ∀ (y_1 : α), y_1 ∈ y :: x :: t₁ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
b : β
⊢ foldl f (f (f b y) x) t₁ = foldl f (f (f b y) x) t₂
exact r (fun x hx y hy => H _ (.tail _ <| .tail _ hx) _ (.tail _ <| .tail _ hy)) _