awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
i : (P.B ax).last
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx Fin2.fz i =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy Fin2.fz i
⊢ R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
have h₂ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)
Tactic: simp only [TypeVec.comp, appendFun, splitFun] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
i : (P.B ax).last
h₁ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)
⊢ R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
have h₂ : Relation.EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
Tactic: replace h₁ := Quot.eqvGen_exact h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
i : (P.B ax).last
h₁ : Relation.EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
have h₂ : R (fx Fin2.fz i) (fy Fin2.fz i)
Tactic: rw [h₀.eqvGen_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
⊢ x = y
have refine_3 : ∀ (this : ∀ (x y : P.M α) (r : Relation.EqvGen R x y), x = y), x = y
Tactic: have := M.bisim₀ P (Relation.EqvGen R) ?_ ?_
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
refine_3 : ∀ (this : ∀ (x y : P.M α) (r : Relation.EqvGen R x y), x = y), x = y
⊢ x = y
have refine_1 : Equivalence (Relation.EqvGen R)
Tactic: have := M.bisim₀ P (Relation.EqvGen R) ?_ ?_
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
r : R x y
refine_3 : ∀ (this : ∀ (x y : P.M α) (r : Relation.EqvGen R x y), x = y), x = y
refine_1 : Equivalence (Relation.EqvGen R)
⊢ x = y
have refine_2 : ∀ (x y : P.M α),
  Relation.EqvGen R x y →
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
        α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
        α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y)
Tactic: have := M.bisim₀ P (Relation.EqvGen R) ?_ ?_
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (hypothesis)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
Hr : Relation.EqvGen R x y
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y)
have this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
Tactic: have : ∀ x y, R x y → Relation.EqvGen R x y := @Relation.EqvGen.rel _ R
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
Hr : Relation.EqvGen R x y
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y)
have refine_2 : ∀ (x y : P.M α),
  R x y →
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
        α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
        α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y)
Tactic: induction Hr
Cleared hypotheses: Hr
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
Hr : Relation.EqvGen R x y
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
refine_2 :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
          α ::: Quot (Relation.EqvGen R))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
          α ::: Quot (Relation.EqvGen R))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R))) (dest P (α := α) y)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) y)
have refine_2₁ : ∀ (x : P.M α),
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R)) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk (Relation.EqvGen R)))
      (dest P (α := α) x)
Tactic: induction Hr
Cleared hypotheses: Hr
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x_1 y_1 : P.M α
h_1 : R x_1 y_1
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R))
      (dest P (α := α) y_1)
have refine_2 : MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot (Relation.EqvGen R))
    (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
    (dest P (α := α) x_1) =
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
    α ::: Quot (Relation.EqvGen R))
    (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
    (dest P (α := α) y_1)
Tactic: rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h :
  ∀ (x y : P.M α),
    R x y →
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)
x y : P.M α
this : ∀ (x y : P.M α), R x y → Relation.EqvGen R x y
x_1 y_1 : P.M α
h_1 : R x_1 y_1
refine_2 :
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
      (dest P (α := α) y_1)
⊢ MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R))
      (dest P (α := α) x_1) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
      α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this ∘ Quot.mk R))
      (dest P (α := α) y_1)
have refine_2₁ : MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Quot R) (β := α ::: Quot (Relation.EqvGen R))
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) x_1)) =
  MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β :=
    α ::: Quot (Relation.EqvGen R))
    (TypeVec.comp (α := α ::: P.M α) (β := α ::: Quot R) (γ := α ::: Quot (Relation.EqvGen R))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.factor R (Relation.EqvGen R) this))
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)))
    (dest P (α := α) y_1)
Tactic: rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
x : P.M α
⊢ dest P (α := β) (MvFunctor.map (F := P.M) (α := α) (β := β) g x) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) x)
have obtain : ∀ (a : P.mp.A) (f : P.mp.B a ⟹ α),
  dest P (α := β) (MvFunctor.map (F := P.M) (α := α) (β := β) g (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
Tactic: obtain ⟨a, f⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
have rhs : MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
  (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
  (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
    (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
    (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
have rw : Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
  ((PFunctor.M.dest
        (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
    (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
  (splitFun (α :=
    P.B
      ((PFunctor.M.dest
            (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
              (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
        (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
    (α' := β ::: P.M β)
    (TypeVec.comp (α :=
      (P.B
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
      (β := α) (γ := (β ::: P.M β).drop) g
      (pathDestLeft P (α := (α ::: P.M α).drop) sorry
        (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
    ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
      fun
        (x :
          (P.B
              ((PFunctor.M.dest
                    (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
      Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
        ((PFunctor.M.dest
              (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
          (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
        (pathDestRight P (α := α) sorry
          (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f)) x)))
Tactic: rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Multivariate.M (goal)
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.mp.A
f : P.mp.B a ⟹ α
| dest P (α := β)
      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ β) a (TypeVec.comp (α := P.mp.B a) (β := α) (γ := β) g f)) =
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := β ::: P.M β)
      (appendFun (α := α) (α' := β) g fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x)
      (dest P (α := α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))
have rw : Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ β ::: P.M β)
  ((PFunctor.M.dest
        (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
    (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))
  (splitFun (α :=
    P.B
      ((PFunctor.M.dest
            (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
              (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
        (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M)))
    (α' := β ::: P.M β)
    (TypeVec.comp (α :=
      (P.B
          ((PFunctor.M.dest
                (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                  (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
            (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).drop)
      (β := α) (γ := (β ::: P.M β).drop) g
      (pathDestLeft P (α := (α ::: P.M α).drop) sorry
        (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))))
    ((fun (x : P.M α) ↦ MvFunctor.map (F := P.M) (α := α) (β := β) g x) ∘
      fun
        (x :
          (P.B
              ((PFunctor.M.dest
                    (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                      (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).fst
                (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M))).last) ↦
      Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
        ((PFunctor.M.dest
              (Sigma.fst (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α)
                (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f))).snd
          (β := fun (a : P.last.A) ↦ P.last.B a → P.last.M) x)
        (pathDestRight P (α := α) sorry
          (Sigma.snd (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) (Sigma.mk (β := fun (a : P.mp.A) ↦ P.mp.B a ⟹ α) a f)) x)))
Tactic: rhs
    rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]