awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u} n
i : Fin2 n
x : α i
a :
  ∀ {n : ℕ} {α : TypeVec.{u} (n + 1)} (x : α Fin2.fz),
    comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
        (diagSub (α := α)) Fin2.fz x =
      prod.diag (α := α) Fin2.fz x
⊢ comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) i x =
    prod.diag (α := α) i x
have a₁ : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α : TypeVec.{u} n} (x : α a),
      comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
          (diagSub (α := α)) a x =
        prod.diag (α := α) a x)
  {α : TypeVec.{u} (n + 1)} (x : α a.fs),
  comp (α := α) (β := Subtype_ (α := α ⊗ α) α.repeatEq) (γ := α ⊗ α) (subtypeVal (α := α ⊗ α) α.repeatEq)
      (diagSub (α := α)) a.fs x =
    prod.diag (α := α) a.fs x
Tactic: induction i with
  | fz => simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]
  | fs _ i_ih => apply @i_ih (drop α)
Cleared hypotheses: α, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
⊢ Eq.{u + 1} (α := α ⊗ β ⟹ α ⊗ β) (prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)))
    (id (α := α ⊗ β))
have a : ∀ (i : Fin2 n) (a : (α ⊗ β) i),
  prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) i a = id (α := α ⊗ β) i a
Tactic: ext i a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n n_1 : ℕ
α β : TypeVec.{u} (n_1 + 1)
a : (α ⊗ β) Fin2.fz
⊢ prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz a = id (α := α ⊗ β) Fin2.fz a
have a₁ : ∀ (fst : α.last) (snd : β.last),
  Eq.{u + 1} (α := (α ⊗ β) Fin2.fz)
    (prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz (fst, snd))
    (id (α := α ⊗ β) Fin2.fz (fst, snd))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
i : Fin2 n
a : (α ⊗ β) i
⊢ prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) i a = id (α := α ⊗ β) i a
have a₁ : ∀ {n : ℕ} {α β : TypeVec.{u} (n + 1)} (a : (α ⊗ β) Fin2.fz),
  prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz a = id (α := α ⊗ β) Fin2.fz a
Tactic: induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, β, i, a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α β : TypeVec.{u} n
i : Fin2 n
a : (α ⊗ β) i
a₁ :
  ∀ {n : ℕ} {α β : TypeVec.{u} (n + 1)} (a : (α ⊗ β) Fin2.fz),
    prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) Fin2.fz a = id (α := α ⊗ β) Fin2.fz a
⊢ prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) i a = id (α := α ⊗ β) i a
have a₂ : ∀ {n : ℕ} (a : Fin2 n)
  (i_ih :
    ∀ {α β : TypeVec.{u} n} (a_1 : (α ⊗ β) a),
      prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) a a_1 = id (α := α ⊗ β) a a_1)
  {α β : TypeVec.{u} (n + 1)} (a_1 : (α ⊗ β) a.fs),
  prod.map (α := α) (α' := β) (β := α) (β' := β) (id (α := α)) (id (α := β)) a.fs a_1 = id (α := α ⊗ β) a.fs a_1
Tactic: induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih
Cleared hypotheses: α, β, i, a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁)
have a : ∀ (i : Fin2 (n + 1)) (a : ((α ⊗ β) ::: (φ × ψ)) i),
  appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) i a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) i a
Tactic: ext i a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) i a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) i a
have a₁ : ∀ (a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz),
  appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
      Fin2.fz a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz a
Tactic: cases i
Cleared hypotheses: i, a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
a₁ :
  ∀ (a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz),
    appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
        Fin2.fz a =
      prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
        (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz a
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) i a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) i a
have a₂ : ∀ (a : Fin2 n) (a_1 : ((α ⊗ β) ::: (φ × ψ)) a.fs),
  appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁) a.fs
      a_1 =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) a.fs a_1
Tactic: cases i
Cleared hypotheses: i, a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
      Fin2.fz a =
    prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz a
