internlm/Lean-Github huggingface dataset:
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₁
⊢ (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
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 =
    (KVChain.cons y₁ y₂ (mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys))).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₁
⊢ (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 g (KVChain.cons x₁ x₂ xs hxs) ys)
        (_ : boundLeft y₁ (mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys))).toList
Tactic:
dsimp
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₁
⊢ { fst := y₁, snd := y₂ } :: (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys).toList =
    { fst := y₁, snd := y₂ } :: (mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys).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₁
⊢ { fst := y₁, snd := y₂ } :: (mergeWith f (KVChain.cons x₁ x₂ xs hxs) ys).toList =
    { fst := y₁, snd := y₂ } :: (mergeWith g (KVChain.cons x₁ x₂ xs hxs) ys).toList
Tactic:
rw [h_ind_ys]
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs ys zs : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
x✝¹ x✝ : KVChain r fun a => β a
⊢ KVChain.rklex s x✝¹ x✝ →
    KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝¹ KVChain.nil)
      (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝ 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)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs ys zs : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
x✝¹ x✝ : KVChain r fun a => β a
⊢ KVChain.rklex s x✝¹ x✝ → KVChain.rklex s x✝¹ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝ KVChain.nil)
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs ys zs : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
x✝¹ x✝ : KVChain r fun a => β a
⊢ KVChain.rklex s x✝¹ x✝ → KVChain.rklex s x✝¹ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) x✝ KVChain.nil)
Tactic:
exact id
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
have h_ind_zs := h_ind_zs KVChain.nil
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  (fun zs =>
      ∀ (xs ys : KVChain r fun a => β a),
        KVChain.rklex s xs ys →
          KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
            (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs))
    zs
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
dsimp at *
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) KVChain.nil (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
rw [nil_mergeWith] at *
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
haz₁ : ¬r a z₁
hz₁a : ¬r z₁ a
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
have : a = z₁ := Trichotomous.eq_of_incomp ⟨haz₁, hz₁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)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
haz₁ : ¬r a z₁
hz₁a : ¬r z₁ a
this : a = z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
haz₁ : ¬r a z₁
hz₁a : ¬r z₁ a
this : a = z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
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)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
ys : KVChain r fun a => β a
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
b : β z₁
hays : boundLeft z₁ ys
haz₁ hz₁a : ¬r z₁ z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons z₁ b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
ys : KVChain r fun a => β a
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
b : β z₁
hays : boundLeft z₁ ys
haz₁ hz₁a : ¬r z₁ z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons z₁ b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
rw [cons_mergeWith_cons_rfl]
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)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
ys : KVChain r fun a => β a
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
b : β z₁
hays : boundLeft z₁ ys
haz₁ hz₁a : ¬r z₁ z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (Option.casesOn (some (f z₁ b z₂)) (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs) fun bf =>
      KVChain.cons z₁ bf (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
        (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
ys : KVChain r fun a => β a
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
b : β z₁
hays : boundLeft z₁ ys
haz₁ hz₁a : ¬r z₁ z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (Option.casesOn (some (f z₁ b z₂)) (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs) fun bf =>
      KVChain.cons z₁ bf (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
        (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)))
Tactic:
exact KVChain.rklex.headSnd $ hsf_right _ _ _
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
haz₁ : r a z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))
Tactic:
rw [cons_mergeWith_cons_rel haz₁]
Proof state after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f✝ : (a : α) → β a → β a → Option (β a)
s : (a : α) → β a → β a → Prop
f : (a : α) → β a → β a → β a
xs✝ ys✝¹ zs✝ : KVChain r β
hsf_right : ∀ (a : α) (b₁ b : β a), s a b₁ (f a b b₁)
hsf_stab : ∀ (a : α) (b₁ b₂ b : β a), s a b₁ b₂ → s a (f a b₁ b) (f a b₂ b)
z₁ : α
z₂ : β z₁
zs : KVChain r fun a => β a
hzs : boundLeft z₁ zs
h_ind_zs✝ :
  ∀ (xs ys : KVChain r fun a => β a),
    KVChain.rklex s xs ys →
      KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
xs ys✝ : KVChain r fun a => β a
h : KVChain.rklex s xs ys✝
a : α
b : β a
ys : KVChain r fun a => β a
hays : boundLeft a ys
h_ind_zs :
  ∀ (ys : KVChain r fun a => β a),
    KVChain.rklex s KVChain.nil ys → KVChain.rklex s zs (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys zs)
haz₁ : r a z₁
⊢ KVChain.rklex s (KVChain.cons z₁ z₂ zs hzs)
    (KVChain.cons a b (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
      (_ : boundLeft a (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))))