-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem pushforwardFamily_apply [G.IsLocallyFull K]
    {X} (x : ℱ.obj (op X)) {Y : C} (f : G.obj Y ⟶ X) :
    pushforwardFamily α x f (Presieve.in_coverByImage G f) = α.app (op Y) (ℱ.map f.op x)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ'.val.map (Nonempty.some ⋯).lift.op (α.app (op (Nonempty.some ⋯).1) (ℱ.map (Nonempty.some ⋯).map.op x)) =
    α.app (op Y) (ℱ.map f.op x)

Tactic:
generalize Nonempty.some (Presieve.in_coverByImage G f) = l

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
l : CoverByImageStructure G f
⊢ ℱ'.val.map l.lift.op (α.app (op l.1) (ℱ.map l.map.op x)) = α.app (op Y) (ℱ.map f.op x)

Proof state:
case mk
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y W : C
iYW : G.obj Y ⟶ G.obj W
iWX : G.obj W ⟶ X
⊢ ℱ'.val.map { obj := W, lift := iYW, map := iWX, fac := ⋯ }.lift.op
      (α.app (op { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1)
        (ℱ.map { obj := W, lift := iYW, map := iWX, fac := ⋯ }.map.op x)) =
    α.app (op Y) (ℱ.map (iYW ≫ iWX).op x)

Tactic:
simp only [← op_comp, ← FunctorToTypes.map_comp_apply, naturality_apply]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
l : CoverByImageStructure G f
⊢ ℱ'.val.map l.lift.op (α.app (op l.1) (ℱ.map l.map.op x)) = α.app (op Y) (ℱ.map f.op x)

Tactic:
obtain ⟨W, iYW, iWX, rfl⟩ := l

Result:
case mk
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y W : C
iYW : G.obj Y ⟶ G.obj W
iWX : G.obj W ⟶ X
⊢ ℱ'.val.map { obj := W, lift := iYW, map := iWX, fac := ⋯ }.lift.op
      (α.app (op { obj := W, lift := iYW, map := iWX, fac := ⋯ }.1)
        (ℱ.map { obj := W, lift := iYW, map := iWX, fac := ⋯ }.map.op x)) =
    α.app (op Y) (ℱ.map (iYW ≫ iWX).op x)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ pushforwardFamily α x f ⋯ = α.app (op Y) (ℱ.map f.op x)

Tactic:
simp only [pushforwardFamily_def, op_obj]

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
D : Type u_2
inst✝¹ : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ ℱ'.val.map (Nonempty.some ⋯).lift.op (α.app (op (Nonempty.some ⋯).1) (ℱ.map (Nonempty.some ⋯).map.op x)) =
    α.app (op Y) (ℱ.map f.op x)