awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ mk (F := F) (α := α)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧

Tactic:
have : Fix.mk (abs ⟨a, q.P.appendContents f' fun x => ⟦f x⟧⟩) = ⟦wrepr (q.P.wMk a f' f)⟧ := by
    apply Quot.sound; apply wEquiv.abs'
    rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
    conv =>
      rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
    congr 2; rw [MvPFunctor.appendContents, MvPFunctor.appendContents]
    rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
    rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this :
  mk (F := F) (α := α)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧
rw : Eq (α := Fix F α) ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧ ⟦(P F).wMk (α := α) a f' f⟧
⊢ mk (F := F) (α := α)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    ⟦(P F).wMk (α := α) a f' f⟧

Tactic:
rw [this]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this :
  mk (F := F) (α := α)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧
a₁ :
  (wSetoid α : (P F).W α → (P F).W α → Prop) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))
    ((P F).wMk (α := α) a f' f)
⊢ Eq (α := Fix F α) ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧ ⟦(P F).wMk (α := α) a f' f⟧

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
this :
  mk (F := F) (α := α)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧
⊢ (wSetoid α : (P F).W α → (P F).W α → Prop) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))
    ((P F).wMk (α := α) a f' f)

Tactic:
apply wrepr_equiv

Premises used: MvQPF.wrepr_equiv
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (Fix.mk (F := F) (α := α) x) = g₂ (Fix.mk (F := F) (α := α) x)
mk :
  ∀ (a : (P F).W α),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) a)
⊢ ∀ (x : Fix F α), g₁ x = g₂ x

Tactic:
apply Quot.ind

Premises used: Quot.ind
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (Fix.mk (F := F) (α := α) x) = g₂ (Fix.mk (F := F) (α := α) x)
x : (P F).W α
mk :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
    (∀ (i : (P F).last.B a),
        g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
          g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))) →
      g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f)) =
        g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f))
⊢ g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) x) =
    g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) x)

Tactic:
induction x using q.P.wInd
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
change : g₁ ⟦(P F).wMk (α := α) a f' f⟧ = g₂ ⟦(P F).wMk (α := α) a f' f⟧
⊢ g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f)) =
    g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) ((P F).wMk (α := α) a f' f))

Tactic:
change g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧

Premises used: Quotient.mk, MvQPF.P, MvPFunctor.wMk
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
rw :
  g₁
      (mk (F := F) (α := α)
        (abs (F := F) (α := α ::: Fix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
            ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)))) =
    g₂
      (mk (F := F) (α := α)
        (abs (F := F) (α := α ::: Fix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
            ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
⊢ g₁ ⟦(P F).wMk (α := α) a f' f⟧ = g₂ ⟦(P F).wMk (α := α) a f' f⟧

Tactic:
rw [← Fix.ind_aux a f' f]

Premises used: MvQPF.Fix.ind_aux
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
a₁ :
  Eq (α := F (α ::: β))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
⊢ g₁
      (mk (F := F) (α := α)
        (abs (F := F) (α := α ::: Fix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
            ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)))) =
    g₂
      (mk (F := F) (α := α)
        (abs (F := F) (α := α ::: Fix F α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
            ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))

Tactic:
apply h
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
a₁ :
  Eq (α := F (α ::: β))
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
⊢ Eq (α := F (α ::: β))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
      (abs (F := F) (α := α ::: Fix F α)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))

Tactic:
rw [← abs_map, ← abs_map, MvPFunctor.map_eq, MvPFunctor.map_eq]

Premises used: MvPFunctor.map_eq, MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
a₁ :
  comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)
⊢ Eq (α := F (α ::: β))
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))

Tactic:
congr 2
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
a₁ :
  splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
⊢ comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂)
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧)

Tactic:
rw [MvPFunctor.appendContents, appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]

Premises used: TypeVec.splitFun_comp, MvPFunctor.appendContents, TypeVec.appendFun
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
h₁ : ∀ (x : (P F).last.B a), (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x = (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x
⊢ Eq (α := (P F).last.B a → β) (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)

Tactic:
ext x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
x : (P F).last.B a
⊢ (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x = (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x

Tactic:
ih x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
x : (P F).last.B a
⊢ (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x = (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) x

Tactic:
exact ih x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
⊢ Eq (α := (P F).last.B a → β) (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)

Tactic:
have : (g₁ ∘ fun x => ⟦f x⟧) = g₂ ∘ fun x => ⟦f x⟧ := by
      ext x
      exact ih x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g₁ g₂ : Fix F α → β
h :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₁)
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) g₂) x →
      g₁ (mk (F := F) (α := α) x) = g₂ (mk (F := F) (α := α) x)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
ih :
  ∀ (i : (P F).last.B a),
    g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i)) =
      g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) (f i))
this : Eq (α := (P F).last.B a → β) (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
a₁ a₂ :
  splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)
⊢ splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₁ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: β)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
      (g₂ ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧)

Tactic:
rw [this]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
h₁ : ∀ (x : Fix F α), rec (F := F) (α := α) g x = h x
⊢ rec (F := F) (α := α) g = h

Tactic:
ext x
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
x : Fix F α
h₁ :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x →
      rec (F := F) (α := α) g (mk (F := F) (α := α) x) = h (mk (F := F) (α := α) x)
⊢ rec (F := F) (α := α) g x = h x

Tactic:
apply Fix.ind_rec

Premises used: MvQPF.Fix.ind_rec
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp :
  ∀ (x : F (α ::: Fix F α)),
    h (mk (F := F) (α := α) x) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x)
x_1 : Fix F α
x : F (α ::: Fix F α)
hyp' :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h) x
h₁ :
  rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) h)
        x)
h₂ :
  rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
h₃ h₄ :
  g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
⊢ rec (F := F) (α := α) g (mk (F := F) (α := α) x) = h (mk (F := F) (α := α) x)

Tactic:
rw [hyp, ← hyp', Fix.rec_eq]

Premises used: MvQPF.Fix.rec_eq