awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst_1 : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) }),
    map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (fun (i : Fin2 n) (t : { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) }) ↦
              (↑t : α i × α i).1)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (fun (i : Fin2 n) (t : { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) }) ↦
              (↑t : α i × α i).2)
            u =
          y ↔
      map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (comp (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
              (β := α ⊗ α) (γ := α) (prod.fst (α := α) (β := α))
              fun (i : Fin2 n) (x : { x : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i x.1 x.2)) }) ↦
              prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2)
            u =
          x ∧
        map (F := F) (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
            (β := α)
            (comp (α := fun (i : Fin2 n) ↦ { p : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i p.1 p.2)) })
              (β := α ⊗ α) (γ := α) (prod.snd (α := α) (β := α))
              fun (i : Fin2 n) (x : { x : α i × α i // ofRepeat (R i (prod.mk (α := α) (β := α) i x.1 x.2)) }) ↦
              prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2)
            u =
          y

Tactic:
simp +unfoldPartialApp [comp]

Premises used: TypeVec.comp
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' pp i p_1) }) i.fs
⊢ ofRepeat (α.PredLast' pp i.fs (↑x : (α ::: β) i.fs)) = α.PredLast pp (↑x : (α ::: β) i.fs)

Tactic:
grind [PredLast]

Premises used: TypeVec.PredLast
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast pp p_1 }) i.fs
erw erw₁ : True = True
⊢ True = ofRepeat (α.PredLast' pp i.fs (↑x : (α ::: β) i.fs))

Tactic:
erw [const_iff_true]

Premises used: TypeVec.const_iff_true
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
dsimp :
  (∃ (u : F fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
        x) ↔
    ∃ (u : F fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) u =
        x
⊢ LiftP' (α := α ::: β) (F := F) (α.PredLast' P) x ↔ LiftP (F := F) (α := α ::: β) (α.PredLast P) x

Tactic:
dsimp only [LiftP, LiftP']

Premises used: MvFunctor.LiftP', MvFunctor.LiftP
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
h₀ :
  comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 })
h₁ :
  ∀ (u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }),
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
        x ↔
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P))
          (map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
            fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) u) =
        x
⊢ (∃ (u : F fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
        x) ↔
    ∃ (u : F fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)),
      map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) u =
        x

Tactic:
apply exists_iff_exists_of_mono F (f _ n α) (g _ n α)

Premises used: _private.0.MvFunctor.f, _private.0.MvFunctor.g, MvFunctor.exists_iff_exists_of_mono
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
h₀ :
  ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i) (property : α.PredLast P x),
    (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) i
            (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) i) =
      (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) i
            (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) i)
⊢ comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
      { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) =
    TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 })

Tactic:
ext i ⟨x, _⟩
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x_1 : F (α ::: β)
i : Fin2 (n + 1)
x : (α ::: β) i
property : α.PredLast P x
h₀ :
  ∀ (x : (α ::: β) Fin2.fz) (property : α.PredLast P x),
    (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) Fin2.fz
            (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) Fin2.fz) =
      (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) Fin2.fz
            (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) Fin2.fz)
h₁ :
  ∀ (a : Fin2 n) (x : (α ::: β) a.fs) (property : α.PredLast P x),
    (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
            { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) a.fs
            (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) a.fs) =
      (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) a.fs
            (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ α.PredLast P p_1) x property)) :
        (α ::: β) a.fs)
⊢ (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) i
          (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) i)

Tactic:
cases i
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x_1 : F (α ::: β)
x : (α ::: β) Fin2.fz
property : α.PredLast P x
⊢ (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) Fin2.fz
          (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) Fin2.fz) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) Fin2.fz
          (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x_1 : F (α ::: β)
a : Fin2 n
x : (α ::: β) a.fs
property : α.PredLast P x
⊢ (↑(comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (β := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (γ := fun (i : Fin2 (n + 1)) ↦
          { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) (g P n α) a.fs
          (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) a.fs) =
    (↑(TypeVec.id (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) a.fs
          (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ α.PredLast P p_1) x property)) :
      (α ::: β) a.fs)

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
h₁ :
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
          fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (γ := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) (f P n α))
        u =
      x
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P))
        (map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
          fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // α.PredLast P p_1 }) (f P n α) u) =
      x

Tactic:
rw [MvFunctor.map_map]

Premises used: MvFunctor.map_map
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
h₁ :
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (comp (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β :=
          fun (i : Fin2 (n + 1)) ↦ Subtype (α := (α ::: β) i) (α.PredLast P)) (γ := α ::: β)
          (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := α.PredLast P)) (f P n α))
        u =
      x

Tactic:
dsimp +unfoldPartialApp [(· ⊚ ·)]

