rw [hfa, hfa₁] at this
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
this : ∀ (b₁ b₂ : β), f a = some b₁ → f a₁ = some b₂ → r' b₁ b₂
⊢ r' b b₁
case left
α : 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 : α
b : β
hfa : f a = some b
a₁ : α
as : List α
h_ind₁ : Ascending r (a :: as) → forAll (r' b) (filterMap f as)
hchain : Ascending r (a :: a₁ :: as)
hchainaas : Ascending r (a :: as)
b₁ : β
hfa₁ : f a₁ = some b₁
this : ∀ (b₁_1 b₂ : β), some b = some b₁_1 → some b₁ = some b₂ → r' b₁_1 b₂
⊢ r' b b₁