-- Mathlib/Data/List/Lookmap.lean
theorem perm_lookmap (f : α → Option α) {l₁ l₂ : List α}
    (H : Pairwise (fun a b => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁) (p : l₁ ~ l₂) :
    lookmap f l₁ ~ lookmap f l₂

Proof state:
α : Type u_1
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₂

Tactic:
induction' p with a l₁ l₂ p IH a b l l₁ l₂ l₃ p₁ _ IH₁ IH₂

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

case cons
α : Type u_1
f : α → Option α
l₁✝ l₂✝ : List α
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 u_1
f : α → Option α
l₁ l₂ : List α
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 u_1
f : α → Option α
l₁✝ 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₃

Proof state:
case swap.none.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
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)

Tactic:
simpa [h₁, lookmap_cons_some _ _ h₂] using swap _ _ _

Result:
no goals

Proof state:
case trans
α : Type u_1
f : α → Option α
l₁✝ 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₁
⊢ ∀ {x y : α},
    (∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d) → ∀ (c : α), c ∈ f y → ∀ (d : α), d ∈ f x → y = x ∧ c = d

Tactic:
intro x y h c hc d hd

Result:
case trans
α : Type u_1
f : α → Option α
l₁✝ 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₁
x y : α
h : ∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d
c : α
hc : c ∈ f y
d : α
hd : d ∈ f x
⊢ y = x ∧ c = d

Proof state:
case swap.some.some.intro
α : Type u_1
f : α → Option α
l₁ l₂ : List α
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
⊢ lookmap f (b :: b :: l) ~ lookmap f (b :: b :: l)

Tactic:
exact Perm.refl _

Result:
no goals

Proof state:
case trans
α : Type u_1
f : α → Option α
l₁✝ 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₁
x y : α
h : ∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d
c : α
hc : c ∈ f y
d : α
hd : d ∈ f x
⊢ y = x ∧ c = d

Tactic:
rw [@eq_comm _ y, @eq_comm _ c]

Result:
case trans
α : Type u_1
f : α → Option α
l₁✝ 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₁
x y : α
h : ∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d
c : α
hc : c ∈ f y
d : α
hd : d ∈ f x
⊢ x = y ∧ d = c

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

Tactic:
simp

Result:
no goals

Proof state:
case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
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)

Tactic:
simpa [lookmap_cons_some _ _ h₁, h₂] using swap _ _ _

Result:
no goals

Proof state:
case trans
α : Type u_1
f : α → Option α
l₁✝ 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₁
x y : α
h : ∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d
c : α
hc : c ∈ f y
d : α
hd : d ∈ f x
⊢ x = y ∧ d = c

Tactic:
apply h d hd c hc

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → Option α
l₁✝ l₂✝ : List α
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₂)

Tactic:
cases h : f a

Result:
case cons.none
α : Type u_1
f : α → Option α
l₁✝ l₂✝ : List α
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 u_1
f : α → Option α
l₁✝ l₂✝ : List α
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₂)