C : Type u
inst✝ : Category C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : Functor.op (inducedFunctor B) ⋙ F ⟶ Functor.op (inducedFunctor B) ⋙ F'.val
i : ι
⊢ (↑(restrictHomEquivHom F F' h) α).app (B i).op =
    (Equiv.invFun (restrictHomEquivHom F F' h) (Equiv.toFun (restrictHomEquivHom F F' h) α)).app i.op
C : Type u
inst✝ : Category C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : Functor.op (inducedFunctor B) ⋙ F ⟶ Functor.op (inducedFunctor B) ⋙ F'.val
i : ι
⊢ (↑(restrictHomEquivHom F F' h) α).app (B i).op = α.app i.op
nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]
no goals
C : Type u
inst✝ : Category C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : Functor.op (inducedFunctor B) ⋙ F ⟶ Functor.op (inducedFunctor B) ⋙ F'.val
i : ι
⊢ (↑(restrictHomEquivHom F F' h) α).app (B i).op =
    (Equiv.invFun (restrictHomEquivHom F F' h) (Equiv.toFun (restrictHomEquivHom F F' h) α)).app i.op
rfl