awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
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:
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
x : (P F).W α
⊢ WEquiv (F := F) (α := α) x x

Tactic:
abs' x x rfl

Premises used: MvQPF.wEquiv.abs', rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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) (α := α) (f₁ x) (f₀ x)
⊢ WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f₁) ((P F).wMk (α := α) a f' f₀)

Tactic:
WEquiv.ind _ _ _ _ ih

Premises used: MvQPF.WEquiv.ind
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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) (α := α) (f₁ x) (f₀ x)
⊢ WEquiv (F := F) (α := α) ((P F).wMk (α := α) a f' f₁) ((P F).wMk (α := α) a f' f₀)

Tactic:
exact WEquiv.ind _ _ _ _ ih

Premises used: MvQPF.WEquiv.ind
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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₁ f'₁ f₁) ((P F).wMk (α := α) a₀ f'₀ f₀)

Tactic:
WEquiv.abs _ _ _ _ _ _ h.symm

Premises used: MvQPF.WEquiv.abs, Eq.symm
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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₁ f'₁ f₁) ((P F).wMk (α := α) a₀ f'₀ f₀)

Tactic:
exact WEquiv.abs _ _ _ _ _ _ h.symm

Premises used: MvQPF.WEquiv.abs, Eq.symm
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x_1 y_1 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:
MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

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
x_1 y_1 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:
exact MvQPF.WEquiv.trans _ _ _ ih₂ ih₁

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
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₀)
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
⊢ WEquiv (F := F) (α := α) y 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₁

Premises used: MvQPF.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 α
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))))))
⊢ 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)))))

Tactic:
rw [wrepr, recF_eq', q.P.wDest'_wMk]

Premises used: MvPFunctor.wDest'_wMk, MvQPF.recF_eq', MvQPF.P, MvQPF.wrepr
-- 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 α
⊢ 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:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : (P F).W α
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)
⊢ WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) x) x

Tactic:
induction x using q.P.wInd
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
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))))
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)
⊢ WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) ((P F).wMk (α := α) a f' f)) ((P F).wMk (α := α) a f' f)

Tactic:
apply WEquiv.trans _ (q.P.wMk' (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))

Premises used: MvPFunctor.wMk', MvPFunctor.appendContents, MvQPF.WEquiv.trans, TypeVec.appendFun, Sigma.mk, MvQPF.P, MvFunctor.map, MvQPF.wrepr, TypeVec.id
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
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)))))
⊢ 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.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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
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)
⊢ 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:
rw [q.P.map_eq, MvPFunctor.wMk', appendFun_comp_splitFun, id_comp]

Premises used: MvPFunctor.wMk', MvPFunctor.map_eq, TypeVec.id_comp, MvQPF.P, TypeVec.appendFun_comp_splitFun
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
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)
⊢ 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:
apply WEquiv.ind

Premises used: MvQPF.WEquiv.ind
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ ∀ (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:
ih

Premises used: MvQPF.recF, TypeVec.lastFun, MvPFunctor.wRec, MvQPF.wrepr, TypeVec.splitFun
-- 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 α
ih : ∀ (i : (P F).last.B a), WEquiv (F := F) (α := α) (wrepr (F := F) (α := α) (f i)) (f i)
⊢ ∀ (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:
exact 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 α
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))
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))
⊢ 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₁))

Tactic:
rw [q.P.w_map_wMk, q.P.w_map_wMk]

Premises used: MvPFunctor.w_map_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
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 ind :
  ∀ (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) (α := β)
    ((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:
apply WEquiv.ind

Premises used: MvQPF.WEquiv.ind
-- 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 α
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))
⊢ ∀ (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))

Tactic:
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 α
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))
⊢ ∀ (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))

Tactic:
exact 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 α
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₁)))
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))
⊢ 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₁))

Tactic:
rw [q.P.w_map_wMk, q.P.w_map_wMk]

Premises used: MvPFunctor.w_map_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
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 α))
    (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₁)))
abs :
  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 (α := β) (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (i : (P F).last.B a₀) ↦
          map (F := (P F).W) (α := α) (β := β) g (f₀ i))))
    (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 (α := β) (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (i : (P F).last.B a₁) ↦
          map (F := (P F).W) (α := α) (β := β) g (f₁ i))))
⊢ 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:
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
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 α))
    (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₁)))
abs :
  Eq (α := F (β ::: (P F).W β))
    (MvQPF.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)))
    (MvQPF.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)))
⊢ 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 (α := β) (comp (α := (P F).drop.B a₀) (β := α) (γ := β) g f'₀) fun (i : (P F).last.B a₀) ↦
          map (F := (P F).W) (α := α) (β := β) g (f₀ i))))
    (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 (α := β) (comp (α := (P F).drop.B a₁) (β := α) (γ := β) g f'₁) fun (i : (P F).last.B a₁) ↦
          map (F := (P F).W) (α := α) (β := β) g (f₁ i))))

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))

Premises used: MvPFunctor.wMap, TypeVec.comp, MvPFunctor.objAppend1, MvQPF.P, MvQPF.abs