case a.h
n✝ n : ℕ
α : TypeVec n
i : Fin2 n
x : α i
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) i x = prod.diag i x
n✝ n : ℕ
α : TypeVec n
⊢ subtypeVal (repeatEq α) ⊚ diagSub = prod.diag
ext i x
case a.h.fz
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x

case a.h.fs
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
case a.h
n✝ n : ℕ
α : TypeVec n
i : Fin2 n
x : α i
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) i x = prod.diag i x
induction' i with _ _ _ i_ih
case a.h.fs
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
case a.h.fz
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) Fin2.fz x = prod.diag Fin2.fz x

case a.h.fs
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
simp [prod.diag, diagSub, repeatEq, subtypeVal, comp]
no goals
case a.h.fs
n✝¹ n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} (x : α a✝), (subtypeVal (repeatEq α) ⊚ diagSub) a✝ x = prod.diag a✝ x
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ (subtypeVal (repeatEq α) ⊚ diagSub) (Fin2.fs a✝) x = prod.diag (Fin2.fs a✝) x
apply @i_ih (drop α)