case a.h
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (p i x) }) i
⊢ (subtypeVal p ⊚ toSubtype p) i x = ↑x
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
⊢ subtypeVal p ⊚ toSubtype p = fun x => Subtype.val
ext (i x)
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : { x // ofRepeat (p a✝ x) }), subtypeVal p a✝ (toSubtype p a✝ x) = ↑x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (p (Fin2.fs a✝) x) }
⊢ subtypeVal (dropFun p) a✝ (toSubtype (dropFun p) a✝ x) = ↑x
case a.h
n : ℕ
α : TypeVec n
p : α ⟹ repeat n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (p i x) }) i
⊢ (subtypeVal p ⊚ toSubtype p) i x = ↑x
induction i <;> dsimp only [toSubtype, comp, subtypeVal] at *
no goals
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec n✝} (p : α ⟹ repeat n✝ Prop) (x : { x // ofRepeat (p a✝ x) }), subtypeVal p a✝ (toSubtype p a✝ x) = ↑x
α : TypeVec (Nat.succ n✝)
p : α ⟹ repeat (Nat.succ n✝) Prop
x : { x // ofRepeat (p (Fin2.fs a✝) x) }
⊢ subtypeVal (dropFun p) a✝ (toSubtype (dropFun p) a✝ x) = ↑x
simp [*]