Theorem: KVChain.boundLeft_mergeWith
Proof state before:
α : 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)
⊢ List.predHead (r d ∘ Sigma.fst)
    (mergeWith.loop 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.fst
        (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
        (_ :
          List.relHead (Sigma.relOnFst r)
            (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)).val.fst.toList
            (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)).val.snd.toList)
        ys.toList (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
        (_ :
          List.predHead
            ((fun a =>
                boundLeft a
                  (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) ∘
              Sigma.fst)
            ys.toList)).toList
Tactic:
rw [toList_mergeWith_loop_eq_reverseAux]
Proof state after:
α : 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)
⊢ 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)