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
α_1 α β : TypeVec.{u} n
g : α ⟹ β
x : (↑(P F).wp : (α : TypeVec.{u} n) → Type u) α
⊢ Quot.mk (WEquiv (F := F) (α := β)) (map (F := (↑(P F).wp : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) g x) =
    Fix.map (F := F) (α := α) (β := β) g (Quot.mk (WEquiv (F := F) (α := α)) x)

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
symm : y.fst (β := β) = x
⊢ x = y.fst (β := β)

Tactic:
symm
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
dsimp :
  Sigma.fst (β := β)
      (rec (F := F) (α := α)
        (fun (i : F (α ::: Sigma β)) ↦
          Sigma.mk (β := β)
            (mk (F := F) (α := α)
              (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
            (g i))
        x) =
    x
⊢ y.fst (β := β) = x

Tactic:
dsimp [y]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
apply :
  ∀ (x : F (α ::: Fix F α)),
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
            Sigma.fst (β := β)
              (rec (F := F) (α := α)
                (fun (i : F (α ::: Sigma β)) ↦
                  Sigma.mk (β := β)
                    (mk (F := F) (α := α)
                      (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                    (g i))
                x))
          x =
        MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x →
      Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            (mk (F := F) (α := α) x)) =
        _root_.id (mk (F := F) (α := α) x)
⊢ Sigma.fst (β := β)
      (rec (F := F) (α := α)
        (fun (i : F (α ::: Sigma β)) ↦
          Sigma.mk (β := β)
            (mk (F := F) (α := α)
              (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
            (g i))
        x) =
    x

Tactic:
apply Fix.ind_rec _ id _ x

Premises used: id, MvQPF.Fix.ind_rec
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) _root_.id) x'
⊢ MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'

Tactic:
simp only [appendFun_id_id, MvFunctor.id_map] at ih

Premises used: MvFunctor.id_map, TypeVec.appendFun_id_id
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
e_x :
  MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i)))
        x') =
    x'
⊢ mk (F := F) (α := α)
      (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
        (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
            (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i)))
          x')) =
    mk (F := F) (α := α) x'

Tactic:
congr
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
rhs : x'
| MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i)))
        x') =
    x'

Tactic:
rhs
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
rw :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
      Sigma.fst (β := β)
        (rec (F := F) (α := α)
          (fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i))
          x))
    x'
| x'

Tactic:
rw [← ih]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
rw :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
      Sigma.fst (β := β)
        (rec (F := F) (α := α)
          (fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i))
          x))
    x'
| MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i)))
        x') =
    x'

Tactic:
rhs
      rw [← ih]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
e_x :
  Eq (α := F (α ::: Fix F α))
    (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i)))
        x'))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x')
⊢ MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β)))
      (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Sigma β)
        (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i)))
        x') =
    x'

Tactic:
conv =>
      rhs
      rw [← ih]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
x' : F (α ::: Fix F α)
ih :
  MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x' =
    x'
⊢ Eq (α := F (α ::: Fix F α))
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α))
        (Function.comp (β := Sigma β) (Sigma.fst (β := β))
          (rec (F := F) (α := α) fun (i : F (α ::: Sigma β)) ↦
            Sigma.mk (β := β)
              (mk (F := F) (α := α)
                (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                  (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
              (g i))))
      x')
    (MvFunctor.map (F := F) (α := α ::: Fix F α) (β := α ::: Fix F α)
      (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) fun (x : Fix F α) ↦
        Sigma.fst (β := β)
          (rec (F := F) (α := α)
            (fun (i : F (α ::: Sigma β)) ↦
              Sigma.mk (β := β)
                (mk (F := F) (α := α)
                  (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
                    (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
                (g i))
            x))
      x')

Tactic:
simp only [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g :
  (x : F (α ::: Sigma β)) →
    β
      (mk (F := F) (α := α)
        (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
          (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) x))
x : Fix F α
y : Sigma β :=
  rec (F := F) (α := α)
    (fun (i : F (α ::: Sigma β)) ↦
      Sigma.mk (β := β)
        (mk (F := F) (α := α)
          (MvFunctor.map (F := F) (α := α ::: Sigma β) (β := α ::: Fix F α)
            (appendFun (α := α) (α' := α) (TypeVec.id (α := α)) (Sigma.fst (β := β))) i))
        (g i))
    x
this : x = y.fst (β := β)
rw rw₁ : β (y.fst (β := β)) = β (y.fst (β := β))
⊢ β (y.fst (β := β)) = β x

Tactic:
rw [this]
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj
Goal:
n : ℕ
i : Fin2 n
α : TypeVec.{u_1} n
x : Prj i α
⊢ abs i (α := α) (repr i (α := α) x) = x

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj
Goal:
n : ℕ
i : Fin2 n
α β : TypeVec.{u_1} n
f : α ⟹ β
P : (↑(Prj.P i) : (α : TypeVec.{u_1} n) → Type u_1) α
mk :
  ∀ (fst : (Prj.P i).A) (snd : (Prj.P i).B fst ⟹ α),
    abs i (α := β)
        (MvFunctor.map (F := (↑(Prj.P i) : (α : TypeVec.{u_1} n) → Type u_1)) (α := α) (β := β) f
          (Sigma.mk (β := fun (a : (Prj.P i).A) ↦ (Prj.P i).B a ⟹ α) fst snd)) =
      MvFunctor.map (F := Prj i) (α := α) (β := β) f
        (abs i (α := α) (Sigma.mk (β := fun (a : (Prj.P i).A) ↦ (Prj.P i).B a ⟹ α) fst snd))
⊢ abs i (α := β) (MvFunctor.map (F := (↑(Prj.P i) : (α : TypeVec.{u_1} n) → Type u_1)) (α := α) (β := β) f P) =
    MvFunctor.map (F := Prj i) (α := α) (β := β) f (abs i (α := α) P)

Tactic:
cases P
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj
Goal:
n : ℕ
i : Fin2 n
α β : TypeVec.{u_1} n
f : α ⟹ β
fst : (P i).A
snd : (P i).B fst ⟹ α
⊢ abs i (α := β)
      (MvFunctor.map (F := (↑(P i) : (α : TypeVec.{u_1} n) → Type u_1)) (α := α) (β := β) f
        (Sigma.mk (β := fun (a : (P i).A) ↦ (P i).B a ⟹ α) fst snd)) =
    MvFunctor.map (F := Prj i) (α := α) (β := β) f
      (abs i (α := α) (Sigma.mk (β := fun (a : (P i).A) ↦ (P i).B a ⟹ α) fst snd))

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Multivariate.Constructions.Quot
Goal:
n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (α := α) (FG_repr (α := α) x) = x
FG_abs_map :
  ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α),
    FG_abs (α := β) (map (F := F) (α := α) (β := β) f x) = map (F := G) (α := α) (β := β) f (FG_abs (α := α) x)
α : TypeVec.{u} n
x : G α
rw : FG_abs (α := α) (FG_repr (α := α) x) = x
rw₁ rw₂ : x = x
⊢ FG_abs (α := α) (abs (F := F) (α := α) (repr (F := F) (α := α) (FG_repr (α := α) x))) = x

Tactic:
rw [abs_repr, FG_abs_repr]

Premises used: MvQPF.abs_repr