α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))
rw [filterMap_cons, filterMap_cons]
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)
exact
  match f a, g b, hfg h₁ with
  | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
  | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)