Theorem: KVChain.mergeWith_flip (Algdata/Data/KVChain/MergeWith.lean)

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs ys x✝ : KVChain r β
⊢ mergeWith f KVChain.nil x✝ = mergeWith (fun a => flip (f a)) x✝ KVChain.nil
Tactic:
simp
State after:
no goals

State before:
α : 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 β
⊢ mergeWith f (KVChain.cons x₁ x₂ xs hxs) KVChain.nil =
    mergeWith (fun a => flip (f a)) KVChain.nil (KVChain.cons x₁ x₂ xs hxs)
Tactic:
simp
State after:
no goals

State before:
α : 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)
⊢ mergeWith f (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) =
    mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)
Tactic:
apply eq_of_toList_eq
State after:
case a
α : 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)
⊢ (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

State before:
case a
α : 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)
⊢ (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 x₁ y₁) <;> intro hx₁y₁
State after:
case a.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₁
⊢ (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
α : 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

State before:
case a.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₁
⊢ (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
α : 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:
. rw [cons_mergeWith_cons_rel hx₁y₁]
  rw [cons_mergeWith_cons_flip hx₁y₁]
  dsimp
  rw [h_ind_xs]
State after:
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

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₁
  . rw [cons_mergeWith_cons_flip hy₁x₁]
    rw [cons_mergeWith_cons_rel hy₁x₁]
    dsimp
    rw [h_ind_ys]
  . 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]
State after:
no goals

State before:
case a.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₁
⊢ (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_rel hx₁y₁]
State after:
case a.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₁
⊢ (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 (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList

State before:
case a.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₁
⊢ (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 (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) (KVChain.cons x₁ x₂ xs hxs)).toList
Tactic:
rw [cons_mergeWith_cons_flip hx₁y₁]
State after:
case a.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₁
⊢ (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 (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs)
        (_ : boundLeft x₁ (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs))).toList

State before:
case a.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₁
⊢ (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 (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs)
        (_ : boundLeft x₁ (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs))).toList
Tactic:
dsimp
State after:
case a.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₁
⊢ { fst := x₁, snd := x₂ } :: (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)).toList =
    { fst := x₁, snd := x₂ } :: (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs).toList

State before:
case a.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₁
⊢ { fst := x₁, snd := x₂ } :: (mergeWith f xs (KVChain.cons y₁ y₂ ys hys)).toList =
    { fst := x₁, snd := x₂ } :: (mergeWith (fun a => flip (f a)) (KVChain.cons y₁ y₂ ys hys) xs).toList
Tactic:
rw [h_ind_xs]
State after:
no goals

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₁
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

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]
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

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]
State after:
no goals

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₁]
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

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₁]
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

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
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

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]
State after:
no goals

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₁⟩
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

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
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

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]
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

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 *
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

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]
State after:
no goals