case h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : last fun i => { x // ofRepeat (p i x) }
⊢ lastFun (toSubtype p) i = _root_.id i
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
⊢ lastFun (toSubtype p) = _root_.id
ext i : 2
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) { val := val✝, property := property✝ } = _root_.id { val := val✝, property := property✝ }
case h
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
i : last fun i => { x // ofRepeat (p i x) }
⊢ lastFun (toSubtype p) i = _root_.id i
induction i
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) { val := val✝, property := property✝ } = _root_.id { val := val✝, property := property✝ }
simp [dropFun, *]
no goals
case h.mk
n : ℕ
α : TypeVec (n + 1)
p : α ⟹ repeat (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
rfl