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
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
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.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.inr i) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inr i)

Tactic:
erw [corec_roll]

Premises used: MvQPF.corec_roll
-- 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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl i) =
    i
⊢ 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)

Tactic:
dsimp [Cofix.corec']

Premises used: 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 i : β
h :
  Eq (α := Cofix F α)
    (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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (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.inr i))
⊢ 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.inr i) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inr i)

Tactic:
dsimp [Cofix.corec']

Premises used: 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 : β
i : Cofix F α
h :
  let R : Cofix F α → Cofix F α → Prop := fun (a b : Cofix F α) ↦
    ∃ (x : Cofix F α),
      a =
          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) (val.dest (F := F) (α := α)))
                fun (val : β) ↦ g val))
            (Sum.inl x) ∧
        b = x;
  ∀ (a b x : Cofix F α)
    (Ha :
      a =
        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) (val.dest (F := F) (α := α)))
              fun (val : β) ↦ g val))
          (Sum.inl x))
    (Hb : b = x),
    LiftR' (α := α ::: Cofix F α) (F := F) (α.RelLast' R) (a.dest (F := F) (α := α)) (b.dest (F := F) (α := α))
⊢ 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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl i) =
    i

Tactic:
mv_bisim i 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x_1 : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : Cofix F α),
      a =
          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) (val.dest (F := F) (α := α)))
                fun (val : β) ↦ g val))
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl x)
Hb : b = x
x_2 : Cofix F α
⊢ R
    (corec (F := F) (α := α)
      (fun (x : 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) (val.dest (F := F) (α := α)))
            (fun (val : β) ↦ g val) x))
      (Sum.inl x_2))
    x_2

Tactic:
⟨_, 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x_1 : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun (a b : Cofix F α) ↦
    ∃ (x : Cofix F α),
      a =
          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) (val.dest (F := F) (α := α)))
                fun (val : β) ↦ g val))
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (Sum.inl x)
Hb : b = x
x_2 : Cofix F α
⊢ R
    (corec (F := F) (α := α)
      (fun (x : 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) (val.dest (F := F) (α := α)))
            (fun (val : β) ↦ g val) x))
      (Sum.inl x_2))
    x_2

Tactic:
exact ⟨_, 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 i : β
h :
  ∀ (y : 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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val)
        y =
      Sum.elim
        (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
          dest (F := F) (α := α))
        g y
⊢ Eq (α := Cofix F α)
    (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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val))
      (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.inr i))

Tactic:
congr 1 with y
-- 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 : β
y : Cofix F α ⊕ β
h :
  (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
          (TypeVec.id (α := α ::: (Cofix F α ⊕ β))) ∘
        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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val)
      y =
    Sum.elim
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
        dest (F := F) (α := α))
      g y
⊢ 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) (val.dest (F := F) (α := α)))
        fun (val : β) ↦ g val)
      y =
    Sum.elim
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
        dest (F := F) (α := α))
      g y

Tactic:
erw [appendFun_id_id]

Premises used: 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: (Cofix F α ⊕ β))
          (TypeVec.id (α := α ::: (Cofix F α ⊕ β))) ∘
        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) (val.dest (F := F) (α := α)))
          fun (val : β) ↦ g val)
      y =
    Sum.elim
      (MvFunctor.map (F := F) (α := α ::: Cofix F α) (β := α ::: (Cofix F α ⊕ β))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) Sum.inl) ∘
        dest (F := F) (α := α))
      g y

Tactic:
simp [MvFunctor.id_map, Sum.elim]

