case cons a as h_ind =>
  intro hchain
  unfold filterMap
  cases hfa : f a <;> dsimp
  case none => exact h_ind hchain.tail
  case some b =>
    apply cons_of_forAll
    . clear h_ind
      induction as <;> dsimp [filterMap]
      case a.nil => dsimp [List.forAll]
      case a.cons a₁ as h_ind₁ =>
        have hchainaas : Ascending r (a::as) := by
          apply hchain.tail.subst_head
          exact λ _ h => trans hchain.head h
        cases hfa₁ : f a₁ <;> dsimp
        case none => exact h_ind₁ hchainaas
        case some b₁ =>
          constructor
          . have := rel_pres a a₁ hchain.head
            rw [hfa, hfa₁] at this
            exact this b b₁ rfl rfl
          . exact h_ind₁ hchainaas
    . exact h_ind hchain.tail
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
β : Type v
r' : β → β → Prop
f : α → Option β
rel_pres : ∀ (a₁ a₂ : α), r a₁ a₂ → ∀ (b₁ b₂ : β), f a₁ = some b₁ → f a₂ = some b₂ → r' b₁ b₂
a : α
as : List α
h_ind : Ascending r as → Ascending r' (filterMap f as)
⊢ Ascending r (a :: as) → Ascending r' (filterMap f (a :: as))
no goals