awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Multivariate.M
Goal:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
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)
⊢ ∀
    (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)

Tactic:
rcases M.dest P x with ⟨ax, fx⟩

Premises used: MvPFunctor.M.dest
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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 α
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)
⊢ ∀
    (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 y with ⟨ay, fy⟩

Premises used: MvPFunctor.M.dest
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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))
⊢ 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

Premises used: MvPFunctor.map_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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))
⊢ ax = ay

Tactic:
injection h with h₀ h₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
⊢ 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₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
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)
⊢ ∃ (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:
subst ay
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
⊢ 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₁

Premises used: heq_eq_eq
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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) (β := α ::: 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₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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₁ :
  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)
⊢ dropFun (α := P.B ax) (β := α ::: P.M α) fx = dropFun (α := P.B ax) (β := α ::: P.M α) fy

Tactic:
simpa using h₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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

Tactic:
have Hdrop : dropFun fx = dropFun fy := by
    replace h₁ := congr_arg dropFun h₁
    simpa using h₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
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)
⊢ ∃ (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:
exists ax, dropFun fx, lastFun fx, lastFun fy

Premises used: TypeVec.lastFun, TypeVec.dropFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
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)
⊢ 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:
rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]

Premises used: TypeVec.split_dropFun_lastFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
simp :
  ∀ (i : (P.B ax).last),
    R (lastFun (α := P.B ax) (β := α ::: P.M α) fx i) (lastFun (α := P.B ax) (β := α ::: P.M α) fy i)
⊢ 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:
simp only [true_and]

Premises used: true_and
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
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)
⊢ 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
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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
⊢ Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)

Tactic:
simp only [TypeVec.comp, appendFun, splitFun] at h₁

Premises used: TypeVec.comp, TypeVec.appendFun, TypeVec.splitFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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)
⊢ Relation.EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)

Tactic:
replace h₁ := Quot.eqvGen_exact h₁
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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 (fx Fin2.fz i) (fy Fin2.fz i)

Tactic:
rw [h₀.eqvGen_iff] at h₁

Premises used: Equivalence.eqvGen_iff
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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₁ : 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)

Tactic:
h₁

Premises used: TypeVec.lastFun
-- Module: Mathlib.Data.PFunctor.Multivariate.M
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₁ : 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)

Tactic:
exact h₁