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
g : α ⟹ β
x_1 y_1 x y z : (P F).W α
h : WEquiv (F := F) (α := α) x y
h_1 : WEquiv (F := F) (α := α) y z
ih₁ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
ih₂ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)
trans : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
trans₁ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)
trans₂ : (P F).W β
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g z)

Tactic:
apply MvQPF.WEquiv.trans

Premises used: MvQPF.WEquiv.trans
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x_1 y_1 x y z : (P F).W α
h : WEquiv (F := F) (α := α) x y
h_1 : WEquiv (F := F) (α := α) y z
ih₁ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
ih₂ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)

Tactic:
apply ih₁
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x_1 y_1 x y z : (P F).W α
h : WEquiv (F := F) (α := α) x y
h_1 : WEquiv (F := F) (α := α) y z
ih₁ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)
ih₂ : WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y) (map (F := (P F).W) (α := α) (β := β) g z)

Tactic:
apply ih₂
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x y : (P F).W α
h : WEquiv (F := F) (α := α) x y
ind :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
    (h : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x))
    (ih :
      ∀ (x : (P F).last.B a),
        WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g (f₀ x))
          (map (F := (P F).W) (α := α) (β := β) g (f₁ x))),
    WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₀))
      (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a f' f₁))
abs :
  ∀ (a₀ : (P F).A) (f'₀ : (P F).drop.B a₀ ⟹ α) (f₀ : (P F).last.B a₀ → (P F).W α) (a₁ : (P F).A)
    (f'₁ : (P F).drop.B a₁ ⟹ α) (f₁ : (P F).last.B a₁ → (P F).W α)
    (h :
      Eq (α := F (α ::: (P F).W α))
        (MvQPF.abs (F := F) (α := α ::: (P F).W α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₀ ((P F).appendContents (α := α) f'₀ f₀)))
        (MvQPF.abs (F := F) (α := α ::: (P F).W α)
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a₁ ((P F).appendContents (α := α) f'₁ f₁)))),
    WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a₀ f'₀ f₀))
      (map (F := (P F).W) (α := α) (β := β) g ((P F).wMk (α := α) a₁ f'₁ f₁))
trans :
  ∀ (x y z : (P F).W α),
    WEquiv (F := F) (α := α) x y →
      WEquiv (F := F) (α := α) y z →
        ∀
          (ih₁ :
            WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x)
              (map (F := (P F).W) (α := α) (β := β) g y))
          (ih₂ :
            WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g y)
              (map (F := (P F).W) (α := α) (β := β) g z)),
          WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g z)
⊢ WEquiv (F := F) (α := β) (map (F := (P F).W) (α := α) (β := β) g x) (map (F := (P F).W) (α := α) (β := β) g y)

Tactic:
induction h with
  | ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
    rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
    change
      abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
        abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
    rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
  | trans x y z _ _ ih₁ ih₂ =>
    apply MvQPF.WEquiv.trans
    · apply ih₁
    · apply ih₂

Premises used: MvPFunctor.w_map_wMk, MvQPF.WEquiv.abs, MvQPF.WEquiv.ind, MvQPF.WEquiv.trans, MvPFunctor.map_objAppend1, MvQPF.abs_map, MvQPF.P, MvQPF.abs
-- 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 (α ::: β) → β
x : F (α ::: Fix F α)
h : ∀ (x : Fix F α), (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) x = rec (F := F) (α := α) g x
⊢ Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)

Tactic:
apply funext

Premises used: funext
-- 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 (α ::: β) → β
x : F (α ::: Fix F α)
h : ∀ (a : (P F).W α), (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) ⟦a⟧ = rec (F := F) (α := α) g ⟦a⟧
⊢ ∀ (x : Fix F α), (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) x = rec (F := F) (α := α) g x

Tactic:
apply Quotient.ind

Premises used: Quotient.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 : F (α ::: β) → β
x_1 : F (α ::: Fix F α)
x : (P F).W α
h : WEquiv (F := F) (α := α) (fixToW (F := F) (α := α) ⟦x⟧) x
⊢ (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) ⟦x⟧ = rec (F := F) (α := α) g ⟦x⟧

Tactic:
apply recF_eq_of_wEquiv

Premises used: MvQPF.recF_eq_of_wEquiv
-- 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 (α ::: β) → β
x_1 : F (α ::: Fix F α)
x : (P F).W α
⊢ WEquiv (F := F) (α := α) (fixToW (F := F) (α := α) ⟦x⟧) x

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 : F (α ::: β) → β
x : F (α ::: Fix F α)
⊢ Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)

Tactic:
have : recF g ∘ fixToW = Fix.rec g := by
    apply funext
    apply Quotient.ind
    intro x
    apply recF_eq_of_wEquiv
    apply 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 : F (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
lhs : rec (F := F) (α := α) g (mk (F := F) (α := α) x)
| rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)

Tactic:
lhs
-- 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 (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
rw :
  recF (F := F) (α := α) g
    ((P F).wMk' (α := α)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
        (repr (F := F) (α := α ::: Fix F α) x)))
| rec (F := F) (α := α) g (mk (F := F) (α := α) x) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)

Tactic:
lhs
    rw [Fix.rec, Fix.mk]
    dsimp

Premises used: MvQPF.Fix.mk, MvQPF.Fix.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 (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
rcases :
  ∀ (a : (P F).A) (f : (P F).B a ⟹ α ::: Fix F α)
    (h : repr (F := F) (α := α ::: Fix F α) x = Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f),
    recF (F := F) (α := α) g
        ((P F).wMk' (α := α)
          (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β :=
            α ::: (P F).W α) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f))) =
      g
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
⊢ recF (F := F) (α := α) g
      ((P F).wMk' (α := α)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          (repr (F := F) (α := α ::: Fix F α) x))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)

Tactic:
rcases h : repr x with ⟨a, f⟩

Premises used: MvQPF.repr
-- 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 (α ::: β) → β
x : F (α ::: Fix F α)
this : Eq (α := Fix F α → β) (recF (F := F) (α := α) g ∘ fixToW (F := F) (α := α)) (rec (F := F) (α := α) g)
a : (P F).A
f : (P F).B a ⟹ α ::: Fix F α
h : repr (F := F) (α := α ::: Fix F α) x = Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f
rw :
  g
      (abs (F := F) (α := α ::: β)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β :=
            α ::: (P F).W α) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f)))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
⊢ recF (F := F) (α := α) g
      ((P F).wMk' (α := α)
        (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: Fix F α) a f))) =
    g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)

