-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_filterMap {f : β → Option α} {l : List β} :
    Pairwise R (filterMap f l) ↔ Pairwise (fun a a' : β => ∀ b ∈ f a, ∀ b' ∈ f a', R b b') l

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
⊢ Pairwise R (b :: filterMap f l) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)

Tactic:
simpa [IH, e] using fun _ =>
  ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
e : f a = none
⊢ Pairwise R (filterMap f l) ↔
    (∀ (a' : β), a' ∈ l → ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') ∧
      Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l

Tactic:
simp only [e, false_implies, implies_true, true_and, IH, reduceCtorEq]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
e : f a = none
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)

Tactic:
rw [filterMap_cons_none e, pairwise_cons]

Result:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
e : f a = none
⊢ Pairwise R (filterMap f l) ↔
    (∀ (a' : β), a' ∈ l → ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') ∧
      Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
l : List β
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l

Tactic:
simp only [Option.mem_def]

Result:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
l : List β
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l

Proof state:
case cons
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)

Tactic:
match e : f a with
| none =>
  rw [filterMap_cons_none e, pairwise_cons]
  simp only [e, false_implies, implies_true, true_and, IH, reduceCtorEq]
| some b =>
  rw [filterMap_cons_some e]
  simpa [IH, e] using fun _ =>
    ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
l : List β
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l

Tactic:
let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b'

Result:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
l : List β
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b') l

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)

Tactic:
rw [filterMap_cons_some e]

Result:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
b : α
e : f a = some b
⊢ Pairwise R (b :: filterMap f l) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)

Proof state:
case nil
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f []) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') []

Tactic:
simp only [filterMap, Pairwise.nil]

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
l : List β
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
⊢ Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l

Tactic:
induction l with
| nil => simp only [filterMap, Pairwise.nil]
| cons a l IH => ?_

Result:
case cons
β : Type u_1
α : Type u_2
R : α → α → Prop
f : β → Option α
_S : β → β → Prop := fun a a' => ∀ (b : α), b ∈ f a → ∀ (b' : α), b' ∈ f a' → R b b'
a : β
l : List β
IH : Pairwise R (filterMap f l) ↔ Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
⊢ Pairwise R (filterMap f (a :: l)) ↔
    Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') (a :: l)