awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
a : P.A
f : P.last.B a → P.last.M
h' :
  Eq.{u + 1} (α := (↑P.last : (α : Type u) → Type u) P.last.M)
    (PFunctor.map.{u, u, v, u} P.last (α := β)
      (PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b))
      (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)))
    (Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f)
j : P.last.B a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
refl :
  ∀ (j : P.last.B (g₀ b)) (h₀ : g₀ b = g₀ b)
    (c :
      Path P
        (((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j)
        i),
    ((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j =
      corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))
⊢ f j = corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
cases h'
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x_1 : P.last.M
b : β
x : P.last.M
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : P.last.B (g₀ b)
h₀ : g₀ b = g₀ b
c :
  Path P (((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j)
    i
⊢ ((PFunctor.M.corec fun (b : β) ↦ Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → β) (g₀ b) (g₂ b)) ∘ g₂ b) j =
    corecShape P g₀ g₂ (g₂ b (P.castLastB h₀ j))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁ f₁
a₂ : P.A
f₂ : P.last.B a₂ → P.last.M
h₂ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₂ f₂
f' : Path P x ⟹ α
refl :
  ∀ (h₂ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁ f₁),
    dest' P (α := α) h₁ f' = dest' P (α := α) h₂ f'
⊢ dest' P (α := α) h₁ f' = dest' P (α := α) h₂ f'

Tactic:
cases h₁.symm.trans h₂

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁ f₁
f' : Path P x ⟹ α
h₂ : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁ f₁
⊢ dest' P (α := α) h₁ f' = dest' P (α := α) h₂ f'

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a : P.A
f : P.last.B a → P.last.M
h : x.dest = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a f
f' : Path P x ⟹ α
⊢ dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) x f') = dest' P (α := α) h f'

Tactic:
M.dest'_eq_dest' _ _ _ _

Premises used: MvPFunctor.M.dest'_eq_dest', MvPFunctor.M.dest
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type v
g₀ : β → P.A
g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α
g₂ : (b : β) → P.last.B (g₀ b) → β
x : β
⊢ dest P (α := α) (corec' P (α := α) g₀ g₁ g₂ x) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) (g₀ x)
      (splitFun (α := P.B (g₀ x)) (α' := α ::: P.M α) (g₁ x) (corec' P (α := α) g₀ g₁ g₂ ∘ g₂ x))

Tactic:
rfl

Premises used: MvPFunctor.M.corecShape, PFunctor.M.corec, cast, PFunctor.M.children, MvPFunctor.M.dest, MvPFunctor.castDropB, MvPFunctor.castLastB, MvPFunctor.M.pathDestLeft, PFunctor.Approx.sCorec, PFunctor.M.head, MvPFunctor.M.dest', MvPFunctor.M.pathDestRight, MvPFunctor.M.corecContents, PFunctor.Approx.children', rfl, MvPFunctor.M.corec', PFunctor.Approx.head'
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
trans :
  dest P (α := α) (corec P (α := α) g x) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))))
trans₁ :
  Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)
trans₂ : (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α)
⊢ dest P (α := α) (corec P (α := α) g x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) (g x)

Tactic:
trans
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
⊢ dest P (α := α) (corec P (α := α) g x) =
    Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
      (splitFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (α' := α ::: P.M α)
        (dropFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
          ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B ((g x).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g x).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))))

Tactic:
apply M.dest_corec'

Premises used: MvPFunctor.M.dest_corec'
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
rw :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B a) (β := α ::: β) f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f))
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B a) (β := α ::: β) f)))
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: β) (β := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β) a f))

Tactic:
rw [MvPFunctor.map_eq]

Premises used: MvPFunctor.map_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
e_snd :
  splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B a) (β := α ::: β) f) =
    TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
        ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
            (fun (b : β) ↦
              dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
                ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
            fun (b : β) ↦
            lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
          lastFun (α := P.B a) (β := α ::: β) f)))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a
      (TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f))

Tactic:
congr
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
rw :
  splitFun (α := P.B a) (α' := α ::: P.M α)
    (TypeVec.comp (α := (P.B a).drop) (β := α) (γ := (α ::: P.M α).drop) (TypeVec.id (α := α))
      (dropFun (α := P.B a) (β := α ::: β) f))
    (corec P (α := α) g ∘ lastFun (α := P.B a) (β := α ::: β) f)
| TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f

Tactic:
rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]