Tactic:
rw [MvPFunctor.map_eq, recF_eq', ← MvPFunctor.map_eq, MvPFunctor.wDest'_wMk']

Premises used: MvPFunctor.wDest'_wMk', MvQPF.recF_eq', MvPFunctor.map_eq
-- 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 α
a₁ :
  (wSetoid α : (P F).W α → (P F).W α → Prop)
    ((P F).wMk' (α := α)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
        (repr (F := F) (α := α ::: Fix 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))
⊢ 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:
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 α
a₁ :
  abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β :=
            α ::: (P F).W α) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
            (repr (F := F) (α := α ::: Fix 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⟧))))))) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))
⊢ (wSetoid α : (P F).W α → (P F).W α → Prop)
    ((P F).wMk' (α := α)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
        (repr (F := F) (α := α ::: Fix 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:
apply wEquiv.abs'

Premises used: MvQPF.wEquiv.abs'
-- 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 α
a₁ :
  abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))
⊢ abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β :=
            α ::: (P F).W α) (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
            (repr (F := F) (α := α ::: Fix 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⟧))))))) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))

Tactic:
rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]

Premises used: MvPFunctor.wDest'_wMk', MvQPF.abs_repr, 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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
rhs : abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))
| abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))

Tactic:
rhs
-- 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 α
rw :
  abs (F := F) (α := α ::: (P F).W α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
      (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        ((P F).appendContents (α := α) f' f)))
| abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))

Tactic:
rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]

Premises used: MvPFunctor.wDest'_wMk', MvQPF.abs_repr, MvPFunctor.map_eq, MvQPF.wrepr_wMk, MvQPF.P
-- 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 α
rw :
  abs (F := F) (α := α ::: (P F).W α)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
      (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        ((P F).appendContents (α := α) f' f)))
| abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))

Tactic:
rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]

Premises used: MvPFunctor.wDest'_wMk', MvQPF.abs_repr, MvPFunctor.map_eq, MvQPF.wrepr_wMk, MvQPF.P
-- 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 α
a₁ :
  Eq (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
          ((P F).appendContents (α := α) f' f))))
⊢ abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))

Tactic:
conv =>
      rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]

Premises used: MvPFunctor.wDest'_wMk', MvQPF.abs_repr, MvPFunctor.map_eq, MvQPF.wrepr_wMk, MvQPF.P
-- 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 α
a₁ :
  comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
      ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
      ((P F).appendContents (α := α) f' f)
⊢ Eq (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
          ((P F).appendContents (α := α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))))
    (abs (F := F) (α := α ::: (P F).W α)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
        (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
          ((P F).appendContents (α := α) f' f))))

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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
a₁ :
  splitFun (α := (P F).B a) (α' := α ::: (P F).W α)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: (P F).W α).drop) (TypeVec.id (α := α)) f')
      (fixToW (F := F) (α := α) ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: (P F).W α)
      (comp (α := ((P F).B a).drop) (β := (α ::: (P F).W α).drop) (γ := (α ::: (P F).W α).drop) (TypeVec.id (α := α))
        f')
      (wrepr (F := F) (α := α) ∘ f)
⊢ Eq.{u + 1} (α := (P F).B a ⟹ α ::: (P F).W α)
    (comp (α := (P F).B a) (β := α ::: Fix F α) (γ := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α)))
      (splitFun (α := (P F).B a) (α' := α ::: Fix F α) f' fun (x : (P F).last.B a) ↦ ⟦f x⟧))
    (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
      (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))

Tactic:
rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]

Premises used: TypeVec.splitFun_comp, TypeVec.appendFun
-- 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 α
⊢ splitFun (α := (P F).B a) (α' := α ::: (P F).W α)
      (comp (α := ((P F).B a).drop) (β := (α ::: Fix F α).drop) (γ := (α ::: (P F).W α).drop) (TypeVec.id (α := α)) f')
      (fixToW (F := F) (α := α) ∘ fun (x : (P F).last.B a) ↦ ⟦f x⟧) =
    splitFun (α := (P F).B a) (α' := α ::: (P F).W α)
      (comp (α := ((P F).B a).drop) (β := (α ::: (P F).W α).drop) (γ := (α ::: (P F).W α).drop) (TypeVec.id (α := α))
        f')
      (wrepr (F := F) (α := α) ∘ f)

Tactic:
rfl