-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.pairwise_iff {R : α → α → Prop} (S : ∀ {x y}, R x y → R y x) :
    ∀ {l₁ l₂ : List α} (_p : l₁ ~ l₂), Pairwise R l₁ ↔ Pairwise R l₂ :=
  suffices ∀ {l₁ l₂}, l₁ ~ l₂ → Pairwise R l₁ → Pairwise R l₂
    from fun p => ⟨this p, this p.symm⟩
  fun {l₁ l₂} p d => by
    induction d generalizing l₂ with
    | nil => rw [← p.nil_eq]; constructor
    | cons h _ IH =>
      have : _ ∈ l₂ := p.subset (mem_cons_self _ _)
      obtain ⟨s₂, t₂, rfl⟩ := append_of_mem this
      have p' := (p.trans perm_middle).cons_inv
      refine (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => ?_, IH p'⟩)
      exact h _ (p'.symm.subset m)

Proof state:
case nil
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ l₂ : List α
p : [] ~ l₂
⊢ Pairwise R l₂

Tactic:
rw [← p.nil_eq]

Result:
case nil
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ l₂ : List α
p : [] ~ l₂
⊢ Pairwise R []

Proof state:
case nil
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ l₂ : List α
p : [] ~ l₂
⊢ Pairwise R []

Tactic:
constructor

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a✝¹ :: l✝ ~ l₂
⊢ Pairwise R l₂

Tactic:
have : _ ∈ l₂ := p.subset (mem_cons_self _ _)

Result:
case cons
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a✝¹ :: l✝ ~ l₂
this : a✝¹ ∈ l₂
⊢ Pairwise R l₂

Proof state:
case cons.intro.intro
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a✝¹ :: l✝ ~ s₂ ++ a✝¹ :: t₂
this : a✝¹ ∈ s₂ ++ a✝¹ :: t₂
p' : l✝ ~ s₂ ++ t₂
⊢ Pairwise R (s₂ ++ a✝¹ :: t₂)

Tactic:
refine (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => ?_, IH p'⟩)

Result:
case cons.intro.intro
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a✝¹ :: l✝ ~ s₂ ++ a✝¹ :: t₂
this : a✝¹ ∈ s₂ ++ a✝¹ :: t₂
p' : l✝ ~ s₂ ++ t₂
b : α
m : b ∈ s₂ ++ t₂
⊢ R a✝¹ b

Proof state:
case cons
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
l₂ : List α
p : a✝¹ :: l✝ ~ l₂
this : a✝¹ ∈ l₂
⊢ Pairwise R l₂

Tactic:
obtain ⟨s₂, t₂, rfl⟩ := append_of_mem this

Result:
case cons.intro.intro
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a✝¹ :: l✝ ~ s₂ ++ a✝¹ :: t₂
this : a✝¹ ∈ s₂ ++ a✝¹ :: t₂
⊢ Pairwise R (s₂ ++ a✝¹ :: t₂)

Proof state:
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ l₂ : List α
p : l₁ ~ l₂
d : Pairwise R l₁
⊢ Pairwise R l₂

Tactic:
induction d generalizing l₂ with
| nil => rw [← p.nil_eq]; constructor
| cons h _ IH =>
  have : _ ∈ l₂ := p.subset (mem_cons_self _ _)
  obtain ⟨s₂, t₂, rfl⟩ := append_of_mem this
  have p' := (p.trans perm_middle).cons_inv
  refine (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => ?_, IH p'⟩)
  exact h _ (p'.symm.subset m)

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a✝¹ :: l✝ ~ s₂ ++ a✝¹ :: t₂
this : a✝¹ ∈ s₂ ++ a✝¹ :: t₂
p' : l✝ ~ s₂ ++ t₂
b : α
m : b ∈ s₂ ++ t₂
⊢ R a✝¹ b

Tactic:
exact h _ (p'.symm.subset m)

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a✝¹ :: l✝ ~ s₂ ++ a✝¹ :: t₂
this : a✝¹ ∈ s₂ ++ a✝¹ :: t₂
⊢ Pairwise R (s₂ ++ a✝¹ :: t₂)

Tactic:
have p' := (p.trans perm_middle).cons_inv

Result:
case cons.intro.intro
α : Type u_1
R : α → α → Prop
S : ∀ {x y : α}, R x y → R y x
l₁✝ l₂✝ l₁ : List α
a✝¹ : α
l✝ : List α
h : ∀ (a' : α), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : ∀ {l₂ : List α}, l✝ ~ l₂ → Pairwise R l₂
s₂ t₂ : List α
p : a✝¹ :: l✝ ~ s₂ ++ a✝¹ :: t₂
this : a✝¹ ∈ s₂ ++ a✝¹ :: t₂
p' : l✝ ~ s₂ ++ t₂
⊢ Pairwise R (s₂ ++ a✝¹ :: t₂)