-- 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:
β : Type u_1
α : Type u_2
f : β → α → β
l₁ l₂ : List α
p : l₁ ~ l₂
comm : ∀ (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₂

Tactic:
induction p using recOnSwap' generalizing init with
| nil => simp
| cons x _p IH =>
  simp only [foldl]
  apply IH; intros; apply comm <;> exact .tail _ ‹_›
| swap' x y _p IH =>
  simp only [foldl]
  rw [comm x (.tail _ <| .head _) y (.head _)]
  apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
| trans p₁ _p₂ IH₁ IH₂ =>
  refine (IH₁ comm init).trans (IH₂ ?_ _)
  intros; apply comm <;> apply p₁.symm.subset <;> assumption

Result:
no goals

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 init (y :: x :: l₁✝) = foldl f init (x :: y :: l₂✝)

Tactic:
simp only [foldl]

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 x) y) l₂✝

Proof state:
case swap'.comm
β : 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 : β
⊢ ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x

Tactic:
intros

Result:
case swap'.comm
β : 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 : β
x✝ : α
a✝¹ : x✝ ∈ l₁✝
y✝ : α
a✝ : y✝ ∈ l₁✝
z✝ : β
⊢ f (f z✝ x✝) y✝ = f (f z✝ y✝) x✝

Proof state:
case swap'.comm
β : 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 : β
x✝ : α
a✝¹ : x✝ ∈ l₁✝
y✝ : α
a✝ : y✝ ∈ l₁✝
z✝ : β
⊢ f (f z✝ x✝) y✝ = f (f z✝ y✝) x✝

Tactic:
apply comm <;> exact .tail _ (.tail _ ‹_›)

Result:
no goals

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 : β
⊢ foldl f init l₁✝ = foldl f init l₃✝

Tactic:
refine (IH₁ comm init).trans (IH₂ ?_ _)

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 : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f (f z x) y = f (f z y) x

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✝ : α
a✝¹ : x✝ ∈ l₁✝
y✝ : α
a✝ : y✝ ∈ l₁✝
z✝ : β
⊢ f (f z✝ x✝) y✝ = f (f z✝ y✝) x✝

Tactic:
apply comm <;> exact .tail _ ‹_›

Result:
no goals

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✝ : α
a✝¹ : x✝ ∈ l₂✝
y✝ : α
a✝ : y✝ ∈ l₂✝
z✝ : β
⊢ f (f z✝ x✝) y✝ = f (f z✝ y✝) x✝

Tactic:
apply comm <;> apply p₁.symm.subset <;> assumption

Result:
no goals

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 init (x :: l₁✝) = foldl f init (x :: l₂✝)

Tactic:
simp only [foldl]

Result:
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₂✝

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 y) x) l₂✝

Tactic:
apply IH

Result:
case swap'.comm
β : 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 : β
⊢ ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f (f z x) y = f (f z y) x