awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀ : Equivalence R
x y : P.M α
⊢ ∀
    (h :
      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)),
    ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
      (P.B a).last → (α ::: P.M α).last),
      dest P (α := α) x =
          Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁) ∧
        dest P (α := α) y =
            Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
          ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have rcases : ∀ (ax : P.A) (fx : P.B ax ⟹ α ::: P.M α)
  (h :
    MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx) =
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)),
  ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      dest P (α := α) y =
          Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Tactic: rcases M.dest P x with ⟨ax, fx⟩
-- 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₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
⊢ ∀
    (h :
      MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx) =
        MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) (dest P (α := α) y)),
    ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
      (P.B a).last → (α ::: P.M α).last),
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
        dest P (α := α) y =
            Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂) ∧
          ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have rcases : ∀ (ay : P.A) (fy : P.B ay ⟹ α ::: P.M α)
  (h :
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: Quot R))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx))
      (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy))),
  ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Tactic: rcases M.dest P y with ⟨ay, fy⟩
-- 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 : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: Quot R))
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx))
    (MvFunctor.map (F := (↑P : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: P.M α) (β := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy))
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have h₁ : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: Quot R))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: Quot R) ax
    (TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx))
  (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: Quot R) ay
    (TypeVec.comp (α := P.B ay) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy))
Tactic: rw [map_eq, map_eq] 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 : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: Quot R))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: Quot R) ax
      (TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: Quot R) ay
      (TypeVec.comp (α := P.B ay) (β := α ::: P.M α) (γ := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy))
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have h₁ : ax = ay
Tactic: injection h with h₀ 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 : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h :
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: Quot R))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: Quot R) ax
      (TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: Quot R) ay
      (TypeVec.comp (α := P.B ay) (β := α ::: P.M α) (γ := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy))
h₁ : ax = ay
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have h₂ : TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx ≍
  TypeVec.comp (α := P.B ay) (β := α ::: P.M α) (γ := α ::: Quot R)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
Tactic: injection h with h₀ 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₀_1 : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h₀ : ax = ay
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx ≍
    TypeVec.comp (α := P.B ay) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ay fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have subst : ∀ (fy : P.B ax ⟹ α ::: P.M α)
  (h₁ :
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx ≍
      TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy),
  ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Tactic: subst ay
Cleared hypotheses: ay, fy, h₀, 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 α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx ≍
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have h₂ : TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
Tactic: simp only [heq_eq_eq] 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 α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
⊢ dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
have h₂ : dropFun (α := P.B ax) (β := α ::: Quot R)
    (TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx) =
  dropFun (α := P.B ax) (β := α ::: Quot R)
    (TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy)
Tactic: replace h₁ := congr_arg dropFun 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 α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
Tactic: have Hdrop : dropFun fx = dropFun fy := by
    replace h₁ := congr_arg dropFun h₁
    simpa using 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₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
⊢ ∃ (a : P.A) (f : (P.B a).drop ⟹ (α ::: P.M α).drop) (f₁ : (P.B a).last → (α ::: P.M α).last) (f₂ :
    (P.B a).last → (α ::: P.M α).last),
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₁)) ∧
      Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
          (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) a (splitFun (α := P.B a) (α' := α ::: P.M α) f f₂)) ∧
        ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
have exists : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax
      (splitFun (α := P.B ax) (α' := α ::: P.M α) (dropFun (α := P.B ax) (β := α ::: P.M α) fx)
        (lastFun (α := P.B ax) (β := α ::: P.M α) fx))) ∧
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax
        (splitFun (α := P.B ax) (α' := α ::: P.M α) (dropFun (α := P.B ax) (β := α ::: P.M α) fx)
          (lastFun (α := P.B ax) (β := α ::: P.M α) fy))) ∧
    ∀ (i : (P.B ax).last),
      R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
Tactic: exists ax, dropFun fx, lastFun fx, lastFun fy
-- 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₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax
        (splitFun (α := P.B ax) (α' := α ::: P.M α) (dropFun (α := P.B ax) (β := α ::: P.M α) fx)
          (lastFun (α := P.B ax) (β := α ::: P.M α) fx))) ∧
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax
          (splitFun (α := P.B ax) (α' := α ::: P.M α) (dropFun (α := P.B ax) (β := α ::: P.M α) fx)
            (lastFun (α := P.B ax) (β := α ::: P.M α) fy))) ∧
      ∀ (i : (P.B ax).last),
        R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
have rw : Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
    (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx) ∧
  Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy) ∧
    ∀ (i : (P.B ax).last),
      R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
Tactic: rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]
-- 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₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
⊢ Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx)
      (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fx) ∧
    Eq (α := (↑P : (α : TypeVec.{u} (n + 1)) → Type u) (α ::: P.M α))
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy)
        (Sigma.mk (β := fun (a : P.A) ↦ P.B a ⟹ α ::: P.M α) ax fy) ∧
      ∀ (i : (P.B ax).last),
        R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
have simp : ∀ (i : (P.B ax).last), R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
Tactic: simp only [true_and]
-- 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₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ :
  TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fx =
    TypeVec.comp (α := P.B ax) (β := α ::: P.M α) (γ := α ::: Quot R)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Quot.mk R)) fy
Hdrop : dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy
i : (P.B ax).last
⊢ R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
have replace : ∀
  (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)
Tactic: replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i
Cleared hypotheses: h₁