have a₁ : ∀ (fst : φ) (snd : ψ),
  Eq (α := ((α' ⊗ β') ::: (φ' × ψ')) Fin2.fz)
    (appendFun (α := α ⊗ β) (α' := α' ⊗ β') (prod.map (α := α) (α' := β) (β := α') (β' := β') f₀ g₀) (Prod.map f₁ g₁)
      Fin2.fz (fst, snd))
    (prod.map (α := α ::: φ) (α' := β ::: ψ) (β := α' ::: φ') (β' := β' ::: ψ') (appendFun (α := α) (α' := α') f₀ f₁)
      (appendFun (α := β) (α' := β') g₀ g₁) Fin2.fz (fst, snd))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (γ := Subtype_ (α := α) p)
      (toSubtype (α := α) p) (ofSubtype (α := α) p) =
    id (α := Subtype_ (α := α) p)
have 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
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
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
have 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
Tactic: induction i
Cleared hypotheses: α, p, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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
⊢ 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
have 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
Tactic: induction i
Cleared hypotheses: α, p, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (p : α ⟹ «repeat» n_1 Prop) (x : Subtype_ (α := α) p a),
    comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 n_1) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
        Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) a x =
      id (α := Subtype_ (α := α) p) a x
α : TypeVec.{u_1} (n_1 + 1)
p : α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α) p a.fs
⊢ comp (α := Subtype_ (α := α) p) (β := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i // ofRepeat (p i x) }) (γ :=
      Subtype_ (α := α) p) (toSubtype (α := α) p) (ofSubtype (α := α) p) a.fs x =
    id (α := Subtype_ (α := α) p) a.fs x
have a : toSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» n_1.succ Prop) p) a
    (ofSubtype (α := α.drop) (dropFun (α := α) (β := «repeat» (n_1 + 1) Prop) p) a x) =
  x
Tactic: simp only [id, toSubtype, comp, ofSubtype] at *
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
⊢ 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))
have 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)
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) i x =
    (↑x : α i)
have 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)
Tactic: induction i
Cleared hypotheses: α, p, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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)
⊢ comp (α := fun (i : Fin2 n) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) i x =
    (↑x : α i)
have 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)
Tactic: induction i
Cleared hypotheses: α, p, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n n_1 : ℕ
a : 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),
    comp (α := fun (i : Fin2 n_1) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
        (subtypeVal (α := α) p) (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) }
⊢ comp (α := fun (i : Fin2 (n_1 + 1)) ↦ { x : α i // ofRepeat (p i x) }) (β := Subtype_ (α := α) p) (γ := α)
      (subtypeVal (α := α) p) (toSubtype (α := α) p) a.fs x =
    (↑x : α a.fs)
have a : 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 only [toSubtype, comp, subtypeVal] at *
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : Arrow.{u_2, u_1} β (Subtype_ (α := α) p)
⊢ 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
have rw : comp (α := β) (β := Subtype_ (α := α) p) (γ := Subtype_ (α := α) p) (id (α := Subtype_ (α := α) p)) f = f
Tactic: rw [← comp_assoc, toSubtype_of_subtype]
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ 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)
have 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
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
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
have 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
Tactic: induction i
Cleared hypotheses: α, r, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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
⊢ 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
have 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
Tactic: induction i
Cleared hypotheses: α, r, i, x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n n_1 : ℕ
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α ⊗ α) r Fin2.fz
⊢ 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
have a : (⟨(↑x : (α ⊗ α) Fin2.fz), sorry⟩ : { x : (α ⊗ α) Fin2.fz // r Fin2.fz x }) = x
Tactic: dsimp only [id, toSubtype', comp, ofSubtype'] at *
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih :
  ∀ {α : TypeVec.{u_1} n_1} (r : α ⊗ α ⟹ «repeat» n_1 Prop) (x : Subtype_ (α := α ⊗ α) r a),
    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 x =
      id (α := Subtype_ (α := α ⊗ α) r) a x
α : TypeVec.{u_1} (n_1 + 1)
r : α ⊗ α ⟹ «repeat» (n_1 + 1) Prop
x : Subtype_ (α := α ⊗ α) r a.fs
⊢ 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.fs x =
    id (α := Subtype_ (α := α ⊗ α) r) a.fs x
have a : toSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a
    (ofSubtype' (α := α.drop) (dropFun (α := α ⊗ α) (β := «repeat» (n_1 + 1) Prop) r) a x) =
  x
Tactic: dsimp only [id, toSubtype', comp, ofSubtype'] at *
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
Goal:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ 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
have 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
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Data.TypeVec (goal)
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
⊢ 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
have 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
Tactic: induction i
Cleared hypotheses: α, r, i, x