internlm/Lean-Github huggingface dataset:
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.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)
Tactic:
dsimp [List.reverse, List.reverseAux]
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)
    ({ fst := a₁, snd := b₁ } ::
      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 True.intro) xs
                  (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) 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)
    ({ fst := a₁, snd := b₁ } ::
      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 True.intro) xs
                  (_ : hingeable (KVChain.cons a₁ b₁ KVChain.nil True.intro) xs) a₂ b₂ ha₁a₂).1.snd
            { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
exact hda₁
Proof state after:
no goals
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e.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₂
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:
. 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 e.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₂
ha₂a₁ : r a₂ a₁
⊢ List.predHead (r d ∘ Sigma.fst)
    (List.reverseAux
      {
              val :=
                (KVChain.cons a₂ b₂ KVChain.nil
                    (_ :
                      List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                        (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                  KVChain.cons a₁ b₁ xs ha₁xs),
              property := ha₂a₁ }.1.fst.toList
      (mergeWith f
          {
                val :=
                  (KVChain.cons a₂ b₂ KVChain.nil
                      (_ :
                        List.predHead ((fun a => boundLeft a KVChain.nil) ∘ Sigma.fst)
                          (KVChain.cons a₂ b₂ ys ha₂ys).toList),
                    KVChain.cons a₁ b₁ xs ha₁xs),
                property := ha₂a₁ }.1.snd
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
dsimp [List.reverseAux]
Proof state after:
case e.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₂
ha₂a₁ : r a₂ a₁
⊢ List.predHead (r d ∘ Sigma.fst)
    ({ fst := a₂, snd := b₂ } ::
      (mergeWith f (KVChain.cons a₁ b₁ xs ha₁xs)
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e.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₂
ha₂a₁ : r a₂ a₁
⊢ List.predHead (r d ∘ Sigma.fst)
    ({ fst := a₂, snd := b₂ } ::
      (mergeWith f (KVChain.cons a₁ b₁ xs ha₁xs)
          { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
exact hda₂
Proof state after:
no goals
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e.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₂
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:
have : a₂ = a₁ := Trichotomous.eq_of_incomp ⟨ha₂a₁, ha₁a₂⟩
Proof state after:
case e.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₂
ha₂a₁ : ¬r a₂ a₁
this : 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)
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case e.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₂
ha₂a₁ : ¬r a₂ a₁
this : 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:
cases this
Proof state after:
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
      (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)
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
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
Tactic:
case none =>
  apply h_ind_ys
  . exact boundLeft_descend (λ _=> trans hda₂) ha₁xs
  . exact boundLeft_descend (λ _=> trans hda₁) ha₂ys
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
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₂
bf : β a₂
⊢ List.predHead (r d ∘ Sigma.fst)
    ({ fst := a₂, snd := bf } ::
      (mergeWith f xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }).toList)
Tactic:
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
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
Tactic:
apply h_ind_ys
Proof state after:
case a
α : 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₂
⊢ boundLeft d xs

case a
α : 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₂
⊢ boundLeft d ys
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case a
α : 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₂
⊢ boundLeft d xs

case a
α : 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₂
⊢ boundLeft d ys
Tactic:
. exact boundLeft_descend (λ _=> trans hda₂) ha₁xs
Proof state after:
case a
α : 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₂
⊢ boundLeft d ys
Theorem: KVChain.boundLeft_mergeWith
Proof state before:
case a
α : 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₂
⊢ boundLeft d ys
Tactic:
. exact boundLeft_descend (λ _=> trans hda₁) ha₂ys
Proof state after:
no goals