awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Comp (goal)
Goal:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst_1 : MvQPF F
inst_2 : (i : Fin2 n) → MvQPF (G i)
α_1 β_1 : TypeVec.{u} m
f_1 : α_1 ⟹ β_1
p : (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u) α_1
⊢ Eq (α := Comp F G β_1)
    (Comp.mk (F := F) (G := G) (α := β_1)
      (MvFunctor.map (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) β_1) (β :=
        fun (i : Fin2 n) ↦ G i β_1) (fun (x : Fin2 n) ↦ abs (F := G x) (α := β_1))
        (abs (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) β_1)
          (comp.get (α := β_1)
            (MvFunctor.map (F := (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u)) (α := α_1)
              (β := β_1) f_1 p)))))
    (MvFunctor.map (F := Comp F G) (α := α_1) (β := β_1) f_1
      (Comp.mk (F := F) (G := G) (α := α_1)
        (MvFunctor.map (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) α_1) (β :=
          fun (i : Fin2 n) ↦ G i α_1) (fun (x : Fin2 n) ↦ abs (F := G x) (α := α_1))
          (abs (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) α_1)
            (comp.get (α := α_1) p)))))
have rw : Eq (α := Comp F G β_1)
  (Comp.mk (F := F) (G := G) (α := β_1)
    (abs (F := F) (α := fun (i : Fin2 n) ↦ G i β_1)
      (MvFunctor.map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := fun (x : Fin2 n) ↦
        (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) β_1) (β := fun (i : Fin2 n) ↦ G i β_1)
        (fun (x : Fin2 n) ↦ abs (F := G x) (α := β_1))
        (comp.get (α := β_1)
          (MvFunctor.map (F := (↑((P F).comp fun (i : Fin2 n) ↦ P (G i)) : (α : TypeVec.{u} m) → Type u)) (α := α_1)
            (β := β_1) f_1 p)))))
  (MvFunctor.map (F := Comp F G) (α := α_1) (β := β_1) f_1
    (Comp.mk (F := F) (G := G) (α := α_1)
      (MvFunctor.map (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) α_1) (β :=
        fun (i : Fin2 n) ↦ G i α_1) (fun (x : Fin2 n) ↦ abs (F := G x) (α := α_1))
        (abs (F := F) (α := fun (x : Fin2 n) ↦ (↑(P (G x)) : (α : TypeVec.{u} m) → Type u) α_1)
          (comp.get (α := α_1) p)))))
Tactic: rw [← abs_map]
-- 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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f))))
have rw : g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' fun (i : (P F).last.B a) ↦
          (P F).wRec (α := α)
            (fun (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (_f : (P F).last.B a → (P F).W α) (rec : (P F).last.B a → β) ↦
              g
                (abs (F := F) (α := α ::: β)
                  (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
                    (splitFun (α := (P F).B a) (α' := α ::: β) f' rec))))
            (f i)))) =
  g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f))))
Tactic: rw [recF, MvPFunctor.wRec_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
β : Type u
g : F (α ::: β) → β
x : (P F).W α
⊢ recF (F := F) (α := α) g x =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g)) ((P F).wDest' (α := α) x)))
have ih : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
  recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
Tactic: induction x using q.P.wCases
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 : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
have rw : g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
  g
    (abs (F := F) (α := α ::: β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
        ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
Tactic: rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]
-- 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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
rw :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
⊢ recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
have rw₁ : g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
  g
    (abs (F := F) (α := α ::: β)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
          (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
Tactic: rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]
-- 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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
rw :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
rw₁ :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
            (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
⊢ recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
have rw₂ : g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
  g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
Tactic: rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]
-- 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 (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
rw :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
rw₁ :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a
            (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
rw₂ :
  g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
    g
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (comp (α := (P F).B a) (β := α ::: (P F).W α) (γ := α ::: β)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
            (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' f))))
⊢ recF (F := F) (α := α) g ((P F).wMk (α := α) a f' f) =
    g
      (abs (F := F) (α := α ::: β)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (recF (F := F) (α := α) g))
          ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))))
have rw₃ : g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) g ∘ f)))) =
  g
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β)
          (comp (α := ((P F).B a).drop) (β := α) (γ := (α ::: β).drop) (TypeVec.id (α := α)) f')
          (recF (F := F) (α := α) g ∘ f))))
Tactic: rw [recF_eq, q.P.wDest'_wMk, MvPFunctor.map_eq, appendFun_comp_splitFun, TypeVec.id_comp]
-- 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
u : F (α ::: β) → β
x y : (P F).W α
⊢ WEquiv (F := F) (α := α) x y → recF (F := F) (α := α) u x = recF (F := F) (α := α) u y
have ih : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
  WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f) y →
    recF (F := F) (α := α) u ((P F).wMk (α := α) a f' f) = recF (F := F) (α := α) u y
Tactic: induction x using q.P.wCases
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
u : F (α ::: β) → β
y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
⊢ WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) y →
    recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u y
