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
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) (α := α)) ∘
            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)))
⊢ 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)))

Tactic:
rw [MvFunctor.map_map, MvFunctor.map_map, ← appendFun_comp_id, ← appendFun_comp_id]

Premises used: TypeVec.appendFun_comp_id, MvFunctor.map_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 : (P F).M α
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)))
                  ⋯)) ∘
          Quot.mk (Mcongr (F := F) (α := α)))
        x)
      (Quot.mk (Mcongr (F := F) (α := α)) x)
⊢ 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)))

Tactic:
apply liftR_map_last

Premises used: MvQPF.liftR_map_last
-- 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 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)))
                ⋯)) ∘
        Quot.mk (Mcongr (F := F) (α := α)))
      x)
    (Quot.mk (Mcongr (F := F) (α := α)) x)

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 Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
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) (α := α))
⊢ 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₀))

Tactic:
mv_bisim x₀ with R a b x Ha Hb
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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)
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))))
⊢ LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (a.dest (F := F) (α := α)) (b.dest (F := F) (α := α))

Tactic:
rw [Ha, Hb, Cofix.dest_corec, Cofix.dest_corec, Function.comp_apply, Function.comp_apply]

Premises used: MvQPF.Cofix.dest_corec, Function.comp_apply
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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)
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)))
⊢ 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 [MvFunctor.map_map, ← appendFun_comp_id]

Premises used: TypeVec.appendFun_comp_id, MvFunctor.map_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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) (α := α ::: 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:
liftR_map_last _ _ _ _ ?_

Premises used: MvQPF.liftR_map_last
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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)
refine :
  ∀ (x : X),
    R (Cofix.corec (F := F) (α := α) (g ∘ f) x)
      ((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) (α := α ::: 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:
refine liftR_map_last _ _ _ _ ?_

Premises used: MvQPF.liftR_map_last
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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_1 b : Cofix F α
x : X
Ha : a_1 = 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)
a : X
⊢ R (Cofix.corec (F := F) (α := α) (g ∘ f) a)
    ((Cofix.corec (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
            g) ∘
        f)
      a)

Tactic:
⟨a, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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_1 b : Cofix F α
x : X
Ha : a_1 = 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)
a : X
⊢ R (Cofix.corec (F := F) (α := α) (g ∘ f) a)
    ((Cofix.corec (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) f) ∘
            g) ∘
        f)
      a)

Tactic:
refine ⟨a, rfl, rfl⟩
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
rw :
  MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α)
          (Sum.elim
            (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
              dest (F := F) (α := α))
            g)))
      (Sum.elim
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
          dest (F := F) (α := α))
        g (Sum.inr x)) =
    MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sum.elim _root_.id (corec' (F := F) (α := α) g))) (g x)
⊢ (corec' (F := F) (α := α) g x).dest (F := F) (α := α) =
    MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sum.elim _root_.id (corec' (F := F) (α := α) g))) (g x)

Tactic:
rw [Cofix.corec', Cofix.dest_corec]

Premises used: MvQPF.Cofix.dest_corec, MvQPF.Cofix.corec'
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
dsimp :
  MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α)
          (Sum.elim
            (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
              dest (F := F) (α := α))
            g)))
      (g x) =
    MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sum.elim _root_.id (corec' (F := F) (α := α) g))) (g x)
⊢ MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α)
          (Sum.elim
            (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
              dest (F := F) (α := α))
            g)))
      (Sum.elim
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
          dest (F := F) (α := α))
        g (Sum.inr x)) =
    MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sum.elim _root_.id (corec' (F := F) (α := α) g))) (g x)

Tactic:
dsimp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
h :
  corec (F := F) (α := α)
      (Sum.elim
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
          dest (F := F) (α := α))
        g) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g)
⊢ MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (corec (F := F) (α := α)
          (Sum.elim
            (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
              dest (F := F) (α := α))
            g)))
      (g x) =
    MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sum.elim _root_.id (corec' (F := F) (α := α) g))) (g x)

Tactic:
congr!
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
h :
  ∀ (i : Cofix F α),
    corec (F := F) (α := α)
        (Sum.elim
          (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
            dest (F := F) (α := α))
          g)
        (Sum.inl i) =
      Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inl i)
h₁ :
  ∀ (i : β),
    corec (F := F) (α := α)
        (Sum.elim
          (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
            dest (F := F) (α := α))
          g)
        (Sum.inr i) =
      Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inr i)
⊢ corec (F := F) (α := α)
      (Sum.elim
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
          dest (F := F) (α := α))
        g) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g)

Tactic:
ext (i | 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
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : Cofix F α
h :
  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) ∘
                dest (F := F) (α := α))
              val)
          fun (val : β) ↦ g val))
      (Sum.inl i) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inl i)
⊢ corec (F := F) (α := α)
      (Sum.elim
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
          dest (F := F) (α := α))
        g)
      (Sum.inl i) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inl i)

Tactic:
erw [corec_roll]

Premises used: MvQPF.corec_roll