-- Mathlib/CategoryTheory/Sites/Subsheaf.lean
theorem Subpresheaf.to_sheafifyLift (f : G.toPresheaf ⟶ F') (h : Presieve.IsSheaf J F') :
    Subpresheaf.homOfLe (G.le_sheafify J) ≫ G.sheafifyLift f h = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
⊢ homOfLe ⋯ ≫ G.sheafifyLift f h = f

Tactic:
ext U s

Result:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
⊢ (homOfLe ⋯ ≫ G.sheafifyLift f h).app U s = f.app U s

Proof state:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows i
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toPresheaf.obj X), f.app Y (G.toPresheaf.map f_1 x) = F'.map f_1 (f.app X x)
⊢ F'.map i.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map i.op (f.app U s)

Tactic:
exact (Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : G ≤ sheafify J G)).app U s).2)
  ((G.family_of_elements_compatible _).compPresheafMap _) _ hi).trans (this _ _)

Result:
no goals

Proof state:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
⊢ (homOfLe ⋯ ≫ G.sheafifyLift f h).app U s = f.app U s

Tactic:
apply (h _ ((Subpresheaf.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext

Result:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
    (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows f_1 →
      F'.map f_1.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map f_1.op (f.app U s)

Proof state:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
    (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows f_1 →
      F'.map f_1.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map f_1.op (f.app U s)

Tactic:
intro V i hi

Result:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows i
⊢ F'.map i.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map i.op (f.app U s)

Proof state:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows i
⊢ F'.map i.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map i.op (f.app U s)

Tactic:
have := elementwise_of% f.naturality

Result:
case w.h.h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : G.toPresheaf ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toPresheaf.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((homOfLe ⋯).app U s)).arrows i
this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toPresheaf.obj X), f.app Y (G.toPresheaf.map f_1 x) = F'.map f_1 (f.app X x)
⊢ F'.map i.op ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U s) = F'.map i.op (f.app U s)