awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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
⊢ 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)
have rw : g
    (abs (F := F) (α := α ::: β)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: Fix F α) (β := α ::: β)
        (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (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.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)) (α := α ::: Fix F α) (β := α ::: β)
          (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
            (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)
⊢ 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)
have rw₁ : g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
      (abs (F := F) (α := α ::: Fix 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.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)) (α := α ::: Fix F α) (β := α ::: β)
          (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
            (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)
rw₁ :
  g
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
        (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
        (abs (F := F) (α := α ::: Fix 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)
⊢ 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)
have rw₂ : g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (comp (α := α ::: Fix F α) (β := α ::: (P F).W α) (γ := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (fixToW (F := F) (α := α))))
      (abs (F := F) (α := α ::: Fix F α) (repr (F := F) (α := α ::: Fix F α) x))) =
  g
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: β)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (rec (F := F) (α := α) g)) x)
Tactic: rw [← MvPFunctor.comp_map, abs_map, ← h, abs_repr, ← appendFun_comp, id_comp, this]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)⟧
have 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))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
⊢ (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))
have 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)))
Tactic: apply wEquiv.abs'
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
⊢ 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)))
have 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)))
Tactic: rw [MvPFunctor.wDest'_wMk', abs_map, abs_repr, ← abs_map, MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
| 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)))
have rhs : abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))
Tactic: rhs
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
| abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)))
have 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)))
Tactic: rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
| 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)))
have 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)))
Tactic: rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
⊢ 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)))
have 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))))
Tactic: conv =>
      rhs
      rw [wrepr_wMk, q.P.wDest'_wMk', abs_repr, MvPFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
⊢ 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))))
have 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)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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 α
⊢ 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))
have 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)
Tactic: rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (hypothesis)
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⟧))) =
    ⟦(P F).wMk (α := α) a f' f⟧
have 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)⟧
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
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)⟧
⊢ 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⟧
have rw : Eq (α := Fix F α) ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧ ⟦(P F).wMk (α := α) a f' f⟧
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)⟧
⊢ Eq (α := Fix F α) ⟦wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)⟧ ⟦(P F).wMk (α := α) a f' f⟧
have a₁ : (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 Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)
⊢ ∀ (x : Fix F α), g₁ x = g₂ x
have 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)
Tactic: apply Quot.ind
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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)
x : (P F).W α
⊢ g₁ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) x) =
    g₂ (Quot.mk (⇑(wSetoid α) : (P F).W α → (P F).W α → Prop) x)
have 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))
Tactic: induction x using q.P.wInd
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (goal)
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))
⊢ 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))
have change : g₁ ⟦(P F).wMk (α := α) a f' f⟧ = g₂ ⟦(P F).wMk (α := α) a f' f⟧
Tactic: change g₁ ⟦q.P.wMk a f' f⟧ = g₂ ⟦q.P.wMk a f' f⟧