Theorem: KVChain.nil_mergeWith (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 KVChain.nil { toList := xs, ascend := ascend✝ } = { toList := xs, ascend := ascend✝ }
Tactic:
dsimp [KVChain.nil, mergeWith, mergeWith.loop]
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 := [], ascend := (_ : List.Ascending (Sigma.relOnFst r) []) } True.intro xs ascend✝
      (_ : List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst) { toList := xs, ascend := ascend✝ }.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 := [], ascend := (_ : List.Ascending (Sigma.relOnFst r) []) } True.intro xs ascend✝
      (_ : List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst) { toList := xs, ascend := ascend✝ }.toList) =
    { toList := xs, ascend := ascend✝ }
Tactic:
cases xs <;> rfl
State after:
no goals