C : Type u_4
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
E : Type ?u.63453
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.63505
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : Functor.op G ⋙ ℱ ⟶ Functor.op G ⋙ ℱ'.val
X : D
Y : C
f : X.op ⟶ (G.obj Y).op
x : ℱ.obj X.op
⊢ pushforwardFamily α x f.unop (_ : coverByImage G X.op.unop f.unop) = α.app Y.op (ℱ.map f x)
C : Type u_4
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
E : Type ?u.63453
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.63505
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : Functor.op G ⋙ ℱ ⟶ Functor.op G ⋙ ℱ'.val
X : D
Y : C
f : X.op ⟶ (G.obj Y).op
x : ℱ.obj X.op
⊢ ℱ'.val.map f (appHom H α X x) = α.app Y.op (ℱ.map f x)
refine'
  ((ℱ'.cond _ (H.is_cover X)).valid_glue (pushforwardFamily_compatible H α x) f.unop
        (Presieve.in_coverByImage G f.unop)).trans
    _
no goals
C : Type u_4
inst✝⁴ : Category C
D : Type u_2
inst✝³ : Category D
E : Type ?u.63453
inst✝² : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type ?u.63505
inst✝¹ : Category A
G : C ⥤ D
H : CoverDense K G
inst✝ : Full G
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : SheafOfTypes K
α : Functor.op G ⋙ ℱ ⟶ Functor.op G ⋙ ℱ'.val
X : D
Y : C
f : X.op ⟶ (G.obj Y).op
x : ℱ.obj X.op
⊢ pushforwardFamily α x f.unop (_ : coverByImage G X.op.unop f.unop) = α.app Y.op (ℱ.map f x)
apply pushforwardFamily_apply