-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.dest_corec' {α : TypeVec.{u} n} {β : Type u}
    (g : β → F (α.append1 (Cofix F α ⊕ β))) (x : β) :
    Cofix.dest (Cofix.corec' g x) =
      appendFun id (Sum.elim _root_.id (Cofix.corec' g)) <$$> g x

Proof state:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        (corec fun x =>
            (TypeVec.id ::: fun x => x) <$$>
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x) ∘
          fun x => x) <$$>
      (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest

Tactic:
rw [MvFunctor.map_map, ← appendFun_comp_id]

Result:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x) ∘
            fun x => x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest

Proof state:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R) a.dest b.dest

Tactic:
rw [Ha, Hb, Cofix.dest_corec]

Result:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        corec
          (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
            Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)) <$$>
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
          Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
        (Sum.inl x))
    x.dest

Proof state:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        corec fun x =>
          (TypeVec.id ::: fun x => x) <$$>
            Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x) <$$>
      (TypeVec.id ::: fun x => x) <$$> (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest

Tactic:
repeat rw [MvFunctor.map_map, ← appendFun_comp_id]

Result:
case h.e'_6.h.e'_7.h.inl.intro.intro
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b =>
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
              Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x => x) ∘
        Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val => g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x =>
              (TypeVec.id ::: fun x => x) <$$>
                Sum.rec (fun val => (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val => g val) x) ∘
            fun x => x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest