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

Tactic:
simp only [foldr]

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

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

Tactic:
intros

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

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

Tactic:
congr 2

Result:
case swap'.e_a.e_a
α : 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 : β
⊢ foldr f init l₁✝ = foldr f init 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 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 : β
⊢ foldr f init (y :: x :: l₁✝) = foldr f init (x :: y :: l₂✝)

Tactic:
simp only [foldr]

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

Proof state:
case swap'.e_a.e_a
α : 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 : β
⊢ foldr f init l₁✝ = foldr f init l₂✝

Tactic:
apply IH

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

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

Tactic:
congr 1

Result:
case cons.e_a
α : 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 : β
⊢ foldr f init l₁✝ = foldr f init l₂✝

Proof state:
case cons.e_a
α : 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 : β
⊢ foldr f init l₁✝ = foldr f init l₂✝

Tactic:
apply IH

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