internlm/Lean-Github huggingface dataset:
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:
intros
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 fun a => β a
a✝¹ : boundLeft d xs✝
a✝ : boundLeft d KVChain.nil
⊢ boundLeft d (mergeWith f xs✝ KVChain.nil)
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
a✝¹ : boundLeft d xs✝
a✝ : boundLeft d KVChain.nil
⊢ boundLeft d (mergeWith f xs✝ KVChain.nil)
Tactic:
rw [mergeWith_nil]
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 fun a => β a
a✝¹ : boundLeft d xs✝
a✝ : boundLeft d KVChain.nil
⊢ boundLeft d xs✝
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
a✝¹ : boundLeft d xs✝
a✝ : boundLeft d KVChain.nil
⊢ boundLeft d xs✝
Tactic:
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:
intro a₂ b₂ ys ha₂ys h_ind_ys xs hdxs hda₂
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
h_ind_ys : ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)
xs : KVChain r fun a => β a
hdxs : boundLeft d xs
hda₂ : boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
⊢ boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂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 β
a₂ : α
b₂ : β a₂
ys : KVChain r fun a => β a
ha₂ys : boundLeft a₂ ys
h_ind_ys : ∀ (xs : KVChain r fun a => β a), boundLeft d xs → boundLeft d ys → boundLeft d (mergeWith f xs ys)
xs : KVChain r fun a => β a
hdxs : boundLeft d xs
hda₂ : boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
⊢ boundLeft d (mergeWith f xs (KVChain.cons a₂ b₂ ys ha₂ys))
Tactic:
revert h_ind_ys hdxs
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)
⊢ (∀ (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))
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)
⊢ (∀ (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))
Tactic:
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)
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 β
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), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d KVChain.nil → boundLeft d (mergeWith f KVChain.nil (KVChain.cons a₂ b₂ ys ha₂ys))

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₂
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) (haxs : boundLeft a xs),
    (fun xs =>
          (∀ (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)))
        xs →
      (fun xs =>
          (∀ (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)))
        (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 β
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), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d KVChain.nil → boundLeft d (mergeWith f KVChain.nil (KVChain.cons a₂ b₂ ys ha₂ys))
Tactic:
case nil => rw [nil_mergeWith]; exact λ _ _=> hda₂
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₂
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) (haxs : boundLeft a xs),
    (fun xs =>
          (∀ (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)))
        xs →
      (fun xs =>
          (∀ (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)))
        (KVChain.cons a b xs haxs)
Tactic:
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
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)
⊢ (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d KVChain.nil → boundLeft d (mergeWith f KVChain.nil (KVChain.cons a₂ b₂ ys ha₂ys))
Tactic:
rw [nil_mergeWith]
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)
⊢ (∀ (xs₁ : KVChain r fun a => β a), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d KVChain.nil → boundLeft d (KVChain.cons a₂ b₂ ys ha₂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 β
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), boundLeft d xs₁ → boundLeft d ys → boundLeft d (mergeWith f xs₁ ys)) →
    boundLeft d KVChain.nil → boundLeft d (KVChain.cons a₂ b₂ ys ha₂ys)
Tactic:
exact λ _ _=> hda₂
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₂
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) (haxs : boundLeft a xs),
    (fun xs =>
          (∀ (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)))
        xs →
      (fun xs =>
          (∀ (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)))
        (KVChain.cons a b xs haxs)
Tactic:
intro a₁ b₁ xs ha₁xs _ h_ind_ys hda₁
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)
⊢ boundLeft d (mergeWith f (KVChain.cons a₁ b₁ xs ha₁xs) (KVChain.cons a₂ b₂ ys ha₂ys))
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e
α : 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)
ha₁a₂ : ¬r a₁ a₂
⊢ 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)
Tactic:
. 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
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case t
α : 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)
ha₁a₂ : r a₁ a₂
⊢ 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)
Tactic:
rw [insertWithAux_cons_rel ha₁a₂]
Proof state after:
case t
α : 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)
ha₁a₂ : r a₁ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂
              ha₁a₂).1.fst.toList
      (mergeWith f
          (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
                (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂ ha₁a₂).1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case t
α : 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)
ha₁a₂ : r a₁ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
              (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂
              ha₁a₂).1.fst.toList
      (mergeWith f
          (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
                (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂ ha₁a₂).1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
rw [toList_fst_insertWithAux_eq_append]
Proof state after:
case t
α : 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)
ha₁a₂ : r a₁ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      ((insertWithAux f KVChain.nil xs True.intro a₂ b₂ True.intro).val.fst.toList ++
        (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)).toList)
      (mergeWith f
          (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
                (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂ ha₁a₂).1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case t
α : 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)
ha₁a₂ : r a₁ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      ((insertWithAux f KVChain.nil xs True.intro a₂ b₂ True.intro).val.fst.toList ++
        (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)).toList)
      (mergeWith f
          (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
                (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂ ha₁a₂).1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
rw [List.reverseAux_append_left]
Proof state after:
case t
α : 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)
ha₁a₂ : r a₁ a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverse (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)).toList ++
      List.reverseAux (insertWithAux f KVChain.nil xs True.intro a₂ b₂ True.intro).val.fst.toList
        (mergeWith f
            (insertWithAux f (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs
                  (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil (_ : boundLeft a₁ KVChain.nil)) xs) a₂ b₂ ha₁a₂).1.snd
            { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)