Theorem: KVChain.insertWithAux_cons_rfl
Proof state before:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ (if hya : r a a then
      insertWithAux.loop f a b
        (KVChain.cons a b₁ xs
          (_ :
            List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
              (KVChain.cons a b₁ ys hays).toList))
        ys.toList (_ : List.Ascending (Sigma.relOnFst r) ys.toList)
        (_ : List.predHead (Sigma.relOnFst r { fst := a, snd := b₁ }) ys.toList) hya
    else
      if hay : r a a then
        {
          val :=
            (KVChain.cons a b xs haxs',
              { toList := { fst := a, snd := b₁ } :: ys.toList,
                ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a, snd := b₁ } :: ys.toList)) }),
          property :=
            (_ :
              hingeable
                (KVChain.cons a b xs haxs',
                    { toList := { fst := a, snd := b₁ } :: ys.toList,
                      ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a, snd := b₁ } :: ys.toList)) }).fst
                (KVChain.cons a b xs haxs',
                    { toList := { fst := a, snd := b₁ } :: ys.toList,
                      ascend := (_ : List.Ascending (Sigma.relOnFst r) ({ fst := a, snd := b₁ } :: ys.toList)) }).snd) }
      else
        match f a b₁ b with
        | none =>
          { val := (xs, { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
            property :=
              (_ : hingeable xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }
        | some z =>
          {
            val :=
              (KVChain.cons a z xs
                  (_ :
                    List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                      (KVChain.cons a b₁ ys hays).toList),
                { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
            property :=
              (_ :
                hingeable
                  (KVChain.cons a z xs
                    (_ :
                      List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                        (KVChain.cons a b₁ ys hays).toList))
                  { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }) =
    Option.rec { val := (xs, ys), property := (_ : hingeable xs ys) }
      (fun val =>
        { val := (KVChain.cons a val xs haxs', ys), property := (_ : hingeable (KVChain.cons a val xs haxs') ys) })
      (f a b₁ b)
Tactic:
rw [dif_neg (Irreflective.irrefl (r:=r) _), dif_neg (Irreflective.irrefl (r:=r) _)]
Proof state after:
α : Type u
r : α → α → Prop
inst✝¹ : StrictLinearOrder r
inst✝ : DecidableRel r
β : α → Type v
f : (a : α) → β a → β a → Option (β a)
xs : KVChain (flip r) β
a : α
b₁ : β a
ys : KVChain r β
hays : boundLeft a ys
haxs : hingeable xs (KVChain.cons a b₁ ys hays)
b : β a
haxs' : boundLeft a xs
⊢ (match f a b₁ b with
    | none =>
      { val := (xs, { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
        property :=
          (_ : hingeable xs { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }
    | some z =>
      {
        val :=
          (KVChain.cons a z xs
              (_ :
                List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                  (KVChain.cons a b₁ ys hays).toList),
            { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }),
        property :=
          (_ :
            hingeable
              (KVChain.cons a z xs
                (_ :
                  List.predHead (fun b => List.predHead (flip (fun a b => r a.fst b.fst) b) xs.toList)
                    (KVChain.cons a b₁ ys hays).toList))
              { toList := ys.toList, ascend := (_ : List.Ascending (Sigma.relOnFst r) ys.toList) }) }) =
    Option.rec { val := (xs, ys), property := (_ : hingeable xs ys) }
      (fun val =>
        { val := (KVChain.cons a val xs haxs', ys), property := (_ : hingeable (KVChain.cons a val xs haxs') ys) })
      (f a b₁ b)