internlm/Lean-Github huggingface dataset:
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
apply dite (r y₁ x₁) <;> intro hy₁x₁
Proof state after:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList

case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList

case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
. rw [cons_mergeWith_cons_flip hy₁x₁]
  rw [cons_mergeWith_cons_rel hy₁x₁]
  dsimp
  rw [h_ind_ys]
Proof state after:
case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
. have : x₁ = y₁ := Trichotomous.eq_of_incomp ⟨hx₁y₁, hy₁x₁⟩
  cases this
  rw [cons_mergeWith_cons_rfl, cons_mergeWith_cons_rfl]
  dsimp [flip] at *
  cases f x₁ x₂ y₂ <;> dsimp <;> rw [h_ind_xs]
Proof state after:
no goals
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [cons_mergeWith_cons_flip hy₁x₁]
Proof state after:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (KVChain.cons y₁ y₂ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys))).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (KVChain.cons y₁ y₂ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys))).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [cons_mergeWith_cons_rel hy₁x₁]
Proof state after:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (KVChain.cons y₁ y₂ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys))).toList =
    (KVChain.cons y₁ y₂ (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs))
        (_ : boundLeft y₁ (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)))).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ (KVChain.cons y₁ y₂ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys))).toList =
    (KVChain.cons y₁ y₂ (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs))
        (_ : boundLeft y₁ (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)))).toList
Tactic:
dsimp
Proof state after:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ { fst := y₁, snd := y₂ } :: (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys).toList =
    { fst := y₁, snd := y₂ } :: (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : r y₁ x₁
⊢ { fst := y₁, snd := y₂ } :: (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys).toList =
    { fst := y₁, snd := y₂ } :: (mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [h_ind_ys]
Proof state after:
no goals
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
have : x₁ = y₁ := Trichotomous.eq_of_incomp ⟨hx₁y₁, hy₁x₁⟩
Proof state after:
case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
this : x₁ = y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
hx₁y₁ : ¬r x₁ y₁
hy₁x₁ : ¬r y₁ x₁
this : x₁ = y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
cases this
Proof state after:
case a.e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons x₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons x₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons x₁ y₂ ys hys)).toList =
    (mergeWith (fun a => flip (f a)) (KVChain.cons x₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [cons_mergeWith_cons_rfl, cons_mergeWith_cons_rfl]
Proof state after:
case a.e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (Option.casesOn (f x₁ x₂ y₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons x₁ bf (mergeWith f xs ys) (_ : boundLeft x₁ (mergeWith f xs ys))).toList =
    (Option.casesOn (flip (f x₁) y₂ x₂) (mergeWith (fun a => flip (f a)) ys xs) fun bf =>
        KVChain.cons x₁ bf (mergeWith (fun a => flip (f a)) ys xs)
          (_ : boundLeft x₁ (mergeWith (fun a => flip (f a)) ys xs))).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a => flip (f a)) x xs
ys✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a => flip (f a)) ys (KVChain.cons x₁ x₂ xs hxs)
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (Option.casesOn (f x₁ x₂ y₂) (mergeWith f xs ys) fun bf =>
        KVChain.cons x₁ bf (mergeWith f xs ys) (_ : boundLeft x₁ (mergeWith f xs ys))).toList =
    (Option.casesOn (flip (f x₁) y₂ x₂) (mergeWith (fun a => flip (f a)) ys xs) fun bf =>
        KVChain.cons x₁ bf (mergeWith (fun a => flip (f a)) ys xs)
          (_ : boundLeft x₁ (mergeWith (fun a => flip (f a)) ys xs))).toList
Tactic:
dsimp [flip] at *
Proof state after:
case a.e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a b a_1 => f a a_1 b) x xs
ys✝ ys : KVChain r β
h_ind_ys :
  mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a b a_1 => f a a_1 b) ys (KVChain.cons x₁ x₂ xs hxs)
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (Option.rec (mergeWith f xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith f xs ys) (_ : boundLeft x₁ (mergeWith f xs ys)))
        (f x₁ x₂ y₂)).toList =
    (Option.rec (mergeWith (fun a b a_1 => f a a_1 b) ys xs)
        (fun val =>
          KVChain.cons x₁ val (mergeWith (fun a b a_1 => f a a_1 b) ys xs)
            (_ : boundLeft x₁ (mergeWith (fun a b a_1 => f a a_1 b) ys xs)))
        (f x₁ x₂ y₂)).toList
Theorem: KVChain.mergeWith_flip
Proof state before:
case a.e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith (fun a b a_1 => f a a_1 b) x xs
ys✝ ys : KVChain r β
h_ind_ys :
  mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith (fun a b a_1 => f a a_1 b) ys (KVChain.cons x₁ x₂ xs hxs)
y₂ : β x₁
hys : boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬r x₁ x₁
⊢ (Option.rec (mergeWith f xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith f xs ys) (_ : boundLeft x₁ (mergeWith f xs ys)))
        (f x₁ x₂ y₂)).toList =
    (Option.rec (mergeWith (fun a b a_1 => f a a_1 b) ys xs)
        (fun val =>
          KVChain.cons x₁ val (mergeWith (fun a b a_1 => f a a_1 b) ys xs)
            (_ : boundLeft x₁ (mergeWith (fun a b a_1 => f a a_1 b) ys xs)))
        (f x₁ x₂ y₂)).toList
Tactic:
cases f x₁ x₂ y₂ <;> dsimp <;> rw [h_ind_xs]
Proof state after:
no goals
Theorem: KVChain.mergeWith_congrFun
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs ys x✝ : KVChain r β
⊢ mergeWith f KVChain.nil x✝ = mergeWith g KVChain.nil x✝
Tactic:
rw [nil_mergeWith, nil_mergeWith]
Proof state after:
no goals
Theorem: KVChain.mergeWith_congrFun
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs✝ ys✝ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
ys : KVChain r β
⊢ mergeWith f (KVChain.cons x₁ x₂ xs hxs) KVChain.nil = mergeWith g (KVChain.cons x₁ x₂ xs hxs) KVChain.nil
Tactic:
rw [mergeWith_nil, mergeWith_nil]
Proof state after:
no goals
Theorem: KVChain.mergeWith_congrFun
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
⊢ mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) =
    mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)
Tactic:
apply eq_of_toList_eq
Proof state after:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList
Tactic:
apply dite (r x₁ y₁) <;> intro hx₁y₁
Proof state after:
case a.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
hx₁y₁ : r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList

case a.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ f g : (a : α) → β a → β a → Option (β a)
hfg : ∀ (a : α) (b₁ b₂ : β a), f a b₁ b₂ = g a b₁ b₂
xs✝ ys✝¹ : KVChain r β
x₁ : α
x₂ : β x₁
xs : KVChain r β
hxs : boundLeft x₁ xs
h_ind_xs : ∀ (x : KVChain r β), mergeWith f xs x = mergeWith g xs x
ys✝ : KVChain r β
y₁ : α
y₂ : β y₁
ys : KVChain r β
hys : boundLeft y₁ ys
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
hx₁y₁ : ¬r x₁ y₁
⊢ (mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList