Theorem: KVChain.forAll_fst_insertWithAux (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 : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
⊢ ∀ {p : α → Prop},
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
Tactic:
intro p
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
p : α → Prop
⊢ List.forAll (p ∘ Sigma.fst) xs.toList →
    List.forAll (p ∘ Sigma.fst) ys.toList →
      p a →
        List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
ys : KVChain r β
hxsys : hingeable xs ys
a : α
b : β a
haxs : boundLeft a xs
p : α → Prop
⊢ List.forAll (p ∘ Sigma.fst) xs.toList →
    List.forAll (p ∘ Sigma.fst) ys.toList →
      p a →
        List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
Tactic:
revert xs
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ {xs : KVChain (flip r) β} {hxsys : hingeable xs ys} {haxs : boundLeft a xs},
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ {xs : KVChain (flip r) β} {hxsys : hingeable xs ys} {haxs : boundLeft a xs},
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
Tactic:
apply ys.recOnList (motive:=λ ys=>∀ xs hxsys haxs, xs.toList.forAll (p ∘ Sigma.fst) → ys.toList.forAll (p ∘ Sigma.fst) → p a → (insertWithAux f xs ys hxsys a b haxs).val.fst.toList.forAll (p ∘ Sigma.fst) ∧ (insertWithAux f xs ys hxsys a b haxs).val.snd.toList.forAll (p ∘ Sigma.fst))
State after:
case nil
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) KVChain.nil.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.toList

case cons
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            List.forAll (p ∘ Sigma.fst) xs.toList →
              List.forAll (p ∘ Sigma.fst) ys.toList →
                p a →
                  List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
                    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            List.forAll (p ∘ Sigma.fst) xs.toList →
              List.forAll (p ∘ Sigma.fst) ys.toList →
                p a →
                  List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
                    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList)
        (KVChain.cons a_1 b_1 xs haxs)

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) KVChain.nil.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.toList
Tactic:
case nil =>
  intro xs hxsys haxs hpxs _ hpa
  dsimp [insertWithAux, insertWithAux.loop]
  exact ⟨⟨hpa, hpxs⟩, True.intro⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            List.forAll (p ∘ Sigma.fst) xs.toList →
              List.forAll (p ∘ Sigma.fst) ys.toList →
                p a →
                  List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
                    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            List.forAll (p ∘ Sigma.fst) xs.toList →
              List.forAll (p ∘ Sigma.fst) ys.toList →
                p a →
                  List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
                    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
case cons =>
  intro a₁ b₁ ys ha₁ys h_ind xs ha₁xs hzxs hpxs hpys hpa
  apply dite (r a₁ a) <;> intro ha₁a
  . rw [insertWithAux_cons_rel ha₁a]
    exact h_ind (xs.cons a₁ b₁ (hingeable_cons ▸ ha₁xs)) (cons_hingeable.symm ▸ ha₁ys) ha₁a ⟨hpys.left, hpxs⟩ hpys.right hpa
  . apply dite (r a a₁) <;> intro haa₁
    . rw [insertWithAux_cons_flip haa₁]
      dsimp
      exact ⟨⟨hpa,hpxs⟩,hpys⟩
    . have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
      cases this
      rw [insertWithAux_cons_rfl]
      cases f a b₁ b
      case none => exact ⟨hpxs, hpys.right⟩
      case some bf => exact ⟨⟨hpys.left, hpxs⟩, hpys.right⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs KVChain.nil) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) KVChain.nil.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.toList
Tactic:
intro xs hxsys haxs hpxs _ hpa
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs KVChain.nil
haxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
a✝ : List.forAll (p ∘ Sigma.fst) KVChain.nil.toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs KVChain.nil
haxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
a✝ : List.forAll (p ∘ Sigma.fst) KVChain.nil.toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs KVChain.nil hxsys a b haxs).val.snd.toList
Tactic:
dsimp [insertWithAux, insertWithAux.loop]
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs KVChain.nil
haxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
a✝ : List.forAll (p ∘ Sigma.fst) KVChain.nil.toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) ({ fst := a, snd := b } :: xs.toList) ∧ List.forAll (p ∘ Sigma.fst) []

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
xs : KVChain (flip r) fun a => β a
hxsys : hingeable xs KVChain.nil
haxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
a✝ : List.forAll (p ∘ Sigma.fst) KVChain.nil.toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) ({ fst := a, snd := b } :: xs.toList) ∧ List.forAll (p ∘ Sigma.fst) []
Tactic:
exact ⟨⟨hpa, hpxs⟩, True.intro⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys : KVChain r β
a : α
b : β a
p : α → Prop
⊢ ∀ (a_1 : α) (b_1 : β a_1) (xs : KVChain r fun a => β a) (haxs : boundLeft a_1 xs),
    (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            List.forAll (p ∘ Sigma.fst) xs.toList →
              List.forAll (p ∘ Sigma.fst) ys.toList →
                p a →
                  List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
                    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList)
        xs →
      (fun ys =>
          ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
            List.forAll (p ∘ Sigma.fst) xs.toList →
              List.forAll (p ∘ Sigma.fst) ys.toList →
                p a →
                  List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
                    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList)
        (KVChain.cons a_1 b_1 xs haxs)
Tactic:
intro a₁ b₁ ys ha₁ys h_ind xs ha₁xs hzxs hpxs hpys hpa
State after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
apply dite (r a₁ a) <;> intro ha₁a
State after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
. rw [insertWithAux_cons_rel ha₁a]
  exact h_ind (xs.cons a₁ b₁ (hingeable_cons ▸ ha₁xs)) (cons_hingeable.symm ▸ ha₁ys) ha₁a ⟨hpys.left, hpxs⟩ hpys.right hpa
State after:
case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
. apply dite (r a a₁) <;> intro haa₁
  . rw [insertWithAux_cons_flip haa₁]
    dsimp
    exact ⟨⟨hpa,hpxs⟩,hpys⟩
  . have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
    cases this
    rw [insertWithAux_cons_rfl]
    cases f a b₁ b
    case none => exact ⟨hpxs, hpys.right⟩
    case some bf => exact ⟨⟨hpys.left, hpxs⟩, hpys.right⟩
State after:
no goals

