Theorem: KVChain.mergeWith_nil (Algdata/Data/KVChain/MergeWith.lean)

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ mergeWith f { toList := xs, ascend := ascend✝ } KVChain.nil = { toList := xs, ascend := ascend✝ }
Tactic:
dsimp [KVChain.nil, mergeWith]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ mergeWith.loop f { toList := [], ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) []) }
      { toList := xs, ascend := ascend✝ } True.intro [] (_ : List.Ascending (Sigma.relOnFst r) [])
      (_ :
        List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
          { toList := [], ascend := (_ : List.Ascending (Sigma.relOnFst r) []) }.toList) =
    { toList := xs, ascend := ascend✝ }

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ mergeWith.loop f { toList := [], ascend := (_ : List.Ascending (Sigma.relOnFst (flip r)) []) }
      { toList := xs, ascend := ascend✝ } True.intro [] (_ : List.Ascending (Sigma.relOnFst r) [])
      (_ :
        List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
          { toList := [], ascend := (_ : List.Ascending (Sigma.relOnFst r) []) }.toList) =
    { toList := xs, ascend := ascend✝ }
Tactic:
rfl
State after:
no goals