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
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 ih : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α)
  (h :
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f)) =
      abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) y)),
  WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f) 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
y : (P F).W α
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
⊢ ∀
    (h :
      abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀)) =
        abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) y)),
    WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) y
have ih : ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α)
  (h :
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀)) =
      abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) ((P F).wMk (α := α) a f' f))),
  WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀ f'₀ f₀) ((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
x y : (P F).W α
h : WEquiv (F := F) (α := α) x y
⊢ WEquiv (F := F) (α := α) y x
have 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) (α := α) (f₁ x) (f₀ x)),
  WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f₁) ((P F).wMk (α := α) a f' f₀)
Tactic: induction h with
  | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
  | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
Cleared hypotheses: 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
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) (α := α) (f₁ x) (f₀ x)),
    WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f₁) ((P F).wMk (α := α) a f' f₀)
⊢ WEquiv (F := F) (α := α) y x
have 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 α))
      (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₁)))),
  WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₁ f'₁ f₁) ((P F).wMk (α := α) a₀ f'₀ f₀)
Tactic: induction h with
  | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
  | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
Cleared hypotheses: 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
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) (α := α) (f₁ x) (f₀ x)),
    WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f₁) ((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) (α := α) ((P F).wMk (α := α) a₁ f'₁ f₁) ((P F).wMk (α := α) a₀ f'₀ f₀)
⊢ WEquiv (F := F) (α := α) y x
have trans : ∀ (x y z : (P F).W α) (_e₁ : WEquiv (F := F) (α := α) x y) (_e₂ : WEquiv (F := F) (α := α) y z)
  (ih₁ : WEquiv (F := F) (α := α) y x) (ih₂ : WEquiv (F := F) (α := α) z y), WEquiv (F := F) (α := α) z x
Tactic: induction h with
  | ind a f' f₀ f₁ _h ih => exact WEquiv.ind _ _ _ _ ih
  | abs a₀ f'₀ f₀ a₁ f'₁ f₁ h => exact WEquiv.abs _ _ _ _ _ _ h.symm
  | trans x y z _e₁ _e₂ ih₁ ih₂ => exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁
Cleared hypotheses: 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
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f) =
    (P F).wMk' (α := α)
      (repr (F := F) (α := α ::: (P F).W α)
        (abs (F := F) (α := α ::: (P F).W α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f)))))
