case fz
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝ : α✝ i
b✝ : β✝ i
n✝ : ℕ
α β : TypeVec (succ n✝)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst Fin2.fz (prod.mk Fin2.fz a b) = a

case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.fst (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = a
n : ℕ
α β : TypeVec n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst i (prod.mk i a b) = a
induction' i with _ _ _ i_ih
case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.fst (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = a
case fz
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝ : α✝ i
b✝ : β✝ i
n✝ : ℕ
α β : TypeVec (succ n✝)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst Fin2.fz (prod.mk Fin2.fz a b) = a

case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.fst (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = a
simp_all only [prod.fst, prod.mk]
no goals
case fs
n : ℕ
α✝ β✝ : TypeVec n
i : Fin2 n
a✝¹ : α✝ i
b✝ : β✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec (succ n✝)
a : α (Fin2.fs a✝)
b : β (Fin2.fs a✝)
⊢ prod.fst (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) a b) = a
apply i_ih