-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_comp_forall₂ {l u v} (hlu : Perm l u) (huv : Forall₂ r u v) :
    (Forall₂ r ∘r Perm) l v

Proof state:
case trans
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩

Result:
case trans.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Proof state:
case swap.cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝¹ : β
h₁ : r a₁ b✝¹
b✝ : β
l₂✝ : List β
h₂ : r a₂ b✝
h₁₂ : Forall₂ r h₂₃ l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝¹ :: b✝ :: l₂✝)

Tactic:
exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩

Result:
no goals

Proof state:
case trans.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
lb₁ : List β
hab₁ : Forall₂ r l₁✝ lb₁
h₁₂ : lb₁ ~ lb₂
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
huv : Forall₂ r [] v
⊢ (Forall₂ r ∘r Perm) [] v

Tactic:
cases huv

Result:
case nil.nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []

Proof state:
case trans.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
⊢ (Forall₂ r ∘r Perm) l₁✝ v

Tactic:
rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩

Result:
case trans.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l u l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
ih₂ : ∀ {v : List β}, Forall₂ r l₃✝ v → (Forall₂ r ∘r Perm) l₂✝ v
v : List β
huv : Forall₂ r l₃✝ v
lb₂ : List β
hab₂ : Forall₂ r l₂✝ lb₂
h₂₃ : lb₂ ~ v
lb₁ : List β
hab₁ : Forall₂ r l₁✝ lb₁
h₁₂ : lb₁ ~ lb₂
⊢ (Forall₂ r ∘r Perm) l₁✝ v

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

Tactic:
obtain - | ⟨h₁, hr₂₃⟩ := huv

Result:
case swap.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝ : β
l₂✝ : List β
h₁ : r a₁ b✝
hr₂₃ : Forall₂ r (a₂ :: h₂₃) l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝ :: l₂✝)

Proof state:
case swap.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝ : β
l₂✝ : List β
h₁ : r a₁ b✝
hr₂₃ : Forall₂ r (a₂ :: h₂₃) l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝ :: l₂✝)

Tactic:
obtain - | ⟨h₂, h₁₂⟩ := hr₂₃

Result:
case swap.cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝¹ : β
h₁ : r a₁ b✝¹
b✝ : β
l₂✝ : List β
h₂ : r a₂ b✝
h₁₂ : Forall₂ r h₂₃ l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝¹ :: b✝ :: l₂✝)

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)

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

Result:
case cons.cons.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
l₂ : List β
h₁₂ : Forall₂ r l₁✝ l₂
h₂₃ : l₂ ~ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)

Proof state:
case nil.nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []

Tactic:
exact ⟨[], Forall₂.nil, Perm.nil⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝ : List α
_hlu : l₁✝ ~ l₂✝
ih : ∀ {v : List β}, Forall₂ r l₂✝ v → (Forall₂ r ∘r Perm) l₁✝ v
v : List β
huv : Forall₂ r (u :: l₂✝) v
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) v

Tactic:
obtain - | ⟨hab, huv'⟩ := huv

Result:
case cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)

Proof state:
case cons.cons.intro.intro
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
l₂ : List β
h₁₂ : Forall₂ r l₁✝ l₂
h₂₃ : l₂ ~ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)

Tactic:
exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
v : List β
hlu : l ~ u
huv : Forall₂ r u v
⊢ (Forall₂ r ∘r Perm) l v

Tactic:
induction hlu generalizing v with
| nil => cases huv; exact ⟨[], Forall₂.nil, Perm.nil⟩
| cons u _hlu ih =>
  obtain - | ⟨hab, huv'⟩ := huv
  rcases ih huv' with ⟨l₂, h₁₂, h₂₃⟩
  exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩
| swap a₁ a₂ h₂₃ =>
  obtain - | ⟨h₁, hr₂₃⟩ := huv
  obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
  exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩
| trans _ _ ih₁ ih₂ =>
  rcases ih₂ huv with ⟨lb₂, hab₂, h₂₃⟩
  rcases ih₁ hab₂ with ⟨lb₁, hab₁, h₁₂⟩
  exact ⟨lb₁, hab₁, Perm.trans h₁₂ h₂₃⟩

Result:
no goals