have rw : Eq (α := (P F).W α)
  (((P F).wMk' (α := α) ∘ repr (F := F) (α := α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (recF (F := F) (α := α) ((P F).wMk' (α := α) ∘ repr (F := F) (α := α ::: (P F).W α))))
        (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)))))
  ((P F).wMk' (α := α)
    (repr (F := F) (α := α ::: (P F).W α)
      (abs (F := F) (α := α ::: (P F).W α)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
            (recF (F := F) (α := α) ((P F).wMk' (α := α) ∘ repr (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))))))
Tactic: rw [wrepr, recF_eq', q.P.wDest'_wMk]
-- 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 : (P F).W α
⊢ WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) x) x
have ih : ∀ (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), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)) →
    WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)) ((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
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), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)) ((P F).wMk (α := α) a f' f)
have a₁ : WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))
  ((P F).wMk' (α := α)
    (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
Tactic: apply WEquiv.trans _ (q.P.wMk' (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
a₁ :
  WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))
    ((P F).wMk' (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
⊢ WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)) ((P F).wMk (α := α) a f' f)
have a₂ : WEquiv (F := F) (α := α)
  ((P F).wMk' (α := α)
    (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
  ((P F).wMk (α := α) a f' f)
Tactic: apply WEquiv.trans _ (q.P.wMk' (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))
    ((P F).wMk' (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
have a₁ : 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' (α := α)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ 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' (α := α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f)))))
have a₁ : Eq (α := F (α ::: (P F).W α))
  (abs (F := F) (α := α ::: (P F).W α)
    ((P F).wDest' (α := α)
      ((P F).wMk' (α := α)
        (repr (F := F) (α := α ::: (P F).W α)
          (abs (F := F) (α := α ::: (P F).W α)
            (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
              (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
              (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 α)
    ((P F).wDest' (α := α)
      ((P F).wMk' (α := α)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))))
Tactic: rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
a₁ :
  Eq (α := F (α ::: (P F).W α))
    (abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (repr (F := F) (α := α ::: (P F).W α)
            (abs (F := F) (α := α ::: (P F).W α)
              (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
                (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 α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (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 α) ((P F).wDest' (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f))) =
    abs (F := F) (α := α ::: (P F).W α)
      ((P F).wDest' (α := α)
        ((P F).wMk' (α := α)
          (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
            (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f)))))
have a₂ : Eq (α := F (α ::: (P F).W α))
  (abs (F := F) (α := α ::: (P F).W α)
    (repr (F := F) (α := α ::: (P F).W α)
      (abs (F := F) (α := α ::: (P F).W α)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
          (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 α)
    ((P F).wDest' (α := α)
      ((P F).wMk' (α := α)
        (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
          (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))))
Tactic: rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ WEquiv (F := F) (α := α)
    ((P F).wMk' (α := α)
      (map (F := (↑(P F) : (α : TypeVec.{u} (n + 1)) → Type u)) (α := α ::: (P F).W α) (β := α ::: (P F).W α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (wrepr (F := F) (α := α)))
        (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ α ::: (P F).W α) a ((P F).appendContents (α := α) f' f))))
    ((P F).wMk (α := α) a f' f)
have a₁ : WEquiv (F := F) (α := α)
  ((P F).wMk (α := α) a
    (dropFun (α := (P F).B a) (β := α ::: (P F).W α)
      (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' (wrepr (F := F) (α := α) ∘ f)))
    (lastFun (α := (P F).B a) (β := α ::: (P F).W α)
      (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' (wrepr (F := F) (α := α) ∘ f))))
  ((P F).wMk (α := α) a f' f)
Tactic: rw [q.P.map_eq, MvPFunctor.wMk', appendFun_comp_splitFun, 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
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), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ WEquiv (F := F) (α := α)
    ((P F).wMk (α := α) a
      (dropFun (α := (P F).B a) (β := α ::: (P F).W α)
        (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' (wrepr (F := F) (α := α) ∘ f)))
      (lastFun (α := (P F).B a) (β := α ::: (P F).W α)
        (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' (wrepr (F := F) (α := α) ∘ f))))
    ((P F).wMk (α := α) a f' f)
have a₁ : ∀ (x : (P F).last.B a),
  WEquiv (F := F) (α := α)
    (lastFun (α := (P F).B a) (β := α ::: (P F).W α)
      (splitFun (α := (P F).B a) (α' := α ::: (P F).W α) f' (wrepr (F := F) (α := α) ∘ f)) x)
    (f x)
Tactic: apply WEquiv.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
g : α ⟹ β
x y : (P F).W α
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₁))
have ind : WEquiv (F := F) (α := β)
  ((P F).wMk (α := β) a (comp (α := (P F).drop.B a) (β := α) (γ := β) g f') fun (i : (P F).last.B a) ↦
    map (F := (P F).W) (α := α) (β := β) g (f₀ i))
  ((P F).wMk (α := β) a (comp (α := (P F).drop.B a) (β := α) (γ := β) g f') fun (i : (P F).last.B a) ↦
    map (F := (P F).W) (α := α) (β := β) g (f₁ i))
Tactic: rw [q.P.w_map_wMk, q.P.w_map_wMk]
-- 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
g : α ⟹ β
x y : (P F).W α
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 α))
    (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₁)))
⊢ 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₁))
have abs : WEquiv (F := F) (α := β)
  ((P F).wMk (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (i : (P F).last.B a₀) ↦
    map (F := (P F).W) (α := α) (β := β) g (f₀ i))
  ((P F).wMk (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (i : (P F).last.B a₁) ↦
    map (F := (P F).W) (α := α) (β := β) g (f₁ i))
Tactic: rw [q.P.w_map_wMk, q.P.w_map_wMk]
-- 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
g : α ⟹ β
x y : (P F).W α
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 α))
    (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₁)))
⊢ WEquiv (F := F) (α := β)
    ((P F).wMk (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (i : (P F).last.B a₀) ↦
      map (F := (P F).W) (α := α) (β := β) g (f₀ i))
    ((P F).wMk (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (i : (P F).last.B a₁) ↦
      map (F := (P F).W) (α := α) (β := β) g (f₁ i))
have abs : 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 (α := β) (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (i : (P F).last.B a₀) ↦
        map (F := (P F).W) (α := α) (β := β) g (f₀ i))))
  (abs (F := F) (α := β ::: (P F).W β)
    (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ β ::: (P F).W β) a₁
      ((P F).appendContents (α := β) (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (i : (P F).last.B a₁) ↦
        map (F := (P F).W) (α := α) (β := β) g (f₁ i))))
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
g : α ⟹ β
x y : (P F).W α
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 α))
    (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₁)))
⊢ 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 (α := β) (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (i : (P F).last.B a₀) ↦
          map (F := (P F).W) (α := α) (β := β) g (f₀ i))))
    (abs (F := F) (α := β ::: (P F).W β)
      (Sigma.mk (β := fun (a : (P F).A) ↦ (P F).B a ⟹ β ::: (P F).W β) a₁
        ((P F).appendContents (α := β) (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (i : (P F).last.B a₁) ↦
          map (F := (P F).W) (α := α) (β := β) g (f₁ i))))
have abs : Eq (α := F (β ::: (P F).W β))
  (abs (F := F) (α := β ::: (P F).W β)
    ((P F).objAppend1 (α := β) a₀ (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (x : (P F).last.B a₀) ↦
      (P F).wMap (α := α) (β := β) g (f₀ x)))
  (abs (F := F) (α := β ::: (P F).W β)
    ((P F).objAppend1 (α := β) a₁ (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (x : (P F).last.B a₁) ↦
      (P F).wMap (α := α) (β := β) g (f₁ x)))
Tactic: 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))