internlm/Lean-Github huggingface dataset:
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
⊢ ∀ (a : α) (b : β a) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun xs =>
          ∀ (hxs : hingeable xs_r xs),
            (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
              List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList)
        xs →
      (fun xs =>
          ∀ (hxs : hingeable xs_r xs),
            (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
              List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList)
        (KVChain.cons a b xs haxs)
Tactic:
intro a b  xs haxs _ hxs
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f xs_r (KVChain.cons a b xs haxs) hxs (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f xs_r (KVChain.cons a b xs haxs) hxs (y :: ys) hascend hyxs).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
dsimp [mergeWith.loop]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ (mergeWith.loop f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst
        (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
        (_ :
          hingeable (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).val.fst
            (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).val.snd)
        ys (_ : List.Ascending (Sigma.relOnFst r) ys)
        (_ :
          List.predHead
            ((fun a_1 => boundLeft a_1 (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst) ∘
              Sigma.fst)
            ys)).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.fst.toList
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [toList_fst_insertWithAux_eq_append]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f xs_r (KVChain.cons a b xs haxs) hxs y.fst y.snd hyxs).1.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [toList_snd_insertWithAux_inv]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      ((insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList ++
        xs_r.toList)
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [List.reverseAux_append_left]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverse xs_r.toList ++
      List.reverseAux
        (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
            { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverse xs_r.toList ++
      List.reverseAux
        (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
            { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
rw [List.reverseAux_eq_append (as:=xs_r.toList)]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverse xs_r.toList ++
      List.reverseAux
        (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
        (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
            { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    List.reverseAux xs_r.toList [] ++
      (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Theorem: KVChain.toList_mergeWith_loop_eq_reverseAux
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
y : Sigma β
ys : List (Sigma β)
h_ind :
  ∀ {xs_r : KVChain (flip r) β} {xs : KVChain r β} {hxs : hingeable xs_r xs}
    {hascend : List.Ascending (Sigma.relOnFst r) ys}
    {hxsys : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) ys},
    (mergeWith.loop f xs_r xs hxs ys hascend hxsys).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := ys, ascend := hascend }).toList
xs_r : KVChain (flip r) β
xs✝ : KVChain r β
hascend : List.Ascending (Sigma.relOnFst r) (y :: ys)
hyxs : List.predHead ((fun a => boundLeft a xs_r) ∘ Sigma.fst) (y :: ys)
a : α
b : β a
xs : KVChain r fun a => β a
haxs : boundLeft a xs
a✝ :
  ∀ (hxs : hingeable xs_r xs),
    (mergeWith.loop f xs_r xs hxs (y :: ys) hascend hyxs).toList =
      List.reverseAux xs_r.toList (mergeWith f xs { toList := y :: ys, ascend := hascend }).toList
hxs : hingeable xs_r (KVChain.cons a b xs haxs)
⊢ List.reverseAux
      (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.fst.toList
      (mergeWith f (insertWithAux f KVChain.nil (KVChain.cons a b xs haxs) True.intro y.fst y.snd True.intro).val.snd
          { toList := ys, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys) }).toList =
    (mergeWith f (KVChain.cons a b xs haxs) { toList := y :: ys, ascend := hascend }).toList
Tactic:
conv =>
  rhs
  unfold mergeWith
  unfold mergeWith.loop
  rw [h_ind]
Proof state after:
no goals
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 : α
xs ys : KVChain r β
⊢ boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)
Tactic:
revert xs
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 β
⊢ ∀ {xs : KVChain r β}, boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)
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 β
⊢ ∀ {xs : KVChain r β}, boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)
Tactic:
apply ys.recOnList (motive:=λ ys=> ∀ xs, xs.boundLeft d → ys.boundLeft d → (mergeWith f xs ys).boundLeft d)
Proof state after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
d : α
ys : KVChain r β
⊢ ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d KVChain.nil → boundLeft d (mergeWith f xs KVChain.nil)

case cons
α : 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) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)) xs →
      (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys))
        (KVChain.cons a b xs haxs)
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 β
⊢ ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d KVChain.nil → boundLeft d (mergeWith f xs KVChain.nil)
Tactic:
case nil =>
  intros; rw [mergeWith_nil]; assumption
Proof state after:
no goals
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) (xs : KVChain r fun a => β a) (haxs : boundLeft a xs),
    (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)) xs →
      (fun ys => ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys))
        (KVChain.cons a b xs haxs)
Tactic:
case cons =>
  intro a₂ b₂ ys ha₂ys h_ind_ys xs hdxs hda₂
  revert h_ind_ys hdxs
  apply xs.recOnList (motive:=λ xs=> (∀ xs₁, xs₁.boundLeft d → ys.boundLeft d → (mergeWith f xs₁ ys).boundLeft d) → xs.boundLeft d → (mergeWith f xs (ys.cons a₂ b₂ ha₂ys)).boundLeft d)
  case nil => rw [nil_mergeWith]; exact λ _ _=> hda₂
  case cons =>
    intro a₁ b₁ xs ha₁xs _ h_ind_ys hda₁
    dsimp [boundLeft, hingeable, mergeWith, mergeWith.loop]
    rw [toList_mergeWith_loop_eq_reverseAux]
    apply dite (r a₁ a₂) <;> intro ha₁a₂
    . rw [insertWithAux_cons_rel ha₁a₂]
      rw [toList_fst_insertWithAux_eq_append]
      rw [List.reverseAux_append_left]
      dsimp [List.reverse, List.reverseAux]
      exact hda₁
    . apply dite (r a₂ a₁) <;> intro ha₂a₁
      . rw [insertWithAux_cons_flip ha₂a₁]
        dsimp [List.reverseAux]
        exact hda₂
      . have : a₂ = a₁ := Trichotomous.eq_of_incomp ⟨ha₂a₁, ha₁a₂⟩
        cases this
        rw [insertWithAux_cons_rfl]
        cases f a₂ b₁ b₂ <;> dsimp
        case none =>
          apply h_ind_ys
          . exact boundLeft_descend (λ _=> trans hda₂) ha₁xs
          . exact boundLeft_descend (λ _=> trans hda₁) ha₂ys
        case some bf =>
          dsimp [List.reverseAux, List.predHead]
          exact hda₂
Proof state after:
no goals