awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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)
⊢ ∀ (j : (P F).B a i), α.RelLast R ((P F).appendContents (α := α) f' f₀ i j) ((P F).appendContents (α := α) f' f₁ i j)
have 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)
Tactic: cases i
Cleared hypotheses: i
-- 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_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)
⊢ ∀ (j : (P F).B a i), α.RelLast R ((P F).appendContents (α := α) f' f₀ i j) ((P F).appendContents (α := α) f' f₁ i j)
have 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)
Tactic: cases i
Cleared hypotheses: i
-- 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
x : Cofix F α
⊢ mk (F := F) (α := α) (x.dest (F := F) (α := α)) = x
have 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) (α := α)))
Tactic: apply Cofix.bisim_rel (fun x y : Cofix F α => x = Cofix.mk (Cofix.dest y)) _ _ _ rfl
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)))
have 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) (α := α)))
Tactic: rw [h]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)))
have 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) (α := α))
Tactic: lhs
-- 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
x_1 x y : Cofix F α
h : 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) (α := α))
have a : appendFun (α := α) (α' := α) (TypeVec.id (α := α))
  (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
Tactic: congr
-- 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
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) (α := α)))
| 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) (α := α))
have a₁ : (mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)
Tactic: congr
-- 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
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
| (mk (F := F) (α := α) (y.dest (F := F) (α := α))).dest (F := F) (α := α)
have 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) (α := α)))
Tactic: rw [Cofix.mk]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)))
have 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) (α := α)))
Tactic: rw [Cofix.dest_corec]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)))
have 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) (α := α)))
Tactic: lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)))
have 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) (α := α)))
Tactic: conv =>
    lhs
    congr
    rfl
    rw [Cofix.mk]
    rw [Cofix.dest_corec]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)))
have 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) (α := α)))
Tactic: rw [← comp_map, ← appendFun_comp, id_comp]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α ::: 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) (α := α)))
have 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) (α := α)) ∘
        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, ← Cofix.mk]
-- 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
x_1 x y : Cofix F α
h : x = mk (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) (α := α)) ∘
          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) (α := α)))
have e_a : Eq.{u + 1} (α :=
  α ::: 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) (α := α)) ∘
      fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)))
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
    (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))))
Tactic: congr 1