awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq :
  (u x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀))
vx'eq :
  (v x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁))
h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
f'₁ :
  ∀ (i : Fin2 (n + 1)) (j : (P F).B a i),
    α.RelLast R ((P F).appendContents (α := α) f' f₀ i j) ((P F).appendContents (α := α) f' f₁ i j)
⊢ ∃ (a : (P F).A) (f₀ : (P F).B a ⟹ α ::: Cofix F α) (f₁ : (P F).B a ⟹ α ::: Cofix F α),
    x.dest (F := F) (α := α) =
        MvQPF.abs (F := F) (α := α ::: Cofix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a f₀) ∧
      y.dest (F := F) (α := α) =
          MvQPF.abs (F := F) (α := α ::: Cofix F α)
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a f₁) ∧
        ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast R (f₀ i j) (f₁ i j)

Tactic:
refine
        ⟨a, q.P.appendContents f' f₀, q.P.appendContents f' f₁, xeq.symm ▸ ux'eq,
          yeq.symm ▸ vx'eq, ?_⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq :
  (u x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀))
vx'eq :
  (v x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁))
h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
i : Fin2 (n + 1)
fz :
  ∀ (j : (P F).B a Fin2.fz),
    α.RelLast R ((P F).appendContents (α := α) f' f₀ Fin2.fz j) ((P F).appendContents (α := α) f' f₁ Fin2.fz j)
fs :
  ∀ (a_1 : Fin2 n) (j : (P F).B a a_1.fs),
    α.RelLast R ((P F).appendContents (α := α) f' f₀ a_1.fs j) ((P F).appendContents (α := α) f' f₁ a_1.fs j)
⊢ ∀ (j : (P F).B a i), α.RelLast R ((P F).appendContents (α := α) f' f₀ i j) ((P F).appendContents (α := α) f' f₁ i j)

Tactic:
cases i
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq :
  (u x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀))
vx'eq :
  (v x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁))
h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
⊢ ∀ (j : (P F).B a Fin2.fz),
    α.RelLast R ((P F).appendContents (α := α) f' f₀ Fin2.fz j) ((P F).appendContents (α := α) f' f₁ Fin2.fz j)

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ : (P F).last.B a → Cofix F α) (f₁ : (P F).last.B a → Cofix F α),
        (u x).dest (F := F) (α := α) =
            MvQPF.abs (F := F) (α := α ::: Cofix F α)
              (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                ((P F).appendContents (α := α) f' f₀)) ∧
          (v x).dest (F := F) (α := α) =
              MvQPF.abs (F := F) (α := α ::: Cofix F α)
                (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a
                  ((P F).appendContents (α := α) f' f₁)) ∧
            ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x_1 : β
Qx : Q x_1
R : (w z : Cofix F α) → Prop := fun (w z : Cofix F α) ↦ ∃ (x' : β), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
h_1 : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq :
  (u x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₀))
vx'eq :
  (v x').dest (F := F) (α := α) =
    MvQPF.abs (F := F) (α := α ::: Cofix F α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Cofix F α) a ((P F).appendContents (α := α) f' f₁))
h' : ∀ (i : (P F).last.B a), ∃ (x' : β), Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a_1 : Fin2 n
j : (P F).B a a_1.fs
⊢ α.RelLast R ((P F).appendContents (α := α) f' f₀ a_1.fs j) ((P F).appendContents (α := α) f' f₁ a_1.fs j)

Tactic:
apply Eq.refl

Premises used: Eq.refl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : Cofix F α
apply :
  ∀ (x y : Cofix F α),
    (fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) x y →
      Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
          α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
            (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
          (x.dest (F := F) (α := α)))
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
          α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
            (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
          (y.dest (F := F) (α := α)))
⊢ mk (F := F) (α := α) (x.dest (F := F) (α := α)) = x

Tactic:
apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl

Premises used: MvQPF.Cofix.mk, MvQPF.Cofix.bisim_rel, Eq, rfl, MvQPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
rw :
  Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      ((mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))
⊢ Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (x.dest (F := F) (α := α)))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))

Tactic:
rw [h]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
lhs :
  MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
    α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    ((mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α))
| Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      ((mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))

Tactic:
lhs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
a :
  appendFun (α := α) (α' := α) (TypeVec.id (α := α))
    (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
a₁ : (mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)
| MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
    α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    ((mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α))

Tactic:
congr
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
| appendFun (α := α) (α' := α) (TypeVec.id (α := α))
    (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
a :
  dest (F := F) (α := α)
    (corec (F := F) (α := α)
      (fun (x : F (α ::: Cofix F α)) ↦
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
      (y.dest (F := F) (α := α)))
| (mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)

Tactic:
rw [Cofix.mk]

Premises used: MvQPF.Cofix.mk
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
a :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
      (y.dest (F := F) (α := α)))
| dest (F := F) (α := α)
    (corec (F := F) (α := α)
      (fun (x : F (α ::: Cofix F α)) ↦
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x)
      (y.dest (F := F) (α := α)))

Tactic:
rw [Cofix.dest_corec]

Premises used: MvQPF.Cofix.dest_corec
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
a :
  MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
        MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
      (y.dest (F := F) (α := α)))
| Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      ((mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))

Tactic:
lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]

Premises used: MvQPF.Cofix.dest_corec, MvQPF.Cofix.mk
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
conv :
  Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
          (y.dest (F := F) (α := α)))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))
⊢ Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      ((mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))

Tactic:
conv =>
    lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]

Premises used: MvQPF.Cofix.dest_corec, MvQPF.Cofix.mk
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
rw :
  Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        ((Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) ∘
          corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
        (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))
⊢ Eq (α := F (α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: F (α ::: Cofix F α)) (β := α ::: Cofix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (corec (F := F) (α := α) fun (x : F (α ::: Cofix F α)) ↦
            MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x))
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: F (α ::: Cofix F α))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (i : Cofix F α) ↦ i.dest (F := F) (α := α))
          (y.dest (F := F) (α := α)))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β :=
      α ::: Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
      (y.dest (F := F) (α := α)))

Tactic:
rw [← comp_map, ← appendFun_comp, id_comp]

Premises used: MvQPF.comp_map, TypeVec.appendFun_comp, TypeVec.id_comp