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
x_1 x y : Cofix F α
h : x = mk (F := F) (α := α) (y.dest (F := F) (α := α))
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) (α := α)))
⊢ 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, ← Cofix.mk]

Premises used: MvQPF.comp_map, TypeVec.appendFun_comp, MvQPF.Cofix.mk, TypeVec.id_comp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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) (α := α))
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) (α := α))))
⊢ 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:
congr 1
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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) (α := α))
e_a :
  Eq.{u + 1} (α := Cofix F α → Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    (((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) (α := α))
    (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
⊢ 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:
apply congrArg

Premises used: congrArg
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
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) (α := α))
e_a :
  ∀ (x : Cofix F α),
    Eq (α := Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
      ((((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) (α := α))
        x)
      (Quot.mk (fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) x)
⊢ Eq.{u + 1} (α := Cofix F α → Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    (((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) (α := α))
    (Quot.mk fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))

Tactic:
funext x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x_2 y : Cofix F α
h : x_2 = mk (F := F) (α := α) (y.dest (F := F) (α := α))
x : Cofix F α
e_a :
  mk (F := F) (α := α) ((fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    mk (F := F) (α := α) (x.dest (F := F) (α := α))
⊢ Eq (α := Quot fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α)))
    ((((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) (α := α))
      x)
    (Quot.mk (fun (x y : Cofix F α) ↦ x = mk (F := F) (α := α) (y.dest (F := F) (α := α))) x)

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 x_2 y : Cofix F α
h : x_2 = mk (F := F) (α := α) (y.dest (F := F) (α := α))
x : Cofix F α
⊢ mk (F := F) (α := α) ((fun (i : Cofix F α) ↦ i.dest (F := F) (α := α)) x) =
    mk (F := F) (α := α) (x.dest (F := F) (α := α))

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 : F (α ::: Cofix F α)
⊢ Eq.{u + 1} (α := Cofix F α → Cofix F α) (mk (F := F) (α := α) ∘ dest (F := F) (α := α)) _root_.id

Tactic:
have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : Cofix F α
h : x.dest (F := F) (α := α) = y.dest (F := F) (α := α)
rw : mk (F := F) (α := α) (x.dest (F := F) (α := α)) = y
rw₁ : mk (F := F) (α := α) (y.dest (F := F) (α := α)) = y
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← Cofix.mk_dest x, h, Cofix.mk_dest]

Premises used: MvQPF.Cofix.mk_dest
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : F (α ::: Cofix F α)
h : mk (F := F) (α := α) x = mk (F := F) (α := α) y
rw : (mk (F := F) (α := α) x).dest (F := F) (α := α) = y
rw₁ : (mk (F := F) (α := α) y).dest (F := F) (α := α) = y
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← Cofix.dest_mk x, h, Cofix.dest_mk]

Premises used: MvQPF.Cofix.dest_mk
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
rw :
  ∃ (u : F' (Subtype_ (α := β ⊗ β) R)),
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
          (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
            (subtypeVal (α := β ⊗ β) R))
          u =
        MvFunctor.map (F := F') (α := α) (β := β) f x ∧
      MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
          (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
            (subtypeVal (α := β ⊗ β) R))
          u =
        MvFunctor.map (F := F') (α := α) (β := β) g x
⊢ LiftR' (α := β) (F := F') R (MvFunctor.map (F := F') (α := α) (β := β) f x)
    (MvFunctor.map (F := F') (α := α) (β := β) g x)

Tactic:
rw [LiftR_def]

Premises used: MvFunctor.LiftR_def
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
exists :
  MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) g x
⊢ ∃ (u : F' (Subtype_ (α := β ⊗ β) R)),
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
          (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
            (subtypeVal (α := β ⊗ β) R))
          u =
        MvFunctor.map (F := F') (α := α) (β := β) f x ∧
      MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
          (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
            (subtypeVal (α := β ⊗ β) R))
          u =
        MvFunctor.map (F := F') (α := α) (β := β) g x

Tactic:
exists h <$$> x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
rw :
  MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) g x
⊢ MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.fst (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) g x

Tactic:
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, fst_prod_mk, comp_assoc, fst_diag]

Premises used: TypeVec.fst_prod_mk, TypeVec.comp_assoc, TypeVec.fst_diag, MvFunctor.map_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
rw :
  MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) g (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) g x
⊢ MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := Subtype_ (α := β ⊗ β) R) (β := β)
        (TypeVec.comp (α := Subtype_ (α := β ⊗ β) R) (β := β ⊗ β) (γ := β) (prod.snd (α := β) (β := β))
          (subtypeVal (α := β ⊗ β) R))
        (MvFunctor.map (F := F') (α := α) (β := Subtype_ (α := β ⊗ β) R) h x) =
      MvFunctor.map (F := F') (α := α) (β := β) g x

Tactic:
rw [MvFunctor.map_map, comp_assoc, hh, ← comp_assoc, snd_prod_mk, comp_assoc, snd_diag]

Premises used: TypeVec.snd_diag, TypeVec.comp_assoc, TypeVec.snd_prod_mk, MvFunctor.map_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
dsimp :
  MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x
⊢ MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) f (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) (TypeVec.comp (α := α) (β := α) (γ := β) g (TypeVec.id (α := α))) x =
      MvFunctor.map (F := F') (α := α) (β := β) g x

Tactic:
dsimp [LiftR']

Premises used: MvFunctor.LiftR'
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
left : MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x
right : MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x
⊢ MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x ∧
    MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (F := F') (α := α) (β := β) g x

Tactic:
constructor
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
⊢ MvFunctor.map (F := F') (α := α) (β := β) f x = MvFunctor.map (F := F') (α := α) (β := β) f x

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α β : TypeVec.{u_1} n
F' : TypeVec.{u_1} n → Type u
inst : MvFunctor F'
inst_1 : LawfulMvFunctor F'
R : β ⊗ β ⟹ «repeat» n Prop
x : F' α
f g : α ⟹ β
h : α ⟹ Subtype_ (α := β ⊗ β) R
hh :
  TypeVec.comp (α := α) (β := Subtype_ (α := β ⊗ β) R) (γ := β ⊗ β) (subtypeVal (α := β ⊗ β) R) h =
    TypeVec.comp (α := α) (β := α ⊗ α) (γ := β ⊗ β) (prod.map (α := α) (α' := α) (β := β) (β' := β) f g)
      (prod.diag (α := α))
⊢ MvFunctor.map (F := F') (α := α) (β := β) g x = MvFunctor.map (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
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₀ :
  Eq.{u + 1} (α := (α ::: ι).drop ⟹ (α ::: ι' ⊗ α ::: ι').drop)
    (fun (i : Fin2 n) (x : (α ::: ι).drop i) ↦
      subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x))
    (prod.diag (α := (α ::: ι).drop))
⊢ TypeVec.comp (α := (α ::: ι).drop) (β := (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop) (γ :=
      (α ::: ι' ⊗ α ::: ι').drop) (subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq)
      (TypeVec.comp (α := (α ::: ι).drop) (β :=
        TypeVec.drop fun (i : Fin2 (n + 1)) ↦ { x : (α ::: ι' ⊗ α ::: ι') i // ofRepeat (α.RelLast' R i x) }) (γ :=
        (Subtype_ (α := α ::: ι' ⊗ α ::: ι') (α.RelLast' R)).drop)
        (toSubtype (α := fun (i : Fin2 n) ↦ (α ::: ι' ⊗ α ::: ι') i.fs) fun (i : Fin2 n) ↦ α.RelLast' R i.fs)
        (TypeVec.comp (α := (α ::: ι).drop) (β :=
          (Subtype_ (α := α ⊗ α) α.repeatEq ::: { x : ι' × ι' // uncurry R x }).drop) (γ :=
          TypeVec.drop
            ((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) }))
          (dropFun (α := 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)
          (diagSub (α := α)))) =
    prod.diag (α := (α ::: ι).drop)

Tactic:
erw [toSubtype_of_subtype_assoc, TypeVec.id_comp]

Premises used: TypeVec.toSubtype_of_subtype_assoc, TypeVec.id_comp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
h₀ :
  ∀ (i : Fin2 n) (x : (α ::: ι).drop i),
    subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x) =
      prod.diag (α := (α ::: ι).drop) i x
⊢ Eq.{u + 1} (α := (α ::: ι).drop ⟹ (α ::: ι' ⊗ α ::: ι').drop)
    (fun (i : Fin2 n) (x : (α ::: ι).drop i) ↦
      subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x))
    (prod.diag (α := (α ::: ι).drop))

Tactic:
ext (i x) : 2
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
ι ι' : Type u
n_1 : ℕ
α : TypeVec.{u} (n_1 + 1)
x : (α ::: ι).drop Fin2.fz
⊢ subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq Fin2.fz (diagSub (α := α) Fin2.fz x) =
    prod.diag (α := (α ::: ι).drop) Fin2.fz x

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
ι ι' : Type u
n_1 : ℕ
a : Fin2 n_1
ih :
  ∀ {α : TypeVec.{u} n_1} (x : (α ::: ι).drop a),
    subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq a (diagSub (α := α) a x) =
      prod.diag (α := (α ::: ι).drop) a x
α : TypeVec.{u} (n_1 + 1)
x : (α ::: ι).drop a.fs
⊢ subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq a.fs (diagSub (α := α) a.fs x) =
    prod.diag (α := (α ::: ι).drop) a.fs x

Tactic:
apply ih
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix
Goal:
n : ℕ
α : TypeVec.{u} n
ι ι' : Type u
i : Fin2 n
x : (α ::: ι).drop i
h₀ :
  ∀ {n : ℕ} {α : TypeVec.{u} (n + 1)} (x : (α ::: ι).drop Fin2.fz),
    subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq Fin2.fz (diagSub (α := α) Fin2.fz x) =
      prod.diag (α := (α ::: ι).drop) Fin2.fz x
h₁ :
  ∀ {n : ℕ} (a : Fin2 n)
    (ih :
      ∀ {α : TypeVec.{u} n} (x : (α ::: ι).drop a),
        subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq a (diagSub (α := α) a x) =
          prod.diag (α := (α ::: ι).drop) a x)
    {α : TypeVec.{u} (n + 1)} (x : (α ::: ι).drop a.fs),
    subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq a.fs (diagSub (α := α) a.fs x) =
      prod.diag (α := (α ::: ι).drop) a.fs x
⊢ subtypeVal (α := (α ::: ι' ⊗ α ::: ι').drop) α.repeatEq i (diagSub (α := α) i x) = prod.diag (α := (α ::: ι).drop) i x

Tactic:
induction i with
      | fz => rfl
      | fs _ ih =>
        apply ih