Theorem: KVChain.rklex_mergeWith_right
Proof state before:
case 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 : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬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:
apply dite (r z₁ a) <;> intro hz₁a
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 : α
b : β a
xs ys : KVChain r fun a => β a
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬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))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))

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 :
  (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
haxs : boundLeft a xs
hays : boundLeft a ys
htail : KVChain.rklex s xs ys
h_ind :
  KVChain.rklex s (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) xs (KVChain.cons z₁ z₂ zs hzs))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) ys (KVChain.cons z₁ z₂ zs hzs))
haz₁ : ¬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))
    (mergeWith (fun a b₁ b₂ => some (f a b₁ b₂)) (KVChain.cons a b ys hays) (KVChain.cons z₁ z₂ zs hzs))