Specify types of arrows

Stream: new members

[Gareth Ma]

import Mathlib.CategoryTheory.FintypeCat
open CategoryTheory Category Opposite Prod
local notation "𝟚" => Fin 2
def ι : (0 : 𝟚) ⟶ (1 : 𝟚) := homOfLE $ zero_le_one (α := ℕ)
universe u
variable {C : Type u} [Category C] {c c' : C}

theorem asdf : ( (c ⟶ c) × ((0 : 𝟚) ⟶ (1 : 𝟚)) ) = ( (c, (0 : 𝟚)) ⟶ (c, (1 : 𝟚)) ) := rfl
theorem qwer : ( (c ⟶ c') × ((1 : 𝟚) ⟶ (1 : 𝟚)) ) = ( (c, (1 : 𝟚)) ⟶ (c', (1 : 𝟚)) ) := rfl

example (f : c ⟶ c') :
    /-
    ((f, ι) : (c, (0 : 𝟚)) ⟶ (c', (1 : 𝟚)))
    =
    ((𝟙 c, ι) : (c, (0 : 𝟚)) ⟶ (c, (1 : 𝟚)))
    ≫
    ((f, 𝟙 1) : (c, (1 : 𝟚)) ⟶ (c', (1 : 𝟚)) := by
    -/
    (f, ι) = (cast asdf (𝟙 c, ι)) ≫ (cast qwer (f, 𝟙 1)) := by
  simp only [cast_eq]

I don't understand why the comment parts don't work - the things have wrong types. However hovering after the simp only call shows the types do work. How should I fix this?