-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem naturality_apply [G.IsLocallyFull K] {X Y : C} (i : G.obj X ⟶ G.obj Y) (x) :
    ℱ'.1.map i.op (α.app _ x) = α.app _ (ℱ.map i.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 Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (G.op ⋙ ℱ).obj (op Y)),
    ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)
V : C
iVX : V ⟶ X
iVY : V ⟶ Y
e : G.map iVY = G.map iVX ≫ i
⊢ ℱ'.val.map (G.map iVX).op (ℱ'.val.map i.op (α.app (op Y) x)) = ℱ'.val.map (G.map iVX).op (α.app (op X) (ℱ.map i.op x))

Tactic:
simp only [comp_obj, types_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← e, this]

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✝ Y✝ : C
i✝ : G.obj X✝ ⟶ G.obj Y✝
x✝ : (G.op ⋙ ℱ).obj (op Y✝)
X Y : C
i : X ⟶ Y
x : (G.op ⋙ ℱ).obj (op Y)
⊢ ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)

Tactic:
exact congr_fun (α.naturality i.op).symm x

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 Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (G.op ⋙ ℱ).obj (op Y)),
    ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)
⊢ ℱ'.val.map i.op (α.app (op Y) x) = α.app (op X) (ℱ.map i.op x)

Tactic:
refine IsLocallyFull.ext G _ i fun V iVX iVY e ↦ ?_

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 Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (G.op ⋙ ℱ).obj (op Y)),
    ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)
V : C
iVX : V ⟶ X
iVY : V ⟶ Y
e : G.map iVY = G.map iVX ≫ i
⊢ ℱ'.val.map (G.map iVX).op (ℱ'.val.map i.op (α.app (op Y) x)) = ℱ'.val.map (G.map iVX).op (α.app (op X) (ℱ.map i.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 Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
⊢ ℱ'.val.map i.op (α.app (op Y) x) = α.app (op X) (ℱ.map i.op x)

Tactic:
have {X Y} (i : X ⟶ Y) (x) :
    ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
  exact congr_fun (α.naturality i.op).symm x

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 Y : C
i : G.obj X ⟶ G.obj Y
x : (G.op ⋙ ℱ).obj (op Y)
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (G.op ⋙ ℱ).obj (op Y)),
    ℱ'.val.map (G.map i).op (α.app (op Y) x) = α.app (op X) (ℱ.map (G.map i).op x)
⊢ ℱ'.val.map i.op (α.app (op Y) x) = α.app (op X) (ℱ.map i.op x)