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