-- Mathlib/Data/List/Perm/Basic.lean
theorem forall₂_comp_perm_eq_perm_comp_forall₂ : Forall₂ r ∘r Perm = Perm ∘r Forall₂ r

Proof state:
case h.h.a.mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
rcases h with ⟨l₂, h₁₂, h₂₃⟩

Result:
case h.h.a.mp.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Proof state:
case h.h.a.mp.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip

Result:
case h.h.a.mp.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
constructor

Result:
case h.h.a.mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

case h.h.a.mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Proof state:
case h.h.a.mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
intro h

Result:
case h.h.a.mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Proof state:
case h.h.a.mp.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩

Result:
case h.h.a.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
l' : List α
h₁ : Forall₂ (flip r) l₃ l'
h₂ : l' ~ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Proof state:
case h.h.a.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
this : Forall₂ (flip r) l₂ l₁
l' : List α
h₁ : Forall₂ (flip r) l₃ l'
h₂ : l' ~ l₁
⊢ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
exact ⟨l', h₂.symm, h₁.flip⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r

Tactic:
funext l₁ l₃

Result:
case h.h
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃

Proof state:
case h.h.a.mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Tactic:
exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
apply propext

Result:
case h.h.a
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