-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.foldr_eq' {f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f y (f x z) = f x (f y z))
    (init) : foldr f init l₁ = foldr f init 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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₂✝ = foldr f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f y (f x z) = f x (f y z)
init : β
x✝ : α
a✝¹ : x✝ ∈ l₂✝
y✝ : α
a✝ : y✝ ∈ l₂✝
z✝ : β
⊢ f y✝ (f x✝ z✝) = f x✝ (f y✝ z✝)

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

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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₂✝ = foldr f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f y (f x z) = f x (f y z)
init : β
⊢ ∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)

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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₂✝ = foldr f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f y (f x z) = f x (f y z)
init : β
x✝ : α
a✝¹ : x✝ ∈ l₂✝
y✝ : α
a✝ : y✝ ∈ l₂✝
z✝ : β
⊢ f y✝ (f x✝ z✝) = f x✝ (f y✝ z✝)

Proof state:
case cons.e_a.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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
comm : ∀ (x_1 : α), x_1 ∈ x :: l₁✝ → ∀ (y : α), y ∈ x :: l₁✝ → ∀ (z : β), f y (f x_1 z) = f x_1 (f y z)
init : β
x✝ : α
a✝¹ : x✝ ∈ l₁✝
y✝ : α
a✝ : y✝ ∈ l₁✝
z✝ : β
⊢ f y✝ (f x✝ z✝) = f x✝ (f y✝ z✝)

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

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
p : l₁ ~ l₂
comm : ∀ (x : α), x ∈ l₁ → ∀ (y : α), y ∈ l₁ → ∀ (z : β), f y (f x z) = f x (f y z)
init : β
⊢ foldr f init l₁ = foldr f init l₂

Tactic:
induction p using recOnSwap' generalizing init with
| nil => simp
| cons x _p IH =>
  simp only [foldr]
  congr 1
  apply IH; intros; apply comm <;> exact .tail _ ‹_›
| swap' x y _p IH =>
  simp only [foldr]
  rw [comm x (.tail _ <| .head _) y (.head _)]
  congr 2
  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'.e_a.e_a.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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
comm :
  ∀ (x_1 : α), x_1 ∈ y :: x :: l₁✝ → ∀ (y_1 : α), y_1 ∈ y :: x :: l₁✝ → ∀ (z : β), f y_1 (f x_1 z) = f x_1 (f y_1 z)
init : β
⊢ ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f y (f x z) = f x (f y z)

Tactic:
intros

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

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

Tactic:
simp

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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₂✝ = foldr f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f y (f x z) = f x (f y z)
init : β
⊢ foldr f init l₁✝ = foldr 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 y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₁✝ = foldr f init l₂✝
IH₂ :
  (∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)) →
    ∀ (init : β), foldr f init l₂✝ = foldr f init l₃✝
comm : ∀ (x : α), x ∈ l₁✝ → ∀ (y : α), y ∈ l₁✝ → ∀ (z : β), f y (f x z) = f x (f y z)
init : β
⊢ ∀ (x : α), x ∈ l₂✝ → ∀ (y : α), y ∈ l₂✝ → ∀ (z : β), f y (f x z) = f x (f y z)

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

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

Result:
no goals