no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option β
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ List.filterMap f l₁ ~ List.filterMap f l₂
induction p with
| nil => simp
| cons x _p IH =>
  simp only [filterMap]
  cases h : f x
    <;> simp [h, filterMap, IH, Perm.cons]
| swap x y l₂ =>
  simp only [filterMap]
  cases hx : f x
    <;> cases hy : f y
      <;> simp [hx, hy, filterMap, swap]
| trans _p₁ _p₂ IH₁ IH₂ =>
  exact IH₁.trans IH₂
no goals
case nil
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
f : α → Option β
l₁ l₂ : List α
⊢ List.filterMap f [] ~ List.filterMap f []
simp
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH : List.filterMap f l₁✝ ~ List.filterMap f l₂✝
⊢ List.filterMap f (x :: l₁✝) ~ List.filterMap f (x :: l₂✝)
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH : List.filterMap f l₁✝ ~ List.filterMap f l₂✝
⊢ List.filterMap f (x :: l₁✝) ~ List.filterMap f (x :: l₂✝)
simp only [filterMap]
no goals
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option β
l₁ l₂ : List α
x : α
l₁✝ l₂✝ : List α
_p : l₁✝ ~ l₂✝
IH : List.filterMap f l₁✝ ~ List.filterMap f l₂✝
⊢ List.filterMap f (x :: l₁✝) ~ List.filterMap f (x :: l₂✝)
cases h : f x
  <;> simp [h, filterMap, IH, Perm.cons]
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
f : α → Option β
l₁ l₂✝ : List α
x y : α
l₂ : List α
⊢ List.filterMap f (y :: x :: l₂) ~ List.filterMap f (x :: y :: l₂)
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
f : α → Option β
l₁ l₂✝ : List α
x y : α
l₂ : List α
⊢ List.filterMap f (y :: x :: l₂) ~ List.filterMap f (x :: y :: l₂)
simp only [filterMap]
no goals
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝¹ : List α
f : α → Option β
l₁ l₂✝ : List α
x y : α
l₂ : List α
⊢ List.filterMap f (y :: x :: l₂) ~ List.filterMap f (x :: y :: l₂)
cases hx : f x
  <;> cases hy : f y
    <;> simp [hx, hy, filterMap, swap]
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
f : α → Option β
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
_p₁ : l₁✝ ~ l₂✝
_p₂ : l₂✝ ~ l₃✝
IH₁ : List.filterMap f l₁✝ ~ List.filterMap f l₂✝
IH₂ : List.filterMap f l₂✝ ~ List.filterMap f l₃✝
⊢ List.filterMap f l₁✝ ~ List.filterMap f l₃✝
exact IH₁.trans IH₂