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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
R₁ : α.RelLast' R
| LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
        (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a))))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
have a : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
  (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
    (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a)))
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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a_1 : (P F).M α
R₁ : α.RelLast' R
a :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
      (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a_1)))
| LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
        (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a_1))))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a_1)))
have a₁ : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
  (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a_1))
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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
| MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
      (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a)))
have a : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
  (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (M.corec (P F) (α := α)
        (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
          Quot.lift (r := Mcongr (F := F) (α := α))
            (fun (x : (P F).M α) ↦
              MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
            sorry)))
    (Quot.lift (r := Mcongr (F := F) (α := α))
      (fun (x : (P F).M α) ↦
        MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
          (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
      sorry (Quot.mk (Mcongr (F := F) (α := α)) a)))
Tactic: rw [Cofix.dest]
-- 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
| LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
        (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a))))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
have a : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
  (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (M.corec (P F) (α := α)
        (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
          Quot.lift (r := Mcongr (F := F) (α := α))
            (fun (x : (P F).M α) ↦
              MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
            sorry)))
    (Quot.lift (r := Mcongr (F := F) (α := α))
      (fun (x : (P F).M α) ↦
        MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
          (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
      sorry (Quot.mk (Mcongr (F := F) (α := α)) a)))
Tactic: congr; rfl; rw [Cofix.dest]
-- 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a_1 : (P F).M α
a :
  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α)
          (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
            Quot.lift (r := Mcongr (F := F) (α := α))
              (fun (x : (P F).M α) ↦
                MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                  (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
              ⋯)))
      (Quot.lift (r := Mcongr (F := F) (α := α))
        (fun (x : (P F).M α) ↦
          MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
            (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
        ⋯ (Quot.mk (Mcongr (F := F) (α := α)) a_1)))
| LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
        (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a_1))))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a_1)))
have a₁ : MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
  (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a_1))
Tactic: congr; rfl; rw [Cofix.dest]
-- 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α) (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘ dest (F := F) (α := α))))
        (dest (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a))))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
have mk : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (M.corec (P F) (α := α)
          (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
            Quot.lift (r := Mcongr (F := F) (α := α))
              (fun (x : (P F).M α) ↦
                MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                  (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
              sorry)))
      (Quot.lift (r := Mcongr (F := F) (α := α))
        (fun (x : (P F).M α) ↦
          MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
            (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
        sorry (Quot.mk (Mcongr (F := F) (α := α)) a))))
  (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
Tactic: conv => congr; rfl; rw [Cofix.dest]
-- 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (P F).M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (M.corec (P F) (α := α)
            (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
              Quot.lift (r := Mcongr (F := F) (α := α))
                (fun (x : (P F).M α) ↦
                  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                    (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
                ⋯)))
        (Quot.lift (r := Mcongr (F := F) (α := α))
          (fun (x : (P F).M α) ↦
            MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
              (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
          ⋯ (Quot.mk (Mcongr (F := F) (α := α)) a))))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
have mk : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      ((Quot.mk (Mcongr (F := F) (α := α)) ∘
          M.corec (P F) (α := α)
            (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
              Quot.lift (r := Mcongr (F := F) (α := α))
                (fun (x : (P F).M α) ↦
                  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                    (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
                sorry)) ∘
        Quot.mk (Mcongr (F := F) (α := α))))
    (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
  (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
    (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
Tactic: rw [MvFunctor.map_map, MvFunctor.map_map, ← appendFun_comp_id, ← appendFun_comp_id]
-- 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        ((Quot.mk (Mcongr (F := F) (α := α)) ∘
            M.corec (P F) (α := α)
              (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
                Quot.lift (r := Mcongr (F := F) (α := α))
                  (fun (x : (P F).M α) ↦
                    MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
                  ⋯)) ∘
          Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
    (MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
      (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) a)))
have mk : ∀ (x : (P F).M α),
  R
    (((Quot.mk (Mcongr (F := F) (α := α)) ∘
          M.corec (P F) (α := α)
            (MvQPF.repr (F := F) (α := α ::: Cofix F α) ∘
              Quot.lift (r := Mcongr (F := F) (α := α))
                (fun (x : (P F).M α) ↦
                  MvFunctor.map (F := F) (α := α ::: (P F).M α) (β := α ::: Cofix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Mcongr (F := F) (α := α))))
                    (MvQPF.abs (F := F) (α := α ::: (P F).M α) (M.dest (P F) (α := α) x)))
                sorry)) ∘
        Quot.mk (Mcongr (F := F) (α := α)))
      x)
    (Quot.mk (Mcongr (F := F) (α := α)) x)
Tactic: apply liftR_map_last
-- 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 Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
⊢ Eq (α := Cofix F α) (Cofix.corec (F := F) (α := α) (g ∘ f) x₀)
    (Cofix.corec (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘ g)
      (f x₀))
have mv_bisim : let R : Cofix F α → Cofix F α → Prop := fun (a b : Cofix F α) ↦
  ∃ (x : X),
    a = Cofix.corec (F := F) (α := α) (g ∘ f) x ∧
      b =
        Cofix.corec (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
            g)
          (f x);
∀ (a b : Cofix F α) (x : X) (Ha : a = Cofix.corec (F := F) (α := α) (g ∘ f) x)
  (Hb :
    b =
      Cofix.corec (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
          g)
        (f x)),
  LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (a.dest (F := F) (α := α)) (b.dest (F := F) (α := α))
Tactic: mv_bisim x₀ with R a b x Ha Hb
-- 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 Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : X),
      a = Cofix.corec (F := F) (α := α) (g ∘ f) x ∧
        b =
          Cofix.corec (F := F) (α := α)
            (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
              g)
            (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (F := F) (α := α) (g ∘ f) x
Hb :
  b =
    Cofix.corec (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘ g)
      (f x)
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (a.dest (F := F) (α := α)) (b.dest (F := F) (α := α))
have rw : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Cofix.corec (F := F) (α := α) (g ∘ f))) (g (f x)))
  (MvFunctor.map (F := F) (α := α ::: Y) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (Cofix.corec (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
          g)))
    (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
      (g (f x))))
Tactic: rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]
-- 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 Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : X),
      a = Cofix.corec (F := F) (α := α) (g ∘ f) x ∧
        b =
          Cofix.corec (F := F) (α := α)
            (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
              g)
            (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (F := F) (α := α) (g ∘ f) x
Hb :
  b =
    Cofix.corec (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘ g)
      (f x)
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Cofix.corec (F := F) (α := α) (g ∘ f))) (g (f x)))
    (MvFunctor.map (F := F) (α := α ::: Y) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Cofix.corec (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
            g)))
      (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f)
        (g (f x))))
have rw : LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
  (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Cofix.corec (F := F) (α := α) (g ∘ f))) (g (f x)))
  (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Cofix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
      (Cofix.corec (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
            g) ∘
        f))
    (g (f x)))
Tactic: rw [MvFunctor.map_map, ← appendFun_comp_id]