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
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x : ι' × ι' // uncurry R x } := fun (x : ι) ↦ Subtype.mk (p := fun (x : ι' × ι') ↦ uncurry R x) (f x, g x) ⋯
b : α ::: ι ⟹ Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } :=
  appendFun (α := α) (α' := Subtype_ (α := α ⊗ α) α.repeatEq) (diagSub (α := α)) h
c : Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } ⟹
  (fun (i : Fin2 n) ↦ { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  appendFun (α := Subtype_ (α := α ⊗ α) α.repeatEq) (α' := fun (i : Fin2 n) ↦
    { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) (ofSubtype (α := α ⊗ α) α.repeatEq) _root_.id
h₁ :
  ∀ (x : (α ::: ι).last),
    (Subtype.val ∘
          lastFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
              (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
                TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                  { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
              c ∘
            h)
        x =
      (Prod.map f g ∘ lastFun (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (prod.diag (α := α ::: ι))) x
⊢ Subtype.val ∘
      lastFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
          (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
            TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
              { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
          c ∘
        h =
    Prod.map f g ∘ lastFun (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (prod.diag (α := α ::: ι))

Tactic:
ext1
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
lawful : LawfulMvFunctor F
α : TypeVec.{u} n
ι ι' : Type u
R : ι' → ι' → Prop
x : F (α ::: ι)
f g : ι → ι'
hh : ∀ (x : ι), R (f x) (g x)
h : ι → { x : ι' × ι' // uncurry R x } := fun (x : ι) ↦ Subtype.mk (p := fun (x : ι' × ι') ↦ uncurry R x) (f x, g x) ⋯
b : α ::: ι ⟹ Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } :=
  appendFun (α := α) (α' := Subtype_ (α := α ⊗ α) α.repeatEq) (diagSub (α := α)) h
c : Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x } ⟹
  (fun (i : Fin2 n) ↦ { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) :=
  appendFun (α := Subtype_ (α := α ⊗ α) α.repeatEq) (α' := fun (i : Fin2 n) ↦
    { x : (α ::: ι' ⊗ α ::: ι') i.fs // ofRepeat (α.RelLast' R i.fs x) }) (ofSubtype (α := α ⊗ α) α.repeatEq) _root_.id
x_1 : (α ::: ι).last
⊢ (Subtype.val ∘
        lastFun (α := Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }) (β :=
            (TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) :::
              TypeVec.last (n := n) fun (i : Fin2 (n + 1)) ↦
                { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) })
            c ∘
          h)
      x_1 =
    (Prod.map f g ∘ lastFun (α := α ::: ι) (β := α ::: ι ⊗ α ::: ι) (prod.diag (α := α ::: ι))) x_1

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
⊢ LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id)
      x)

Tactic:
have := liftR_map_last R x f id hh
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this :
  LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id)
      x)
rwa :
  ∀
    (this :
      LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
        (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
        (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (TypeVec.id (α := α ::: ι)) x)),
    LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
      (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
        (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x)
        x),
    LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
      (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x
⊢ LiftR' (α := α ::: ι) (F := F) (α.RelLast' R)
    (MvFunctor.map (F := F) (α := α ::: ι) (β := α ::: ι) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) x) x

Tactic:
rwa [appendFun_id_id, MvFunctor.id_map] at this

Premises used: MvFunctor.id_map, TypeVec.appendFun_id_id
-- 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 α
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
⊢ Quot.mk (Mcongr (F := F) (α := α)) (x.repr (F := F) (α := α)) = x

Tactic:
Cofix.bisim₂ R ?_ _ _ rfl

Premises used: MvQPF.Cofix.bisim₂, MvQPF.Cofix, rfl
-- 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 α
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
refine :
  ∀ (x y : Cofix F α),
    R x y → LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))
⊢ Quot.mk (Mcongr (F := F) (α := α)) (x.repr (F := F) (α := α)) = x

Tactic:
refine Cofix.bisim₂ R ?_ _ _ rfl

Premises used: MvQPF.Cofix.bisim₂, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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
x y : Cofix F α
h : R x y
subst :
  LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    ((abs (F := F) (α := α) (y.repr (F := F) (α := α))).dest (F := F) (α := α)) (y.dest (F := F) (α := α))
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (x.dest (F := F) (α := α)) (y.dest (F := F) (α := α))

Tactic:
subst h
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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
y : Cofix F α
dsimp :
  LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (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) (α := α) (y.repr (F := 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)))
      ⋯ y)
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    ((abs (F := F) (α := α) (y.repr (F := F) (α := α))).dest (F := F) (α := α)) (y.dest (F := F) (α := α))

Tactic:
dsimp [Cofix.dest, Cofix.abs]

Premises used: MvQPF.Cofix.abs, 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
y : Cofix F α
mk :
  ∀ (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) (α := α))))
        (MvQPF.abs (F := F) (α := α ::: (P F).M α)
          (M.dest (P F) (α := α) (repr (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a)))))
      (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))
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (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) (α := α) (y.repr (F := 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)))
      ⋯ y)

Tactic:
induction y using Quot.ind

Premises used: Quot.ind
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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 α
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 α) ∘ 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)))
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R)
    (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) (α := α) (repr (F := F) (α := α) (Quot.mk (Mcongr (F := F) (α := α)) a)))))
    (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))

Tactic:
simp only [Cofix.repr, M.dest_corec, abs_map, MvQPF.abs_repr, Function.comp]

Premises used: MvQPF.abs_repr, Function.comp, MvQPF.Cofix.repr, MvPFunctor.M.dest_corec, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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)))
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))
| 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)))

Tactic:
congr
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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 α
| α.RelLast' R

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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)))
| 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)))

Tactic:
rw [Cofix.dest]

Premises used: 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
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)))
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))
| 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)))

Tactic:
congr; rfl; rw [Cofix.dest]

Premises used: 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
R : (x y : Cofix F α) → Prop := fun (x y : Cofix F α) ↦ abs (F := F) (α := α) (y.repr (F := F) (α := α)) = x
a : (P F).M α
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)))
                ⋯)))
        (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)))
⊢ 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)))

Tactic:
conv => congr; rfl; rw [Cofix.dest]

Premises used: MvQPF.Cofix.dest