internlm/Lean-Github huggingface dataset:
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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : r z₁ a₂
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)))
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₂ b₂ ys hays) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₂ b₂ ys hays) zs)))
Tactic:
apply KVChain.rklex.tail
Proof state after:
case t.a
α : 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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : r z₁ a₂
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₂ b₂ ys hays) zs)
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case t.a
α : 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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : r z₁ a₂
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₂ b₂ ys hays) zs)
Tactic:
exact h_ind_zs _ _ (KVChain.rklex.headFst ha₂a₁)
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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 ha₂z₁]
Proof state after:
case e.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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))))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : ¬r z₁ a₁
ha₁z₁ : ¬r a₁ z₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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))))
Tactic:
have : z₁ = a₁ := Trichotomous.eq_of_incomp ⟨hz₁a₁, ha₁z₁⟩
Proof state after:
case e.t.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : ¬r z₁ a₁
ha₁z₁ : ¬r a₁ z₁
this : z₁ = a₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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))))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : ¬r z₁ a₁
ha₁z₁ : ¬r a₁ z₁
this : z₁ = a₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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))))
Tactic:
cases this
Proof state after:
case e.t.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 :
  (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₂
xs ys : KVChain r fun a => β a
hays : boundLeft a₂ ys
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
b₁ : β z₁
haxs : boundLeft z₁ xs
ha₂a₁ : r a₂ z₁
hz₁a₁ ha₁z₁ : ¬r z₁ z₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons z₁ b₁ xs haxs) (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))))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.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 :
  (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₂
xs ys : KVChain r fun a => β a
hays : boundLeft a₂ ys
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
b₁ : β z₁
haxs : boundLeft z₁ xs
ha₂a₁ : r a₂ z₁
hz₁a₁ ha₁z₁ : ¬r z₁ z₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons z₁ b₁ xs haxs) (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))))
Tactic:
rw [cons_mergeWith_cons_rfl]
Proof state after:
case e.t.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 :
  (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₂
xs ys : KVChain r fun a => β a
hays : boundLeft a₂ ys
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
b₁ : β z₁
haxs : boundLeft z₁ xs
ha₂a₁ : r a₂ z₁
hz₁a₁ ha₁z₁ : ¬r z₁ z₁
⊢ KVChain.rklex s
    (Option.casesOn (some (f z₁ b₁ z₂)) (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs) fun bf =>
      KVChain.cons z₁ bf (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)))
    (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))))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.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 :
  (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₂
xs ys : KVChain r fun a => β a
hays : boundLeft a₂ ys
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
b₁ : β z₁
haxs : boundLeft z₁ xs
ha₂a₁ : r a₂ z₁
hz₁a₁ ha₁z₁ : ¬r z₁ z₁
⊢ KVChain.rklex s
    (Option.casesOn (some (f z₁ b₁ z₂)) (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs) fun bf =>
      KVChain.cons z₁ bf (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)
        (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs zs)))
    (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))))
Tactic:
exact KVChain.rklex.headFst ha₂a₁
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : r z₁ a₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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))))
Tactic:
rw [cons_mergeWith_cons_flip hz₁a₁]
Proof state after:
case e.t.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : r z₁ a₁
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)))
    (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))))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : r z₁ a₁
⊢ KVChain.rklex s
    (KVChain.cons z₁ z₂ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)
      (_ : boundLeft z₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) zs)))
    (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))))
Tactic:
exact KVChain.rklex.headFst ha₂z₁
Proof state after:
no goals
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.e.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : ¬r z₁ a₁
ha₁z₁ : r a₁ z₁
⊢ KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a₁ b₁ xs haxs) (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))))
Tactic:
rw [cons_mergeWith_cons_rel ha₁z₁]
Proof state after:
case e.t.e.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : ¬r z₁ a₁
ha₁z₁ : r a₁ z₁
⊢ KVChain.rklex s
    (KVChain.cons a₁ b₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
      (_ : boundLeft a₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (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))))
Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case e.t.e.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 :
  (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₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
xs ys : KVChain r fun a => β a
haxs : boundLeft a₁ xs
hays : boundLeft a₂ ys
ha₂a₁ : r a₂ a₁
hz₁a₂ : ¬r z₁ a₂
ha₂z₁ : r a₂ z₁
hz₁a₁ : ¬r z₁ a₁
ha₁z₁ : r a₁ z₁
⊢ KVChain.rklex s
    (KVChain.cons a₁ b₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
      (_ : boundLeft a₁ (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (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))))
Tactic:
exact KVChain.rklex.headFst ha₂a₁
Proof state after:
no goals