State before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
rw [insertWithAux_cons_rel ha₁a]
State after:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : r a₁ a
⊢ List.forAll (p ∘ Sigma.fst)
      (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
              (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
              (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.snd.toList

State before:
case t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : r a₁ a
⊢ List.forAll (p ∘ Sigma.fst)
      (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
              (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (insertWithAux f (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys
              (_ : hingeable (KVChain.cons a₁ b₁ xs (_ : boundLeft a₁ xs)) ys) a b ha₁a).val.snd.toList
Tactic:
exact h_ind (xs.cons a₁ b₁ (hingeable_cons ▸ ha₁xs)) (cons_hingeable.symm ▸ ha₁ys) ha₁a ⟨hpys.left, hpxs⟩ hpys.right hpa
State after:
no goals

State before:
case e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
apply dite (r a a₁) <;> intro haa₁
State after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
. rw [insertWithAux_cons_flip haa₁]
  dsimp
  exact ⟨⟨hpa,hpxs⟩,hpys⟩
State after:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
. have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
  cases this
  rw [insertWithAux_cons_rfl]
  cases f a b₁ b
  case none => exact ⟨hpxs, hpys.right⟩
  case some bf => exact ⟨⟨hpys.left, hpxs⟩, hpys.right⟩
State after:
no goals

State before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
rw [insertWithAux_cons_flip haa₁]
State after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst)
      { val := (KVChain.cons a b xs hzxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      { val := (KVChain.cons a b xs hzxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.snd.toList

State before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst)
      { val := (KVChain.cons a b xs hzxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      { val := (KVChain.cons a b xs hzxs, KVChain.cons a₁ b₁ ys ha₁ys), property := haa₁ }.val.snd.toList
Tactic:
dsimp
State after:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst) ({ fst := a, snd := b } :: xs.toList) ∧
    List.forAll (p ∘ Sigma.fst) ({ fst := a₁, snd := b₁ } :: ys.toList)

State before:
case e.t
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : r a a₁
⊢ List.forAll (p ∘ Sigma.fst) ({ fst := a, snd := b } :: xs.toList) ∧
    List.forAll (p ∘ Sigma.fst) ({ fst := a₁, snd := b₁ } :: ys.toList)
Tactic:
exact ⟨⟨hpa,hpxs⟩,hpys⟩
State after:
no goals

State before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
have : a = a₁ := Trichotomous.eq_of_incomp ⟨haa₁, ha₁a⟩
State after:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
this : a = a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
case e.e
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
a₁ : α
b₁ : β a₁
ys : KVChain r fun a => β a
ha₁ys : boundLeft a₁ ys
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
ha₁xs : hingeable xs (KVChain.cons a₁ b₁ ys ha₁ys)
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a₁ b₁ ys ha₁ys).toList
hpa : p a
ha₁a : ¬r a₁ a
haa₁ : ¬r a a₁
this : a = a₁
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a₁ b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
cases this
State after:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList

State before:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a b₁ ys ha₁ys) ha₁xs a b hzxs).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst) (insertWithAux f xs (KVChain.cons a b₁ ys ha₁ys) ha₁xs a b hzxs).val.snd.toList
Tactic:
rw [insertWithAux_cons_rfl]
State after:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList

State before:
case e.e.refl
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (f a b₁ b) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList
Tactic:
cases f a b₁ b
State after:
case e.e.refl.none
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList

case e.e.refl.some
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
val✝ : β a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (some val✝) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (some val✝) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList
Tactic:
case none => exact ⟨hpxs, hpys.right⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
bf : β a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (some bf) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (some bf) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList
Tactic:
case some bf => exact ⟨⟨hpys.left, hpxs⟩, hpys.right⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn none { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList
Tactic:
exact ⟨hpxs, hpys.right⟩
State after:
no goals

State before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
ys✝ : KVChain r β
a : α
b : β a
p : α → Prop
ys : KVChain r fun a => β a
h_ind :
  ∀ (xs : KVChain (flip r) fun a => β a) (hxsys : hingeable xs ys) (haxs : boundLeft a xs),
    List.forAll (p ∘ Sigma.fst) xs.toList →
      List.forAll (p ∘ Sigma.fst) ys.toList →
        p a →
          List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.fst.toList ∧
            List.forAll (p ∘ Sigma.fst) (insertWithAux f xs ys hxsys a b haxs).val.snd.toList
xs : KVChain (flip r) fun a => β a
hzxs : boundLeft a xs
hpxs : List.forAll (p ∘ Sigma.fst) xs.toList
hpa : p a
b₁ : β a
ha₁ys : boundLeft a ys
ha₁xs : hingeable xs (KVChain.cons a b₁ ys ha₁ys)
hpys : List.forAll (p ∘ Sigma.fst) (KVChain.cons a b₁ ys ha₁ys).toList
ha₁a haa₁ : ¬r a a
bf : β a
⊢ List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (some bf) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.fst.toList ∧
    List.forAll (p ∘ Sigma.fst)
      (Option.casesOn (some bf) { val := (xs, ys), property := (_ : hingeable (xs, ys).fst (xs, ys).snd) } fun bf =>
              { val := (KVChain.cons a bf xs hzxs, ys),
                property :=
                  (_ : hingeable (KVChain.cons a bf xs hzxs) (KVChain.cons a bf xs hzxs, ys).snd) }).val.snd.toList
Tactic:
exact ⟨⟨hpys.left, hpxs⟩, hpys.right⟩
State after:
no goals