awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ dropFun (α := Subtype_ (α := α) p) (β := α) (subtypeVal (α := α) p) =
    subtypeVal (α := α.drop) (dropFun (α := α) (β := «repeat» (n + 1) Prop) p)

Tactic:
rfl

Premises used: rfl, TypeVec.dropFun, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ lastFun (α := Subtype_ (α := α) p) (β := α) (subtypeVal (α := α) p) = Subtype.val

Tactic:
rfl

Premises used: TypeVec.lastFun, rfl, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ dropFun (α := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p)
      (toSubtype (α := α) p) =
    toSubtype (α := fun (i : Fin2 n) ↦ α i.fs) fun (i : Fin2 n) ↦ p i.fs

Tactic:
rfl

Premises used: TypeVec.ofRepeat, TypeVec.toSubtype, TypeVec.drop, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ lastFun (α := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p)
      (toSubtype (α := α) p) =
    _root_.id

Tactic:
rfl

Premises used: TypeVec.last, TypeVec.lastFun, TypeVec.toSubtype, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ dropFun (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) })
      (ofSubtype (α := α) p) =
    ofSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» (n + 1) Prop) p)

Tactic:
rfl

Premises used: TypeVec.ofSubtype, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ lastFun (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) })
      (ofSubtype (α := α) p) =
    _root_.id

Tactic:
rfl

Premises used: TypeVec.last, TypeVec.lastFun, TypeVec.ofSubtype, TypeVec.Subtype_, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : Type u_1
R : β → β → Prop
⊢ dropFun (α := α ::: β ⊗ α ::: β) (β := «repeat» (n + 1) Prop) (α.RelLast' R) = α.repeatEq

Tactic:
rfl

Premises used: TypeVec.RelLast', TypeVec.splitFun, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ dropFun (α := α ⊗ α') (β := β ⊗ β') (prod.map (α := α) (α' := α') (β := β) (β' := β') f f') =
    prod.map (α := α.drop) (α' := α'.drop) (β := β.drop) (β' := β'.drop) (dropFun (α := α) (β := β) f)
      (dropFun (α := α') (β := β') f')

Tactic:
rfl

Premises used: TypeVec.prod.map, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ lastFun (α := α ⊗ α') (β := β ⊗ β') (prod.map (α := α) (α' := α') (β := β) (β' := β') f f') =
    Prod.map (lastFun (α := α) (β := β) f) (lastFun (α := α') (β := β') f')

Tactic:
rfl

Premises used: Prod.map, TypeVec.append1, TypeVec.prod, TypeVec.lastFun, TypeVec.prod.map, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ Eq.{u_1 + 1} (α := (α.drop ::: α.last).drop ⟹ α.drop)
    (dropFun (α := α.drop ::: α.last) (β := α) (fromAppend1DropLast (α := α))) (id (α := (α.drop ::: α.last).drop))

Tactic:
rfl

Premises used: Eq.mp, TypeVec.append1, TypeVec.Arrow.mp, TypeVec.fromAppend1DropLast, TypeVec.drop, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ Eq.{u_1 + 1} (α := (α.drop ::: α.last).last → α.last)
    (lastFun (α := α.drop ::: α.last) (β := α) (fromAppend1DropLast (α := α))) _root_.id

Tactic:
rfl

Premises used: TypeVec.last, TypeVec.append1, TypeVec.lastFun, TypeVec.Arrow.mp, TypeVec.fromAppend1DropLast, rfl
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ Eq.{u_1 + 1} (α := α.drop ⟹ α.drop) (dropFun (α := α) (β := α) (id (α := α))) (id (α := α.drop))

Tactic:
rfl

Premises used: TypeVec.drop, TypeVec.id, rfl, TypeVec.dropFun
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α β : TypeVec.{u_1} n
⊢ Eq.{u_1 + 1} (α := α ⊗ β ⟹ α ⊗ β) (prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)))
    (id (α := α ⊗ β))

Tactic:
prod_id

Premises used: TypeVec.prod_id
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
a :
  ∀ (i : Fin2 n) (x : Subtype_ (α := α) p i),
    comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (γ := Subtype_ (α := α) p)
        (toSubtype (α := α) p) (ofSubtype (α := α) p) i x =
      id (α := Subtype_ (α := α) p) i x
⊢ comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (γ := Subtype_ (α := α) p)
      (toSubtype (α := α) p) (ofSubtype (α := α) p) =
    id (α := Subtype_ (α := α) p)

Tactic:
ext i x
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ (α := α) p i
a :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α ⟹ «repeat» (n + 1) Prop) (x : Subtype_ (α := α) p Fin2.fz),
    comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
        Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) Fin2.fz x =
      id (α := Subtype_ (α := α) p) Fin2.fz x
