-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Cofix (goal)
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x_1 : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : Cofix F α),
      a =
          corec (F := F) (α := α) (β := Cofix F α ⊕ β)
            (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
              (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
              (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
                (fun (val : Cofix F α) ↦
                  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
                fun (val : β) ↦ g val))
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec (F := F) (α := α) (β := Cofix F α ⊕ β)
      (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
        (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
        (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
          (fun (val : Cofix F α) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (a.dest (F := F) (α := α)) (b.dest (F := F) (α := α))
have h : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (corec (F := F) (α := α)
        (Function.comp (β := F (α ::: (Cofix F α ⊕ β)))
          (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
          (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
            (fun (val : Cofix F α) ↦
              MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
            fun (val : β) ↦ g val))))
    (Function.comp (α := Cofix F α ⊕ β) (β := F (α ::: (Cofix F α ⊕ β)))
      (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Cofix F α ⊕ β) ↦ x))
      (Sum.rec (motive := fun (x : Cofix F α ⊕ β) ↦ F (α ::: (Cofix F α ⊕ β)))
        (fun (val : Cofix F α) ↦
          MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) (val.dest (F := F) (α := α)))
        fun (val : β) ↦ g val)
      (Sum.inl x)))
  (x.dest (F := F) (α := α))
Tactic: rw [Ha, Hb, Cofix.dest_corec]