Premises used: TypeVec.split_dropFun_lastFun, TypeVec.appendFun_comp_splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
e_snd :
  splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B a) (β := α ::: β) f) =
    splitFun (α := P.B a) (α' := α ::: P.M α)
      (TypeVec.comp (α := (P.B a).drop) (β := α) (γ := (α ::: P.M α).drop) (TypeVec.id (α := α))
        (dropFun (α := P.B a) (β := α ::: β) f))
      (corec P (α := α) g ∘ lastFun (α := P.B a) (β := α ::: β) f)
⊢ splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B a) (β := α ::: β) f) =
    TypeVec.comp (α := P.B a) (β := α ::: β) (γ := α ::: P.M α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (corec P (α := α) g)) f

Tactic:
conv_rhs => rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]

Premises used: TypeVec.split_dropFun_lastFun, TypeVec.appendFun_comp_splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: β)
x : β
a : P.A
f : P.B a ⟹ α ::: β
⊢ splitFun (α := P.B a) (α' := α ::: P.M α) (dropFun (α := P.B a) (β := α ::: β) f)
      ((corec' P (α := α) (fun (b : β) ↦ (g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))
          (fun (b : β) ↦
            dropFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
              ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β)))
          fun (b : β) ↦
          lastFun (α := P.B ((g b).fst (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) (β := α ::: β)
            ((g b).snd (β := fun (a : P.A) ↦ P.B a ⟹ α ::: β))) ∘
        lastFun (α := P.B a) (β := α ::: β) f) =
    splitFun (α := P.B a) (α' := α ::: P.M α)
      (TypeVec.comp (α := (P.B a).drop) (β := α) (γ := (α ::: P.M α).drop) (TypeVec.id (α := α))
        (dropFun (α := P.B a) (β := α ::: β) f))
      (corec P (α := α) g ∘ lastFun (α := P.B a) (β := α ::: β) f)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' (splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁'))
generalize :
  ∀ (ff : P.B a' ⟹ α ::: P.M α) (ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff)
    (e₁ :
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff)),
    ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
      PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
      f' = pathDestLeft P (α := α) e₁' f₁ ∧
        f₁' = fun (x : P.last.B a') ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)

Tactic:
generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁

Premises used: TypeVec.splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff)
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
rcases :
  ∀ (a₁' : P.last.A) (g₁' : P.last.B a₁' → P.last.M)
    (e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁' g₁'),
    ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
      PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
      f' = pathDestLeft P (α := α) e₁' f₁ ∧
        f₁' = fun (x : P.last.B a') ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)

Tactic:
rcases e₁' : he₁' with ⟨a₁', g₁'⟩
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff
e₁ :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a₁ f₁))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff)
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁' g₁'
⊢ dest' P (α := α) e₁' f₁ = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff

Tactic:
rw [M.dest_eq_dest' _ e₁'] at e₁

Premises used: MvPFunctor.M.dest_eq_dest'
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' = ff
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a₁' g₁'
e₁ : dest' P (α := α) e₁' f₁ = Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a' ff
refl :
  ∀ (g₁' : P.last.B a' → P.last.M) (e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁')
    (ef :
      splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' =
        splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := (α ::: P.M α).drop) e₁' f₁)
          fun (x : (P.B a').last) ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)),
    ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
      PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
      f' = pathDestLeft P (α := α) e₁' f₁ ∧
        f₁' = fun (x : P.last.B a') ↦
          Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)

Tactic:
cases e₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
g₁' : P.last.B a' → P.last.M
e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'
ef :
  splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' =
    splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := (α ::: P.M α).drop) e₁' f₁)
      fun (x : (P.B a').last) ↦
      Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)

Tactic:
⟨_, e₁', splitFun_inj ef⟩

Premises used: Exists.intro, TypeVec.splitFun_inj
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
he₁' : (↑P.last : (α : Type u) → Type u) P.last.M := PFunctor.M.dest a₁
g₁' : P.last.B a' → P.last.M
e₁' : he₁' = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'
ef :
  splitFun (α := P.B a') (α' := α ::: P.M α) f' f₁' =
    splitFun (α := P.B a') (α' := α ::: P.M α) (pathDestLeft P (α := (α ::: P.M α).drop) e₁' f₁)
      fun (x : (P.B a').last) ↦
      Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)
⊢ ∃ (g₁' : P.last.B a' → P.last.M) (e₁' :
    PFunctor.M.dest a₁ = Sigma.mk (β := fun (x : P.last.A) ↦ P.last.B x → P.last.M) a' g₁'),
    f' = pathDestLeft P (α := α) e₁' f₁ ∧
      f₁' = fun (x : P.last.B a') ↦
        Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (g₁' x) (pathDestRight P (α := α) e₁' f₁ x)

Tactic:
exact ⟨_, e₁', splitFun_inj ef⟩