no goals
β : Type w
C : Type u
inst✝² : Category C
γ : Type v
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ↑ε)
b : β
⊢ ι f (↑ε b) ≫ (reindex ε f).inv = ι (f ∘ ↑ε) b
simp [Iso.comp_inv_eq]