Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e.e.refl
α : 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)
xs : KVChain r fun a => β a
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)
b₁ : β a₂
ha₁xs : boundLeft a₂ xs
hda₁ : boundLeft d (KVChain.cons a₂ b₁ xs ha₁xs)
ha₁a₂ ha₂a₁ : ¬r a₂ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      (Option.casesOn (f a₂ b₁ b₂)
              { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) }
              fun bf =>
              {
                val :=
                  (KVChain.cons a₂ bf KVChain.nil
                      (_ :
                        List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                          (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                    xs),
                property :=
                  (_ :
                    hingeable
                      (KVChain.cons a₂ bf KVChain.nil
                        (_ :
                          List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                            (KVChain.cons a₂ b₂ ys ha₂ys).toList))
                      (KVChain.cons a₂ bf KVChain.nil
                            (_ :
                              List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                                (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                          xs).snd) }).1.fst.toList
      (mergeWith f
          (Option.casesOn (f a₂ b₁ b₂)
                { val := (KVChain.nil, xs), property := (_ : hingeable (KVChain.nil, xs).fst (KVChain.nil, xs).snd) }
                fun bf =>
                {
                  val :=
                    (KVChain.cons a₂ bf KVChain.nil
                        (_ :
                          List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                            (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                      xs),
                  property :=
                    (_ :
                      hingeable
                        (KVChain.cons a₂ bf KVChain.nil
                          (_ :
                            List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                              (KVChain.cons a₂ b₂ ys ha₂ys).toList))
                        (KVChain.cons a₂ bf KVChain.nil
                              (_ :
                                List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                                  (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                            xs).snd) }).1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
cases f a₂ b₁ b₂ <;> dsimp
Proof state after:
case e.e.refl.none
α : 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)
xs : KVChain r fun a => β a
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)
b₁ : β a₂
ha₁xs : boundLeft a₂ xs
hda₁ : boundLeft d (KVChain.cons a₂ b₁ xs ha₁xs)
ha₁a₂ ha₂a₁ : ¬r a₂ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (mergeWith f xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList

case e.e.refl.some
α : 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)
xs : KVChain r fun a => β a
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)
b₁ : β a₂
ha₁xs : boundLeft a₂ xs
hda₁ : boundLeft d (KVChain.cons a₂ b₁ xs ha₁xs)
ha₁a₂ ha₂a₁ : ¬r a₂ a₂
val✝ : β a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    ({ fst := a₂, snd := val✝ } ::
      (mergeWith f xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)