have ih : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
  WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) ((P F).wMk (α := α) a f' f) →
    recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a f' f)
Tactic: induction y using q.P.wCases
Cleared hypotheses: y
-- 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
u : F (α ::: β) → β
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 : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) ((P F).wMk (α := α) a₁ f'₁ f₁)
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a₁ f'₁ f₁)
have refine_1 : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
  (a_1 : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x)),
  (∀ (x : (P F).last.B a),
      (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
          recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
        (f₀ x) (f₁ x) sorry) →
    (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
        recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
      ((P F).wMk (α := α) a f' f₀) ((P F).wMk (α := α) a f' f₁) sorry
Tactic: refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
-- 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
u : F (α ::: β) → β
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 : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) ((P F).wMk (α := α) a₁ f'₁ f₁)
refine_1 :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
    (a_1 : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x)),
    (∀ (x : (P F).last.B a),
        (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
            recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
          (f₀ x) (f₁ x) ⋯) →
      (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
          recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
        ((P F).wMk (α := α) a f' f₀) ((P F).wMk (α := α) a f' f₁) ⋯
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a₁ f'₁ f₁)
have refine_2 : ∀ (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 α)
  (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₀ ((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₁ ((P F).appendContents (α := α) f'₁ f₁)))),
  (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
      recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
    ((P F).wMk (α := α) a₀ f'₀ f₀) ((P F).wMk (α := α) a₁ f'₁ f₁) sorry
Tactic: refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
-- 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
u : F (α ::: β) → β
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 : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) ((P F).wMk (α := α) a₁ f'₁ f₁)
refine_1 :
  ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α)
    (a_1 : ∀ (x : (P F).last.B a), WEquiv (F := F) (α := α) (f₀ x) (f₁ x)),
    (∀ (x : (P F).last.B a),
        (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
            recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
          (f₀ x) (f₁ x) ⋯) →
      (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
          recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
        ((P F).wMk (α := α) a f' f₀) ((P F).wMk (α := α) a f' f₁) ⋯
refine_2 :
  ∀ (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 α)
    (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₀ ((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₁ ((P F).appendContents (α := α) f'₁ f₁)))),
    (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
        recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
      ((P F).wMk (α := α) a₀ f'₀ f₀) ((P F).wMk (α := α) a₁ f'₁ f₁) ⋯
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a₁ f'₁ f₁)
have refine_3 : ∀ (u_1 v w : (P F).W α) (a : WEquiv (F := F) (α := α) u_1 v) (a_1 : WEquiv (F := F) (α := α) v w),
  (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
        recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
      u_1 v a →
    (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
          recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
        v w a_1 →
      (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
          recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
        u_1 w sorry
Tactic: refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
-- 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
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀_1 : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁_1 : (P F).last.B a₁ → (P F).W α
h : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀_1) ((P F).wMk (α := α) a₁ f'₁ f₁_1)
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),
    (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
        recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
      (f₀ x) (f₁ x) ⋯
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a f' f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a f' f₁)
have refine_1 : u
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) u ∘ f₀)))) =
  u
    (abs (F := F) (α := α ::: β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
        (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) u ∘ f₁))))
Tactic: simp only [recF_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
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀_1 : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁_1 : (P F).last.B a₁ → (P F).W α
h : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀_1) ((P F).wMk (α := α) a₁ f'₁ f₁_1)
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),
    (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
        recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
      (f₀ x) (f₁ x) ⋯
⊢ u
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) u ∘ f₀)))) =
    u
      (abs (F := F) (α := α ::: β)
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: β) a
          (splitFun (α := (P F).B a) (α' := α ::: β) f' (recF (F := F) (α := α) u ∘ f₁))))
have refine_1 : recF (F := F) (α := α) u ∘ f₀ = recF (F := F) (α := α) u ∘ f₁
Tactic: congr 4
-- 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
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀_1 : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁_1 : (P F).last.B a₁ → (P F).W α
h : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀_1) ((P F).wMk (α := α) a₁ f'₁ f₁_1)
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),
    (fun (a a' : (P F).W α) (x : WEquiv (F := F) (α := α) a a') ↦
        recF (F := F) (α := α) u a = recF (F := F) (α := α) u a')
      (f₀ x) (f₁ x) ⋯
⊢ recF (F := F) (α := α) u ∘ f₀ = recF (F := F) (α := α) u ∘ f₁
have refine_1 : ∀ (x : ((P F).B a).last), (recF (F := F) (α := α) u ∘ f₀) x = (recF (F := F) (α := α) u ∘ f₁) x
Tactic: funext
-- 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
x y : (P F).W α
h :
  abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) x) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) y)
⊢ WEquiv (F := F) (α := α) x y
have revert : ∀
  (h :
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) x) =
      abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) y)),
  WEquiv (F := F) (α := α) x y
Tactic: revert h
Cleared hypotheses: h