case h.e'_5
C : Type u_5
inst✝⁴ : Category C
D : Type u_3
inst✝³ : Category D
E : Type ?u.139299
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft (Functor.op G) α.val)
⊢ α = (sheafIso H (asIso (whiskerLeft (Functor.op G) α.val))).hom
C : Type u_5
inst✝⁴ : Category C
D : Type u_3
inst✝³ : Category D
E : Type ?u.139299
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft (Functor.op G) α.val)
⊢ IsIso α
convert IsIso.of_iso (sheafIso H (asIso (whiskerLeft G.op α.val))) using 1
case h.e'_5.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_3
inst✝³ : Category D
E : Type ?u.139299
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft (Functor.op G) α.val)
⊢ α.val = (sheafIso H (asIso (whiskerLeft (Functor.op G) α.val))).hom.val
case h.e'_5
C : Type u_5
inst✝⁴ : Category C
D : Type u_3
inst✝³ : Category D
E : Type ?u.139299
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft (Functor.op G) α.val)
⊢ α = (sheafIso H (asIso (whiskerLeft (Functor.op G) α.val))).hom
ext1
no goals
case h.e'_5.h
C : Type u_5
inst✝⁴ : Category C
D : Type u_3
inst✝³ : Category D
E : Type ?u.139299
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (whiskerLeft (Functor.op G) α.val)
⊢ α.val = (sheafIso H (asIso (whiskerLeft (Functor.op G) α.val))).hom.val
apply (sheafHom_eq H _).symm