awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Fix (hypothesis)
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'
⊢ 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'
have 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'
Tactic: simp only [appendFun_id_id, MvFunctor.id_map] at ih
Cleared hypotheses: ih
-- 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
β : 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'
⊢ 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'
have 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'
Tactic: congr
-- 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
β : 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'
| 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'
have rhs : x'
Tactic: rhs
-- 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
β : 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'
| x'
have 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'
Tactic: rw [← ih]
-- 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
β : 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'
| 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'
have 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'
Tactic: rhs
      rw [← ih]
-- 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
β : 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'
⊢ 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'
have 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')
Tactic: conv =>
      rhs
      rw [← ih]
-- 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
β : 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 (β := β)
⊢ β (y.fst (β := β)) = β x
have rw : β (y.fst (β := β)) = β (y.fst (β := β))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Prj (goal)
Goal:
n : ℕ
i : Fin2 n
α β : TypeVec.{u_1} n
f : α ⟹ β
P : (↑(Prj.P i) : (α : TypeVec.{u_1} n) → Type u_1) α
⊢ 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)
have 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))
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Quot (goal)
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 α
⊢ FG_abs (α := α) (abs (F := F) (α := α) (repr (F := F) (α := α) (FG_repr (α := α) x))) = x
have rw : FG_abs (α := α) (FG_repr (α := α) x) = x
Tactic: rw [abs_repr, FG_abs_repr]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Quot (goal)
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
⊢ FG_abs (α := α) (abs (F := F) (α := α) (repr (F := F) (α := α) (FG_repr (α := α) x))) = x
have rw₁ : x = x
Tactic: rw [abs_repr, FG_abs_repr]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Quot (goal)
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
f : α ⟹ β
p : (↑(P F) : (α : TypeVec.{u} n) → Type u) α
⊢ FG_abs (α := β) (abs (F := F) (α := β) (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f p)) =
    map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
have rw : FG_abs (α := β) (map (F := F) (α := α) (β := β) f (abs (F := F) (α := α) p)) =
  map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
Tactic: rw [abs_map, FG_abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Quot (goal)
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
f : α ⟹ β
p : (↑(P F) : (α : TypeVec.{u} n) → Type u) α
rw :
  FG_abs (α := β) (map (F := F) (α := α) (β := β) f (abs (F := F) (α := α) p)) =
    map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
⊢ FG_abs (α := β) (abs (F := F) (α := β) (map (F := (↑(P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f p)) =
    map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
have rw₁ : map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p)) =
  map (F := G) (α := α) (β := β) f (FG_abs (α := α) (abs (F := F) (α := α) p))
Tactic: rw [abs_map, FG_abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Multivariate.Constructions.Sigma (goal)
Goal:
n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst_1 : (α : A) → MvQPF (F α)
α β : TypeVec.{u} n
f : α ⟹ β
x : (Pi.P F).A
g : (Pi.P F).B x ⟹ α
⊢ Pi.abs F (α := β)
      (map (F := (↑(Pi.P F) : (α : TypeVec.{u} n) → Type u)) (α := α) (β := β) f
        (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g)) =
    map (F := Pi F) (α := α) (β := β) f
      (Pi.abs F (α := α) (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g))
have simp : Eq (α := Pi F β)
  (match (motive := (↑(Pi.P F) : (α : TypeVec.{u} n) → Type u) β → Pi F β)
      (Pi.P F).map (α := α) (β := β) f (Sigma.mk (β := fun (a : (Pi.P F).A) ↦ (Pi.P F).B a ⟹ α) x g) with
    | ⟨a, f⟩ => fun (x : A) ↦
      abs (F := F x) (α := β)
        (Sigma.mk (β := fun (a : (P (F x)).A) ↦ (P (F x)).B a ⟹ β) (a x) fun (i : Fin2 n) (y : (P (F x)).B (a x) i) ↦
          f i (Sigma.mk (β := fun (a_1 : A) ↦ (P (F a_1)).B (a a_1) i) x y)) :
    Pi F β)
  fun (a : A) ↦
  abs (F := F a) (α := β)
    ((P (F a)).map (α := α) (β := β) f
      (Sigma.mk (β := fun (a_1 : (P (F a)).A) ↦ (P (F a)).B a_1 ⟹ α) (x a) fun (i : Fin2 n) (y : (P (F a)).B (x a) i) ↦
        g i (Sigma.mk (β := fun (a : A) ↦ (P (F a)).B (x a) i) a y)))
Tactic: simp only [Pi.abs, (· <$$> ·), ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
x : F α
⊢ id <$> x = x
have rw : id <$> abs.{u, u_1, v} (repr x) = abs.{u, u_1, v} (repr x)
Tactic: rw [← abs_repr x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
x : F α
⊢ id <$> abs.{u, u_1, v} (repr x) = abs.{u, u_1, v} (repr x)
have obtain : ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
  Eq (α := F α) (id <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: obtain ⟨a, f⟩ := repr x
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
x : F α
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
⊢ Eq (α := F α) (id <$> abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
    (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
have rw : Eq (α := F α) (abs ((P F).map id (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f)))
  (abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f))
Tactic: rw [← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> x = g <$> f <$> x
have rw : (g ∘ f) <$> abs.{u, u_1, v} (repr x) = g <$> f <$> abs.{u, u_1, v} (repr x)
Tactic: rw [← abs_repr x]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs.{u, u_1, v} (repr x) = g <$> f <$> abs.{u, u_1, v} (repr x)
have rw : abs.{u, u_1, v} ((P F).map (g ∘ f) (repr x)) = abs.{u, u_1, v} ((P F).map g ((P F).map f (repr x)))
Tactic: rw [← abs_map, ← abs_map, ← abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type v
q : QPF.{u, u_1, v} F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x ↔
    ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
have mp : Liftp p x →
  ∃ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) ∧ ∀ (i : (P F).B a), p (f i)
Tactic: constructor