a₁ :
  ∀ {n : ℕ} (a : Fin2 n),
    (∀ {α : TypeVec.{u_1} n} (p : α ⟹ «repeat» n Prop) (x : Subtype_ (α := α) p a),
        comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
            Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) a x =
          id (α := Subtype_ (α := α) p) a x) →
      ∀ {α : TypeVec.{u_1} (n + 1)} (p : α ⟹ «repeat» (n + 1) Prop) (x : Subtype_ (α := α) p a.fs),
        comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
            Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) a.fs x =
          id (α := Subtype_ (α := α) p) a.fs x
⊢ comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (γ := Subtype_ (α := α) p)
      (toSubtype (α := α) p) (ofSubtype (α := α) p) i x =
    id (α := Subtype_ (α := α) p) i x

Tactic:
induction i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α) p Fin2.fz
⊢ comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
      Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) Fin2.fz x =
    id (α := Subtype_ (α := α) p) Fin2.fz x

Tactic:
simp only [id, toSubtype, comp, ofSubtype] at *

Premises used: TypeVec.comp, TypeVec.ofSubtype, TypeVec.toSubtype, TypeVec.id
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a_1 : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (p : α ⟹ «repeat» n_1 Prop) (x : Subtype_ (α := α) p a_1),
    comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n_1) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
        Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) a_1 x =
      id (α := Subtype_ (α := α) p) a_1 x
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α) p a_1.fs
a :
  toSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» n_1.succ Prop) p) a_1
      (ofSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» (n_1 + 1) Prop) p) a_1 x) =
    x
⊢ comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
      Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) a_1.fs x =
    id (α := Subtype_ (α := α) p) a_1.fs x

Tactic:
simp only [id, toSubtype, comp, ofSubtype] at *

Premises used: TypeVec.comp, TypeVec.ofSubtype, TypeVec.toSubtype, TypeVec.id
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (p : α ⟹ «repeat» n_1 Prop) (x : Subtype_ (α := α) p a),
    toSubtype (α := α) p a (ofSubtype (α := α) p a x) = x
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α) p a.fs
⊢ toSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» n_1.succ Prop) p) a
      (ofSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» (n_1 + 1) Prop) p) a x) =
    x

Tactic:
simp [*]
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
a :
  ∀ (i : Fin2 n) (x : (fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) i),
    comp (α := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
        (subtypeVal (α := α) p) (toSubtype (α := α) p) i x =
      (↑x : α i)
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) =
    fun (x : Fin2 n) ↦ Subtype.val (p := fun (x_1 : α x) ↦ ofRepeat (p x x_1))

