-- Mathlib/CategoryTheory/Sites/CoversTop.lean
lemma existsUnique_section (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : IsSheaf J F) :
    ∃! (s : F.sections), ∀ (i : I), s.1 (Opposite.op (Y i)) = x i

Proof state:
case hex.op.op.op.intro.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I), (W ⟶ Y i) → F.map a.op (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ F.map φ.op (F.map f.op (s Y₁)) = (F.map f.op ≫ F.map φ.op) (s Y₁)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
h : F.map (𝟙 X).op (⋯.amalgamate (x.familyOfElements X) ⋯) = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = F.map f.op (x i)

Tactic:
simp only [op_id, F.map_id, types_id_apply] at h

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
X : C
i : I
f : X ⟶ Y i
h : ⋯.amalgamate (x.familyOfElements X) ⋯ = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = F.map f.op (x i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
⊢ ∀ {W X : C} (a : W ⟶ X) (i : I), (W ⟶ Y i) → F.map a.op (s X) = s W

Tactic:
intro W X a i b

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
W X : C
a : W ⟶ X
i : I
b : W ⟶ Y i
⊢ F.map a.op (s X) = s W

Proof state:
case hex.op.op.op
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I), (W ⟶ Y i) → F.map a.op (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ F.map (Opposite.op f) ((fun X => s (Opposite.unop X)) (Opposite.op Y₁)) =
    (fun X => s (Opposite.unop X)) (Opposite.op Y₂)

Tactic:
change F.map f.op (s Y₁) = s Y₂

Result:
case hex.op.op.op
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I), (W ⟶ Y i) → F.map a.op (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ F.map f.op (s Y₁) = s Y₂

Proof state:
case hex.op.op.op
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I), (W ⟶ Y i) → F.map a.op (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ F.map f.op (s Y₁) = s Y₂

Tactic:
apply (Presieve.isSeparated_of_isSheaf J F H _ (hY Y₂)).ext

Result:
case hex.op.op.op
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I), (W ⟶ Y i) → F.map a.op (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y₂⦄,
    (Sieve.ofObjects Y Y₂).arrows f_1 → F.map f_1.op (F.map f.op (s Y₁)) = F.map f_1.op (s Y₂)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X => ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i)
W X : C
a : W ⟶ X
i : I
b : W ⟶ Y i
⊢ F.map a.op (s X) = F.map b.op (x i)

Tactic:
exact (Presieve.IsSheafFor.valid_glue (H _ (hY X))
  (hx.familyOfElements_isCompatible _) a ⟨i, ⟨b⟩⟩).trans (familyOfElements_apply hx _ _ _)

Result:
no goals