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
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)))
have 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)
Tactic: refine 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
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)
have 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)
Tactic: rw [Cofix.corec', Cofix.dest_corec]
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
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)
have 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)
Tactic: dsimp
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
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)))
      (g x) =
    MvFunctor.map (F := F) (α := α ::: (Cofix F α ⊕ β)) (β := α ::: Cofix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sum.elim _root_.id (corec' (F := F) (α := α) g))) (g x)
have 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)
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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
⊢ 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)
have 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)
Tactic: ext (i | i)
-- 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
β : 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)
⊢ 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)
have 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)
Tactic: ext (i | i)
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
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)
have 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)
Tactic: erw [corec_roll]
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x 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)
have 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)
Tactic: erw [corec_roll]
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : 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) ∘
                dest (F := F) (α := α))
              val)
          fun (val : β) ↦ g val))
      (Sum.inl i) =
    Sum.elim _root_.id (corec' (F := F) (α := α) g) (Sum.inl i)
have 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
Tactic: dsimp [Cofix.corec']
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x 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)
have 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))
Tactic: dsimp [Cofix.corec']
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x : β
i : 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.inl i) =
    i
have 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) (α := α))
Tactic: mv_bisim i 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
⊢ 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))
have 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
Tactic: congr 1 with y
-- 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
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
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
have 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
Tactic: erw [appendFun_id_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
β : 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)
⊢ (corec₁ (F := F) (α := α) (@g) x).dest (F := F) (α := α) = g _root_.id (corec₁ (F := F) (α := α) @g) x
have 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
Tactic: rw [Cofix.corec₁, Cofix.dest_corec', ← h]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Comp (goal)
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 β_1 : TypeVec.{u} m
f_1 : α_1 ⟹ β_1
p : (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u) α_1
⊢ Eq (α := Comp F G β_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))
      (MvFunctor.map (F := (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u)) (α := α_1) (β :=
        β_1) f_1 p))
    (MvFunctor.map (F := Comp F G) (α := α_1) (β := β_1) f_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))
        p))
have simp : Eq (α := Comp F G β_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)
          (MvFunctor.map (F := (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u)) (α := α_1)
            (β := β_1) f_1 p)))))
  (MvFunctor.map (F := Comp F G) (α := α_1) (β := β_1) f_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) p)))))
Tactic: simp only [(· ∘ ·)]