Theorem: KVChain.forAll_fst_insertWithAux
Proof 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
Proof 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