-- 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:
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)

Tactic:
rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d

Result:
case swap.none.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)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

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)

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)

case swap.some.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)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

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₁
⊢ lookmap f l₁ ~ lookmap f l₃

Tactic:
refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))

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 : α},
    (∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d) → ∀ (c : α), c ∈ f y → ∀ (d : α), d ∈ f x → y = x ∧ c = d

Proof state:
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₂)

Tactic:
simp [lookmap_cons_some _ _ h, p]

Result:
no goals

Proof state:
case swap.some.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)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩

Result:
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)

Proof state:
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₂)

Tactic:
simpa [h] using IH (pairwise_cons.1 H).2

Result:
no goals

Proof state:
case swap.none.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)
h₁ : f a = none
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

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

Result:
no goals