internlm/Lean-Github huggingface dataset:
Theorem: KVChain.mergeWith_congrFun
Proof state before:
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
Tactic:
. rw [cons_mergeWith_cons_rel hx₁y₁]
  rw [cons_mergeWith_cons_rel hx₁y₁]
  dsimp
  rw [h_ind_xs]
Proof state after:
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
Theorem: KVChain.mergeWith_congrFun
Proof state before:
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
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✝ 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₁
hy₁x₁ : r y₁ x₁
⊢ (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.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₁
hy₁x₁ : ¬r y₁ x₁
⊢ (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.e.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₁
hy₁x₁ : r y₁ x₁
⊢ (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.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₁
hy₁x₁ : ¬r y₁ x₁
⊢ (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:
. rw [cons_mergeWith_cons_flip hy₁x₁]
  rw [cons_mergeWith_cons_flip 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✝ 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₁
hy₁x₁ : ¬r y₁ x₁
⊢ (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.e.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₁
hy₁x₁ : ¬r y₁ x₁
⊢ (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:
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✝ 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₁
hy₁x₁ : ¬r y₁ x₁
this : 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
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a.e.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₁
hy₁x₁ : ¬r y₁ x₁
this : 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
Tactic:
cases this
Proof state after:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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 g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons x₁ y₂ ys hys)).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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 g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons x₁ y₂ ys hys)).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✝ 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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 (g x₁ x₂ y₂) (mergeWith g xs ys) fun bf =>
        KVChain.cons x₁ bf (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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 (g x₁ x₂ y₂) (mergeWith g xs ys) fun bf =>
        KVChain.cons x₁ bf (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))).toList
Tactic:
dsimp
Proof state after:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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 g xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))) (g x₁ x₂ y₂)).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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 g xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))) (g x₁ x₂ y₂)).toList
Tactic:
rw [hfg]
Proof state after:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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)))
        (g x₁ x₂ y₂)).toList =
    (Option.rec (mergeWith g xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))) (g x₁ x₂ y₂)).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a.e.e.refl
α : 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✝ ys : KVChain r β
h_ind_ys : mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys = mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys
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)))
        (g x₁ x₂ y₂)).toList =
    (Option.rec (mergeWith g xs ys)
        (fun val => KVChain.cons x₁ val (mergeWith g xs ys) (_ : boundLeft x₁ (mergeWith g xs ys))) (g x₁ x₂ y₂)).toList
Tactic:
cases g x₁ x₂ y₂ <;> dsimp <;> rw [h_ind_xs]
Proof state after:
no goals
Theorem: KVChain.mergeWith_congrFun
Proof state before:
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
Tactic:
rw [cons_mergeWith_cons_rel 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₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (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.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₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (mergeWith g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList
Tactic:
rw [cons_mergeWith_cons_rel 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₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (KVChain.cons x₁ x₂ (mergeWith g xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith g xs (KVChain.cons y₁ y₂ ys hys)))).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
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₁
⊢ (KVChain.cons x₁ x₂ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)))).toList =
    (KVChain.cons x₁ x₂ (mergeWith g xs (KVChain.cons y₁ y₂ ys hys))
        (_ : boundLeft x₁ (mergeWith g xs (KVChain.cons y₁ y₂ ys hys)))).toList
Tactic:
dsimp
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₁
⊢ { fst := x₁, snd := x₂ } :: (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)).toList =
    { fst := x₁, snd := x₂ } :: (mergeWith g xs (KVChain.cons y₁ y₂ ys hys)).toList
Theorem: KVChain.mergeWith_congrFun
Proof state before:
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₁
⊢ { fst := x₁, snd := x₂ } :: (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)).toList =
    { fst := x₁, snd := x₂ } :: (mergeWith g xs (KVChain.cons y₁ y₂ ys hys)).toList
Tactic:
rw [h_ind_xs]
Proof state after:
no goals
Theorem: KVChain.mergeWith_congrFun
Proof state before:
case a.e.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₁
hy₁x₁ : r y₁ x₁
⊢ (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:
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✝ 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₁
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 g (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys)).toList