Premises used: TypeVec.comp
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
this :
  Eq.{u + 1} (α := (i : Fin2 (n + 1)) → (self : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) → (α ::: β) i)
    (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)))
    fun (i : Fin2 (n + 1)) (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
    (↑(f P n α i x) : (α ::: β) i)
rw rw₁ :
  map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1))
            (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x

Tactic:
rw [this]
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
h₁ :
  Eq.{u + 1} (α := (i : Fin2 (n + 1)) → (self : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) → (α ::: β) i)
    (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)))
    fun (i : Fin2 (n + 1)) (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
    (↑(f P n α i x) : (α ::: β) i)
⊢ map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { x : (α ::: β) i // ofRepeat (α.PredLast' P i x) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (x : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i x))) u =
      x ↔
    map (F := F) (α := fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) (β := α ::: β)
        (fun (i : Fin2 (n + 1)) (x : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) ↦
          (↑(f P n α i x) : (α ::: β) i))
        u =
      x

Tactic:
suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw [this]
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
h₁ :
  ∀ (i : Fin2 (n + 1)) (x : (α ::: β) i) (property : ofRepeat (α.PredLast' P i x)),
    (↑(Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property) : (α ::: β) i) =
      (↑(f P n α i (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property)) :
        (α ::: β) i)
⊢ Eq.{u + 1} (α := (i : Fin2 (n + 1)) → (self : { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) → (α ::: β) i)
    (fun (i : Fin2 (n + 1)) ↦ Subtype.val (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)))
    fun (i : Fin2 (n + 1)) (x : (fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }) i) ↦
    (↑(f P n α i x) : (α ::: β) i)

Tactic:
ext i ⟨x, _⟩
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x_1 : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
i : Fin2 (n + 1)
x : (α ::: β) i
property : ofRepeat (α.PredLast' P i x)
h₁ :
  ∀ (x : (α ::: β) Fin2.fz) (property : ofRepeat (α.PredLast' P Fin2.fz x)),
    (↑(Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property) :
        (α ::: β) Fin2.fz) =
      (↑(f P n α Fin2.fz
            (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property)) :
        (α ::: β) Fin2.fz)
h₂ :
  ∀ (a : Fin2 n) (x : (α ::: β) a.fs) (property : ofRepeat (α.PredLast' P a.fs x)),
    (↑(Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ ofRepeat (α.PredLast' P a.fs p_1)) x property) : (α ::: β) a.fs) =
      (↑(f P n α a.fs (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ ofRepeat (α.PredLast' P a.fs p_1)) x property)) :
        (α ::: β) a.fs)
⊢ (↑(Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property) : (α ::: β) i) =
    (↑(f P n α i (Subtype.mk (p := fun (p_1 : (α ::: β) i) ↦ ofRepeat (α.PredLast' P i p_1)) x property)) : (α ::: β) i)

Tactic:
cases i
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x_1 : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
x : (α ::: β) Fin2.fz
property : ofRepeat (α.PredLast' P Fin2.fz x)
⊢ (↑(Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property) :
      (α ::: β) Fin2.fz) =
    (↑(f P n α Fin2.fz
          (Subtype.mk (p := fun (p_1 : (α ::: β) Fin2.fz) ↦ ofRepeat (α.PredLast' P Fin2.fz p_1)) x property)) :
      (α ::: β) Fin2.fz)

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x_1 : F (α ::: β)
u : F fun (i : Fin2 (n + 1)) ↦ { p_1 : (α ::: β) i // ofRepeat (α.PredLast' P i p_1) }
a : Fin2 n
x : (α ::: β) a.fs
property : ofRepeat (α.PredLast' P a.fs x)
⊢ (↑(Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ ofRepeat (α.PredLast' P a.fs p_1)) x property) : (α ::: β) a.fs) =
    (↑(f P n α a.fs (Subtype.mk (p := fun (p_1 : (α ::: β) a.fs) ↦ ofRepeat (α.PredLast' P a.fs p_1)) x property)) :
      (α ::: β) a.fs)

Tactic:
rfl
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x :
  (fun (i : Fin2 (x_1 + 1)) ↦
      { p_1 : (α ::: β) i × (α ::: β) i //
        ofRepeat (α.RelLast' rr i (prod.mk (α := α ::: β) (β := α ::: β) i p_1.1 p_1.2)) })
    i.fs
erw erw₁ :
  ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
    ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)
⊢ ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)) =
    ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)

Tactic:
erw [repeatEq_iff_eq]

Premises used: TypeVec.repeatEq_iff_eq
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) i.fs
simp :
  ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
    ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2))
⊢ α.RelLast rr (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2 =
    ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2))

Tactic:
simp only [RelLast]

Premises used: TypeVec.RelLast
-- Module: Mathlib.Control.Functor.Multivariate
Goal:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst : MvFunctor F
inst_1 : LawfulMvFunctor F
α_1 : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x_1 : ℕ
α : TypeVec.{u} x_1
i : Fin2 x_1
x : (fun (i : Fin2 (x_1 + 1)) ↦ { p_1 : (α ::: β) i × (α ::: β) i // α.RelLast rr p_1.1 p_1.2 }) i.fs
erw erw₁ :
  ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
    ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2)
⊢ ((↑x : (α ::: β) i.fs × (α ::: β) i.fs).1 = (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2) =
    ofRepeat
      (α.RelLast' rr i.fs
        (prod.mk (α := α ::: β) (β := α ::: β) i.fs (↑x : (α ::: β) i.fs × (α ::: β) i.fs).1
          (↑x : (α ::: β) i.fs × (α ::: β) i.fs).2))

Tactic:
erw [repeatEq_iff_eq]

Premises used: TypeVec.repeatEq_iff_eq