-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x)
    (init) : foldl f init l₁ = foldl f init l₂

Proof state:
case cons.comm
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
comm : ∀ (x_1 : α), x_1 ∈ x :: l₁✝ → ∀ (y : α), y ∈ x :: l₁✝ → ∀ (z : β), f (f z x_1) y = f (f z y) x_1
init : β
⊢ ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x

Tactic:
intros

Result:
case cons.comm
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
comm : ∀ (x_1 : α), x_1 ∈ x :: l₁✝ → ∀ (y : α), y ∈ x :: l₁✝ → ∀ (z : β), f (f z x_1) y = f (f z y) x_1
init : β
x✝ : α
a✝¹ : x✝ ∈ l₁✝
y✝ : α
a✝ : y✝ ∈ l₁✝
z✝ : β
⊢ f (f z✝ x✝) y✝ = f (f z✝ y✝) x✝

Proof state:
case cons
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
comm : ∀ (x_1 : α), x_1 ∈ x :: l₁✝ → ∀ (y : α), y ∈ x :: l₁✝ → ∀ (z : β), f (f z x_1) y = f (f z y) x_1
init : β
⊢ foldl f (f init x) l₁✝ = foldl f (f init x) l₂✝

Tactic:
apply IH

Result:
case cons.comm
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
comm : ∀ (x_1 : α), x_1 ∈ x :: l₁✝ → ∀ (y : α), y ∈ x :: l₁✝ → ∀ (z : β), f (f z x_1) y = f (f z y) x_1
init : β
⊢ ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x

Proof state:
case swap'
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
x y : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
comm :
  ∀ (x_1 : α), x_1 ∈ y :: x :: l₁✝ → ∀ (y_1 : α), y_1 ∈ y :: x :: l₁✝ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
init : β
⊢ foldl f (f (f init y) x) l₁✝ = foldl f (f (f init x) y) l₂✝

Tactic:
rw [comm x (.tail _ <| .head _) y (.head _)]

Result:
case swap'
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
x y : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
comm :
  ∀ (x_1 : α), x_1 ∈ y :: x :: l₁✝ → ∀ (y_1 : α), y_1 ∈ y :: x :: l₁✝ → ∀ (z : β), f (f z x_1) y_1 = f (f z y_1) x_1
init : β
⊢ foldl f (f (f init y) x) l₁✝ = foldl f (f (f init y) x) l₂✝

Proof state:
case trans
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
_p₂ : l₂✝ ~ l₃✝
IH₁ :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₂✝ = foldl f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x
init : β
⊢ ∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f (f z x) y = f (f z y) x

Tactic:
intros

Result:
case trans
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
p₁ : l₁✝ ~ l₂✝
_p₂ : l₂✝ ~ l₃✝
IH₁ :
  (∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₁✝ = foldl f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f (f z x) y = f (f z y) x) →
    ∀ (init : β), foldl f init l₂✝ = foldl f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x
init : β
x✝ : α
a✝¹ : x✝ ∈ l₂✝
y✝ : α
a✝ : y✝ ∈ l₂✝
z✝ : β
⊢ f (f z✝ x✝) y✝ = f (f z✝ y✝) x✝

Proof state:
case nil
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
comm : ∀ (x : α), x ∈ [] → ∀ (y : α), y ∈ [] → ∀ (z : β), f (f z x) y = f (f z y) x
init : β
⊢ foldl f init [] = foldl f init []

Tactic:
simp

Result:
no goals