Premises used: MvFunctor.id_map, Sum.elim
-- 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 : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y),
    g (k ∘ f) (k ∘ f') x =
      MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) k)
        (g f f' x)
rw :
  g
      (Function.comp (β := Cofix F α ⊕ β)
        (Sum.elim _root_.id (corec' (F := F) (α := α) fun (x : β) ↦ g Sum.inl Sum.inr x)) Sum.inl)
      (Sum.elim _root_.id (corec' (F := F) (α := α) fun (x : β) ↦ g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ (F := F) (α := α) @g) x
⊢ (corec₁ (F := F) (α := α) (@g) x).dest (F := F) (α := α) = g _root_.id (corec₁ (F := F) (α := α) @g) x

Tactic:
rw [Cofix.corec₁, Cofix.dest_corec', ← h]

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 : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y),
    g (k ∘ f) (k ∘ f') x =
      MvFunctor.map (F := F) (α := α ::: X) (β := α ::: Y) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) k)
        (g f f' x)
⊢ g
      (Function.comp (β := Cofix F α ⊕ β)
        (Sum.elim _root_.id (corec' (F := F) (α := α) fun (x : β) ↦ g Sum.inl Sum.inr x)) Sum.inl)
      (Sum.elim _root_.id (corec' (F := F) (α := α) fun (x : β) ↦ g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ (F := F) (α := α) @g) 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
f : α ⟹ β
p : (↑(P F).mp : (α : TypeVec.{u} n) → Type u) α
⊢ Eq (α := Cofix F β)
    (Quot.mk (Mcongr (F := F) (α := β))
      (MvFunctor.map (F := (↑(P F).mp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f p))
    (MvFunctor.map (F := Cofix F) (α := α) (β := β) f (Quot.mk (Mcongr (F := F) (α := α)) p))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
Goal:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α : TypeVec.{u} m
x : Comp F G α
⊢ Comp.mk (F := F) (G := G) (α := α) (x.get (F := F) (G := G) (α := α)) = x

Tactic:
rfl

Premises used: MvQPF.Comp.get, MvQPF.Comp.mk, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
Goal:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α : TypeVec.{u} m
x : F fun (i : Fin2 n) ↦ G i α
⊢ (Comp.mk (F := F) (G := G) (α := α) x).get (F := F) (G := G) (α := α) = x

Tactic:
rfl

Premises used: MvQPF.Comp.get, MvQPF.Comp.mk, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
Goal:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst : MvFunctor F
inst_1 : (i : Fin2 n) → MvFunctor (G i)
x : F fun (i : Fin2 n) ↦ G i α
⊢ MvFunctor.map (F := Comp F G) (α := α) (β := β) f (Comp.mk (F := F) (G := G) (α := α) x) =
    Comp.mk (F := F) (G := G) (α := β)
      (MvFunctor.map (F := F) (α := fun (i : Fin2 n) ↦ G i α) (β := fun (i : Fin2 n) ↦ G i β)
        (fun (i : Fin2 n) (x : G i α) ↦ MvFunctor.map (F := G i) (α := α) (β := β) f x) x)

Tactic:
rfl

Premises used: MvQPF.Comp.map, MvQPF.Comp.mk, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
Goal:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst : MvFunctor F
inst_1 : (i : Fin2 n) → MvFunctor (G i)
x : Comp F G α
⊢ (MvFunctor.map (F := Comp F G) (α := α) (β := β) f x).get (F := F) (G := G) (α := β) =
    MvFunctor.map (F := F) (α := fun (i : Fin2 n) ↦ G i α) (β := fun (i : Fin2 n) ↦ G i β)
      (fun (i : Fin2 n) (x : G i α) ↦ MvFunctor.map (F := G i) (α := α) (β := β) f x) (x.get (F := F) (G := G) (α := α))

Tactic:
rfl

Premises used: MvQPF.Comp.map, MvQPF.Comp.get, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
Goal:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst_1 : MvQPF F
inst_2 : (i : Fin2 n) → MvQPF (G i)
α_1 : TypeVec.{u} m
x : Comp F G α_1
⊢ Function.comp (α := (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u) α_1)
      (Comp.mk (F := F) (G := G) (α := α_1))
      ((MvFunctor.map (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) α_1) (β :=
          fun (i : Fin2 n) ↦ G i α_1) fun (x : Fin2 n) ↦ abs (F := G x) (α := α_1)) ∘
        abs (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) α_1) ∘ comp.get (α := α_1))
      ((comp.mk (α := α_1) ∘
          repr (F := F) (α := fun (i : Fin2 n) ↦ (↑(P (G i)) : (α : TypeVec.{u} m) → Type u) α_1) ∘
            (MvFunctor.map (F := F) (α := fun (i : Fin2 n) ↦ G i α_1) (β := fun (i : Fin2 n) ↦
                (↑(P (G i)) : (α : TypeVec.{u} m) → Type u) α_1) fun (i : Fin2 n) ↦ repr (F := G i) (α := α_1)) ∘
              Comp.get (F := F) (G := G) (α := α_1))
        x) =
    x

Tactic:
simp +unfoldPartialApp only [Function.comp_def, comp.get_mk, abs_repr,
      map_map, TypeVec.comp, MvFunctor.id_map', Comp.mk_get]

Premises used: MvQPF.abs_repr, MvFunctor.id_map', TypeVec.comp, MvQPF.Comp.mk_get, Function.comp_def, MvPFunctor.comp.get_mk, MvFunctor.map_map