case h.h
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
α : Type uu
β : Type vv
l₁ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
⊢ Forall₂ r ∘r Perm = Perm ∘r Forall₂ r
funext l₁ l₃
case h.h.a
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃
case h.h
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
apply propext
case h.h.a.mp
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

case h.h.a.mpr
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃
case h.h.a
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃
constructor
case h.h.a.mp
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃
case h.h.a.mp
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃
intro h
case h.h.a.mp.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃
case h.h.a.mp
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
h : (Forall₂ r ∘r Perm) l₁ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃
rcases h with ⟨l₂, h₁₂, h₂₃⟩
case h.h.a.mp.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → 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₃
case h.h.a.mp.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ l₂ : List β
h₁₂ : Forall₂ r l₁ l₂
h₂₃ : l₂ ~ l₃
⊢ (Perm ∘r Forall₂ r) l₁ l₃
have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
case h.h.a.mp.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → 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₃
case h.h.a.mp.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → 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₃
rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
no goals
case h.h.a.mp.intro.intro.intro.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → 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₃
exact ⟨l', h₂.symm, h₁.flip⟩
no goals
case h.h.a.mpr
α : Type uu
β : Type vv
l₁✝ l₂ : List α
γ : Type ?u.38852
δ : Type ?u.38855
r : α → β → Prop
p : γ → δ → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃
exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