awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
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
simp :
  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)))))
⊢ 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))

Tactic:
simp only [(· ∘ ·)]

Premises used: Function.comp
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
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
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)))))
⊢ 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)))))

Tactic:
rw [← abs_map]

Premises used: MvQPF.abs_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp
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)
      (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:
simp +unfoldPartialApp only [comp.get_map, map_map, TypeVec.comp,
      abs_map, map_mk]

Premises used: MvPFunctor.comp.get_map, TypeVec.comp, MvQPF.Comp.map_mk, MvQPF.abs_map, MvFunctor.map_map
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Const
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
x : Const n A α
⊢ Const.mk (α := α) (x.get (α := α)) = x

Tactic:
rfl

Premises used: MvQPF.Const.mk, MvQPF.Const.get, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Const
Goal:
n : ℕ
A : Type u
α : TypeVec.{u} n
x : A
⊢ Const.get (α := α) (Const.mk (α := α) x) = x

Tactic:
rfl

Premises used: MvQPF.Const.mk, MvQPF.Const.get, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Const
Goal:
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : A
⊢ MvFunctor.map (F := Const n A) (α := α) (β := β) f (Const.mk (α := α) x) = Const.mk (α := β) x

Tactic:
rfl

Premises used: MvQPF.Const.mk, MvQPF.Const.map, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Const
Goal:
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : Const n A α
⊢ (MvFunctor.map (F := Const n A) (α := α) (β := β) f x).get (α := β) = x.get (α := α)

Tactic:
rfl

Premises used: MvQPF.Const.map, MvQPF.Const.get, rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
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' 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))))
⊢ 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))))

Tactic:
rw [recF, MvPFunctor.wRec_eq]

Premises used: MvQPF.recF, MvPFunctor.wRec_eq
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ 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:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
x : (P F).W α
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))))
⊢ 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)))

Tactic:
induction x using q.P.wCases
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
x y : (P F).W α
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
⊢ WEquiv (F := F) (α := α) x y → recF (F := F) (α := α) u x = recF (F := F) (α := α) u y

Tactic:
induction x using q.P.wCases
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 α
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)
⊢ 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 y using q.P.wCases
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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₁)

Tactic:
@WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_

Premises used: MvQPF.WEquiv.recOn
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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₁) ⋯
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 ⋯
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a₁ f'₁ f₁)

Tactic:
refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_

Premises used: MvQPF.WEquiv.recOn
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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) ⋯
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₁))))
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a f' f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a f' f₁)

Tactic:
simp only [recF_eq]

Premises used: MvQPF.recF_eq
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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) ⋯
refine_1 : recF (F := F) (α := α) u ∘ 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₀)))) =
    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:
congr 4
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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) ⋯
refine_1 : ∀ (x : ((P F).B a).last), (recF (F := F) (α := α) u ∘ f₀) x = (recF (F := F) (α := α) u ∘ f₁) x
⊢ recF (F := F) (α := α) u ∘ f₀ = recF (F := F) (α := α) u ∘ f₁

Tactic:
funext
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
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) ⋯
x : ((P F).B a).last
⊢ (recF (F := F) (α := α) u ∘ f₀) x = (recF (F := F) (α := α) u ∘ f₁) x

Tactic:
apply ih
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀_1 : (P F).A
f'₀_1 : (P F).drop.B a₀_1 ⟹ α
f₀_1 : (P F).last.B a₀_1 → (P F).W α
a₁_1 : (P F).A
f'₁_1 : (P F).drop.B a₁_1 ⟹ α
f₁_1 : (P F).last.B a₁_1 → (P F).W α
h_1 : WEquiv (F := F) (α := α) ((P F).wMk (α := α) a₀_1 f'₀_1 f₀_1) ((P F).wMk (α := α) a₁_1 f'₁_1 f₁_1)
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₁)))
⊢ recF (F := F) (α := α) u ((P F).wMk (α := α) a₀ f'₀ f₀) = recF (F := F) (α := α) u ((P F).wMk (α := α) a₁ f'₁ f₁)

Tactic:
simp only [recF_eq', abs_map, MvPFunctor.wDest'_wMk, h]

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

Tactic:
Eq.trans ih₁ ih₂

Premises used: Eq.trans
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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₁)
x y z : (P F).W α
_e₁ : WEquiv (F := F) (α := α) x y
_e₂ : WEquiv (F := F) (α := α) y z
ih₁ : recF (F := F) (α := α) u x = recF (F := F) (α := α) u y
ih₂ : recF (F := F) (α := α) u y = recF (F := F) (α := α) u z
⊢ recF (F := F) (α := α) u x = recF (F := F) (α := α) u z

Tactic:
exact Eq.trans ih₁ ih₂

Premises used: Eq.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 :
  abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) x) =
    abs (F := F) (α := α ::: (P F).W α) ((P F).wDest' (α := α) y)
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
⊢ WEquiv (F := F) (α := α) x y

Tactic:
revert h
-- 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 α
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
⊢ ∀
    (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:
induction x using q.P.wCases
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
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 α
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)
⊢ ∀
    (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 y using q.P.wCases