Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r fun a => β a
ha₂ys : boundLeft a₂ ys
xs✝ : KVChain r fun a => β a
hda₂ : boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d xs → boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂ys))
h_ind_ys : ∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)
hda₁ : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
ha₁a₂ : ¬r a₁ a₂
ha₂a₁ : r a₂ a₁
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a₂ b₂
              (_ :
                List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                  (KVChain.cons a₂ b₂ ys ha₂ys).toList)).1.fst.toList
      (mergeWith f
          (insertWithAux f KVChain.nil (KVChain.cons a₁ b₁ xs ha₁xs) True.intro a₂ b₂
                (_ :
                  List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                    (KVChain.cons a₂ b₂ ys ha₂ys).toList)).1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
rw [insertWithAux_cons_flip ha₂a₁]
Proof state after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys✝ : KVChain r β
a₂ : α
b₂ : β a₂
ys : KVChain r fun a => β a
ha₂ys : boundLeft a₂ ys
xs✝ : KVChain r fun a => β a
hda₂ : boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
a₁ : α
b₁ : β a₁
xs : KVChain r fun a => β a
ha₁xs : boundLeft a₁ xs
a✝ :
  (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d xs → boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂ys))
h_ind_ys : ∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)
hda₁ : boundLeft d (KVChain.cons a₁ b₁ xs ha₁xs)
ha₁a₂ : ¬r a₁ a₂
ha₂a₁ : r a₂ a₁
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      {
              val :=
                (KVChain.cons a₂ b₂ KVChain.nil
                    (_ :
                      List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                        (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                  KVChain.cons a₁ b₁ xs ha₁xs),
              property := ha₂a₁ }.1.fst.toList
      (mergeWith f
          {
                val :=
                  (KVChain.cons a₂ b₂ KVChain.nil
                      (_ :
                        List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                          (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                    KVChain.cons a₁ b₁ xs ha₁xs),
                property := ha₂a₁ }.1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)