α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
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
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
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
let _S (a a' : β) := ∀ b ∈ f a, ∀ b' ∈ f a', R b b'
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
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
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
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
simp only [Option.mem_def]
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
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') []

case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l✝ : List α
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
induction' l with a l IH
case cons.none
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)

case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
case cons
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
cases' e : f a with b
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
rw [filterMap_cons_some _ _ _ e]
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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 (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l →
    ((∀ (a' : α) (x : β), x ∈ l → f x = some a' → R b a') ↔ ∀ (a' : β), a' ∈ l → ∀ (b' : α), f a' = some b' → R b b')
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
simp only [pairwise_cons, mem_filterMap, forall_exists_index, and_imp, IH, e, Option.some.injEq,
  forall_eq', and_congr_left_iff]
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝¹ : α
l✝ : List α
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
a✝ : Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
⊢ (∀ (a' : α) (x : β), x ∈ l → f x = some a' → R b a') ↔ ∀ (a' : β), a' ∈ l → ∀ (b' : α), f a' = some b' → R b b'
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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 (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l →
    ((∀ (a' : α) (x : β), x ∈ l → f x = some a' → R b a') ↔ ∀ (a' : β), a' ∈ l → ∀ (b' : α), f a' = some b' → R b b')
intro _
no goals
case cons.some
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝¹ : α
l✝ : List α
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
a✝ : Pairwise (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') l
⊢ (∀ (a' : α) (x : β), x ∈ l → f x = some a' → R b a') ↔ ∀ (a' : β), a' ∈ l → ∀ (b' : α), f a' = some b' → R b b'
exact ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
no goals
case nil
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a : α
l : List α
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') []
simp only [filterMap, Pairwise.nil]
case cons.none
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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 (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') 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
case cons.none
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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)
rw [filterMap_cons_none _ _ e, propext IH, pairwise_cons]
no goals
case cons.none
α : Type u_1
β : Type u_2
R S T : α → α → Prop
a✝ : α
l✝ : List α
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 (fun a a' => ∀ (b : α), f a = some b → ∀ (b' : α), f a' = some b' → R b b') 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
simp only [e, forall_prop_of_false not_false, forall₃_true_iff, true_and_iff]