Tactic:
ext i x
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) i
a :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α ⟹ «repeat» (n + 1) Prop)
    (x : { x : α Fin2.fz // ofRepeat (p Fin2.fz x) }),
    comp (α := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
        (subtypeVal (α := α) p) (toSubtype (α := α) p) Fin2.fz x =
      (↑x : α Fin2.fz)
a₁ :
  ∀ {n : ℕ} (a : Fin2 n),
    (∀ {α : TypeVec.{u_1} n} (p : α ⟹ «repeat» n Prop) (x : (fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) a),
        comp (α := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
            (subtypeVal (α := α) p) (toSubtype (α := α) p) a x =
          (↑x : α a)) →
      ∀ {α : TypeVec.{u_1} (n + 1)} (p : α ⟹ «repeat» (n + 1) Prop) (x : { x : α a.fs // ofRepeat (p a.fs x) }),
        comp (α := fun (i : Fin2 (n + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
            (subtypeVal (α := α) p) (toSubtype (α := α) p) a.fs x =
          (↑x : α a.fs)
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) i x =
    (↑x : α i)

Tactic:
induction i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α Fin2.fz // ofRepeat (p Fin2.fz x) }
⊢ comp (α := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) Fin2.fz x =
    (↑x : α Fin2.fz)

Tactic:
simp only [toSubtype, comp, subtypeVal] at *

Premises used: TypeVec.comp, TypeVec.toSubtype, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a_1 : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (p : α ⟹ «repeat» n_1 Prop)
    (x : (fun (i : Fin2 n_1) ↦ { x : α i // ofRepeat (p i x) }) a_1),
    comp (α := fun (i : Fin2 n_1) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
        (subtypeVal (α := α) p) (toSubtype (α := α) p) a_1 x =
      (↑x : α a_1)
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α a_1.fs // ofRepeat (p a_1.fs x) }
a :
  subtypeVal (α := α.drop) (dropFun (α := α) (β := «repeat» (n_1 + 1) Prop) p) a_1
      (toSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» n_1.succ Prop) p) a_1 x) =
    (↑x : α a_1.fs)
⊢ comp (α := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) a_1.fs x =
    (↑x : α a_1.fs)

Tactic:
simp only [toSubtype, comp, subtypeVal] at *

Premises used: TypeVec.comp, TypeVec.toSubtype, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (p : α ⟹ «repeat» n_1 Prop) (x : { x : α a // ofRepeat (p a x) }),
    subtypeVal (α := α) p a (toSubtype (α := α) p a x) = (↑x : α a)
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α a.fs // ofRepeat (p a.fs x) }
⊢ subtypeVal (α := α.drop) (dropFun (α := α) (β := «repeat» (n_1 + 1) Prop) p) a
      (toSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» n_1.succ Prop) p) a x) =
    (↑x : α a.fs)

Tactic:
simp [*]
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : Arrow.{u_2, u_1} β (Subtype_ (α := α) p)
rw : comp (α := β) (β := Subtype_ (α := α) p) (γ := Subtype_ (α := α) p) (id (α := Subtype_ (α := α) p)) f = f
⊢ comp (α := β) (β := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (γ := Subtype_ (α := α) p)
      (toSubtype (α := α) p)
      (comp (α := β) (β := Subtype_ (α := α) p) (γ := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) })
        (ofSubtype (α := α) p) f) =
    f

Tactic:
rw [← comp_assoc, toSubtype_of_subtype]

Premises used: TypeVec.toSubtype_of_subtype, TypeVec.comp_assoc
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : Arrow.{u_2, u_1} β (Subtype_ (α := α) p)
⊢ comp (α := β) (β := Subtype_ (α := α) p) (γ := Subtype_ (α := α) p) (id (α := Subtype_ (α := α) p)) f = f

Tactic:
simp
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
a :
  ∀ (i : Fin2 n) (x : Subtype_ (α := α ⊗ α) r i),
    comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 n) ↦
        { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
        (toSubtype' (α := α) r) (ofSubtype' (α := α) r) i x =
      id (α := Subtype_ (α := α ⊗ α) r) i x
⊢ comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 n) ↦
      { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
      (toSubtype' (α := α) r) (ofSubtype' (α := α) r) =
    id (α := Subtype_ (α := α ⊗ α) r)

Tactic:
ext i x
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ (α := α ⊗ α) r i
a :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (r : α ⊗ α ⟹ «repeat» (n + 1) Prop) (x : Subtype_ (α := α ⊗ α) r Fin2.fz),
    comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 (n + 1)) ↦
        { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
        (toSubtype' (α := α) r) (ofSubtype' (α := α) r) Fin2.fz x =
      id (α := Subtype_ (α := α ⊗ α) r) Fin2.fz x
a₁ :
  ∀ {n : ℕ} (a : Fin2 n),
    (∀ {α : TypeVec.{u_1} n} (r : α ⊗ α ⟹ «repeat» n Prop) (x : Subtype_ (α := α ⊗ α) r a),
        comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 n) ↦
            { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
            (toSubtype' (α := α) r) (ofSubtype' (α := α) r) a x =
          id (α := Subtype_ (α := α ⊗ α) r) a x) →
      ∀ {α : TypeVec.{u_1} (n + 1)} (r : α ⊗ α ⟹ «repeat» (n + 1) Prop) (x : Subtype_ (α := α ⊗ α) r a.fs),
        comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 (n + 1)) ↦
            { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
            (toSubtype' (α := α) r) (ofSubtype' (α := α) r) a.fs x =
          id (α := Subtype_ (α := α ⊗ α) r) a.fs x
⊢ comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 n) ↦
      { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
      (toSubtype' (α := α) r) (ofSubtype' (α := α) r) i x =
    id (α := Subtype_ (α := α ⊗ α) r) i x

Tactic:
induction i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α ⊗ α) r Fin2.fz
a : (⟨(↑x : (α ⊗ α) Fin2.fz), ⋯⟩ : { x : (α ⊗ α) Fin2.fz // r Fin2.fz x }) = x
⊢ comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 (n_1 + 1)) ↦
      { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
      (toSubtype' (α := α) r) (ofSubtype' (α := α) r) Fin2.fz x =
    id (α := Subtype_ (α := α ⊗ α) r) Fin2.fz x

Tactic:
dsimp only [id, toSubtype', comp, ofSubtype'] at *

Premises used: TypeVec.toSubtype', TypeVec.comp, TypeVec.ofSubtype', TypeVec.id
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a_1 : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (r : α ⊗ α ⟹ «repeat» n_1 Prop) (x : Subtype_ (α := α ⊗ α) r a_1),
    comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 n_1) ↦
        { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
        (toSubtype' (α := α) r) (ofSubtype' (α := α) r) a_1 x =
      id (α := Subtype_ (α := α ⊗ α) r) a_1 x
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α ⊗ α) r a_1.fs
a :
  toSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a_1
      (ofSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a_1 x) =
    x
⊢ comp (α := Subtype_ (α := α ⊗ α) r) (β := fun (i : Fin2 (n_1 + 1)) ↦
      { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (γ := Subtype_ (α := α ⊗ α) r)
      (toSubtype' (α := α) r) (ofSubtype' (α := α) r) a_1.fs x =
    id (α := Subtype_ (α := α ⊗ α) r) a_1.fs x

Tactic:
dsimp only [id, toSubtype', comp, ofSubtype'] at *

Premises used: TypeVec.toSubtype', TypeVec.comp, TypeVec.ofSubtype', TypeVec.id
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α ⊗ α) r Fin2.fz
⊢ (⟨(↑x : (α ⊗ α) Fin2.fz), ⋯⟩ : { x : (α ⊗ α) Fin2.fz // r Fin2.fz x }) = x

Tactic:
simp [*]
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (r : α ⊗ α ⟹ «repeat» n_1 Prop) (x : Subtype_ (α := α ⊗ α) r a),
    toSubtype' (α := α) r a (ofSubtype' (α := α) r a x) = x
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α ⊗ α) r a.fs
⊢ toSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a
      (ofSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a x) =
    x

Tactic:
simp [*]
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
a :
  ∀ (i : Fin2 n) (x : (fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) i),
    comp (α := fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
        Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) i x =
      prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
      Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) =
    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

Tactic:
ext i x
-- Module: Mathlib.Data.TypeVec
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) i
a :
  ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (r : α ⊗ α ⟹ «repeat» (n + 1) Prop)
    (x : { x : α Fin2.fz × α Fin2.fz // ofRepeat (r Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz x.1 x.2)) }),
    comp (α := fun (i : Fin2 (n + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
        Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) Fin2.fz x =
      prod.mk (α := α) (β := α) Fin2.fz (↑x : α Fin2.fz × α Fin2.fz).1 (↑x : α Fin2.fz × α Fin2.fz).2
a₁ :
  ∀ {n : ℕ} (a : Fin2 n),
    (∀ {α : TypeVec.{u_1} n} (r : α ⊗ α ⟹ «repeat» n Prop)
        (x : (fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) a),
        comp (α := fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
            Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a x =
          prod.mk (α := α) (β := α) a (↑x : α a × α a).1 (↑x : α a × α a).2) →
      ∀ {α : TypeVec.{u_1} (n + 1)} (r : α ⊗ α ⟹ «repeat» (n + 1) Prop)
        (x : { x : α a.fs × α a.fs // ofRepeat (r a.fs (prod.mk (α := α) (β := α) a.fs x.1 x.2)) }),
        comp (α := fun (i : Fin2 (n + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) })
            (β := Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a.fs x =
          prod.mk (α := α) (β := α) a.fs (↑x : α a.fs × α a.fs).1 (↑x : α a.fs × α a.fs).2
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
      Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) i x =
    prod.mk (α := α) (β := α) i (↑x : α i × α i).1 (↑x : α i × α i).2

Tactic:
induction i
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α Fin2.fz × α Fin2.fz // ofRepeat (r Fin2.fz (prod.mk (α := α) (β := α) Fin2.fz x.1 x.2)) }
⊢ comp (α := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
      Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) Fin2.fz x =
    prod.mk (α := α) (β := α) Fin2.fz (↑x : α Fin2.fz × α Fin2.fz).1 (↑x : α Fin2.fz × α Fin2.fz).2

Tactic:
simp only [toSubtype', comp, subtypeVal, prod.mk] at *

Premises used: TypeVec.prod.mk, TypeVec.toSubtype', TypeVec.comp, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a_1 : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (r : α ⊗ α ⟹ «repeat» n_1 Prop)
    (x : (fun (i : Fin2 n_1) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) a_1),
    comp (α := fun (i : Fin2 n_1) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
        Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a_1 x =
      prod.mk (α := α) (β := α) a_1 (↑x : α a_1 × α a_1).1 (↑x : α a_1 × α a_1).2
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α a_1.fs × α a_1.fs // ofRepeat (r a_1.fs (prod.mk (α := α) (β := α) a_1.fs x.1 x.2)) }
a :
  subtypeVal (α := (α ⊗ α).drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a_1
      (toSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a_1 x) =
    prod.mk (α := fun (i : Fin2 n_1) ↦ α i.fs) (β := fun (i : Fin2 n_1) ↦ α i.fs) a_1 (↑x : α a_1.fs × α a_1.fs).1
      (↑x : α a_1.fs × α a_1.fs).2
⊢ comp (α := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i × α i // ofRepeat (r i (prod.mk (α := α) (β := α) i x.1 x.2)) }) (β :=
      Subtype_ (α := α ⊗ α) r) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) r) (toSubtype' (α := α) r) a_1.fs x =
    prod.mk (α := α) (β := α) a_1.fs (↑x : α a_1.fs × α a_1.fs).1 (↑x : α a_1.fs × α a_1.fs).2

Tactic:
simp only [toSubtype', comp, subtypeVal, prod.mk] at *

Premises used: TypeVec.prod.mk, TypeVec.toSubtype', TypeVec.comp, TypeVec.subtypeVal
-- Module: Mathlib.Data.TypeVec
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (r : α ⊗ α ⟹ «repeat» n_1 Prop)
    (x : { x : α a × α a // ofRepeat (r a (prod.mk (α := α) (β := α) a x.1 x.2)) }),
    subtypeVal (α := α ⊗ α) r a (toSubtype' (α := α) r a x) =
      prod.mk (α := α) (β := α) a (↑x : α a × α a).1 (↑x : α a × α a).2
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : { x : α a.fs × α a.fs // ofRepeat (r a.fs (prod.mk (α := α) (β := α) a.fs x.1 x.2)) }
⊢ subtypeVal (α := (α ⊗ α).drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a
      (toSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a x) =
    prod.mk (α := fun (i : Fin2 n_1) ↦ α i.fs) (β := fun (i : Fin2 n_1) ↦ α i.fs) a (↑x : α a.fs × α a.fs).1
      (↑x : α a.fs × α a.fs).2

Tactic:
simp [*]
-- Module: Mathlib.Data.UInt
Goal:
n : UInt8
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 8 < 55296

Tactic:
decide