case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []
⊢ lookmap f [] ~ lookmap f []

case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
⊢ lookmap f (a :: l₁) ~ lookmap f (a :: l₂)

case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
IH₂ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂ → lookmap f l₂ ~ lookmap f l₃
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
⊢ lookmap f l₁ ~ lookmap f l₃
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
p : l₁ ~ l₂
⊢ lookmap f l₁ ~ lookmap f l₂
induction' p with a l₁ l₂ p IH a b l l₁ l₂ l₃ p₁ _ IH₁ IH₂
no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []
⊢ lookmap f [] ~ lookmap f []
simp
case cons.none
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
h : f a = none
⊢ lookmap f (a :: l₁) ~ lookmap f (a :: l₂)

case cons.some
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
val✝ : α
h : f a = some val✝
⊢ lookmap f (a :: l₁) ~ lookmap f (a :: l₂)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
⊢ lookmap f (a :: l₁) ~ lookmap f (a :: l₂)
cases h : f a
case cons.none
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
h : f a = none
⊢ lookmap f l₁ ~ lookmap f l₂
case cons.none
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
h : f a = none
⊢ lookmap f (a :: l₁) ~ lookmap f (a :: l₂)
simp [h]
no goals
case cons.none
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
h : f a = none
⊢ lookmap f l₁ ~ lookmap f l₂
exact IH (pairwise_cons.1 H).2
no goals
case cons.some
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
IH : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)
val✝ : α
h : f a = some val✝
⊢ lookmap f (a :: l₁) ~ lookmap f (a :: l₂)
simp [lookmap_cons_some _ _ h, p]
case swap.none.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.none.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.some.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.some.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
cases' h₁ : f a with c <;> cases' h₂ : f b with d
case swap.none.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ b :: a :: lookmap f l ~ a :: b :: lookmap f l
case swap.none.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
simp [h₁, h₂]
no goals
case swap.none.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
h₂ : f b = none
⊢ b :: a :: lookmap f l ~ a :: b :: lookmap f l
apply swap
case swap.none.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ d :: a :: l ~ a :: d :: l
case swap.none.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
simp [h₁, lookmap_cons_some _ _ h₂]
no goals
case swap.none.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
d : α
h₂ : f b = some d
⊢ d :: a :: l ~ a :: d :: l
apply swap
case swap.some.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ b :: c :: l ~ c :: b :: l
case swap.some.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
simp [lookmap_cons_some _ _ h₁, h₂]
no goals
case swap.some.none
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ b :: c :: l ~ c :: b :: l
apply swap
case swap.some.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ d :: a :: l ~ c :: b :: l
case swap.some.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
simp [lookmap_cons_some _ _ h₁, lookmap_cons_some _ _ h₂]
case swap.some.some.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
b : α
l : List α
d : α
h₂ : f b = some d
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: b :: l)
h₁ : f b = some d
⊢ d :: b :: l ~ d :: b :: l
case swap.some.some
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
a b : α
l : List α
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ d :: a :: l ~ c :: b :: l
rcases(pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩
no goals
case swap.some.some.intro
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option α
l₁ l₂ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
b : α
l : List α
d : α
h₂ : f b = some d
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: b :: l)
h₁ : f b = some d
⊢ d :: b :: l ~ d :: b :: l
exact Perm.refl _
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
IH₂ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂ → lookmap f l₂ ~ lookmap f l₃
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
⊢ Symmetric fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
IH₂ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂ → lookmap f l₂ ~ lookmap f l₃
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
⊢ lookmap f l₁ ~ lookmap f l₃
refine' (IH₁ H).trans (IH₂ ((p₁.pairwise_iff _).1 H))
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option α
l₁✝ l₂✝ : List α
H✝ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝
l₁ l₂ l₃ : List α
p₁ : l₁ ~ l₂
a✝ : l₂ ~ l₃
IH₁ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁ → lookmap f l₁ ~ lookmap f l₂
IH₂ : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂ → lookmap f l₂ ~ lookmap f l₃
H : Pairwise (fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
⊢ Symmetric fun a b => ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d
exact fun a b h c h₁ d h₂ => (h d h₂ c h₁).imp Eq.symm Eq.symm