-- 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:
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
i : I
⊢ F.map (𝟙 (Y i)).op (x i) = x i

Tactic:
simp

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 : ⋯.amalgamate (x.familyOfElements X) ⋯ = x.familyOfElements X (𝟙 X) ⋯
⊢ s X = F.map f.op (x i)

Tactic:
exact h.trans (hx.familyOfElements_apply _ _ _)

Result:
no goals

Proof state:
case hex
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)
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Tactic:
have hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (_ : W ⟶ Y i), F.map a.op (s X) = s W := by
  intro W X a i b
  rw [hs i b]
  exact (Presieve.IsSheafFor.valid_glue (H _ (hY X))
    (hx.familyOfElements_isCompatible _) a ⟨i, ⟨b⟩⟩).trans (familyOfElements_apply hx _ _ _)

Result:
case hex
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
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Proof state:
case hex
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
⊢ (fun X => s (Opposite.unop X)) ∈ F.sections

Tactic:
rintro ⟨Y₁⟩ ⟨Y₂⟩ ⟨f : Y₂ ⟶ 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 (Opposite.op f) ((fun X => s (Opposite.unop X)) (Opposite.op Y₁)) =
    (fun X => s (Opposite.unop X)) (Opposite.op 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
⊢ ∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i

Tactic:
have H := (isSheaf_iff_isSheaf_of_type _ _).1 hF

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, ∀ (i : I), ↑s (Opposite.op (Y i)) = 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
y₁ y₂ : ↑F.sections
hy₁ : ∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i
i : I
⊢ ↑y₁ (Opposite.op (Y i)) = ↑y₂ (Opposite.op (Y i))

Tactic:
rw [hy₁, hy₂]

Result:
no goals

Proof state:
case hunique
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
y₁ y₂ : ↑F.sections
hy₁ : ∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i
⊢ y₁ = y₂

Tactic:
exact hY.sections_ext ⟨F, hF⟩ (fun i => by rw [hy₁, hy₂])

Result:
no goals

Proof state:
case hex
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
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Tactic:
let s := fun (X : C) => (H _ (hY X)).amalgamate _
  (hx.familyOfElements_isCompatible X)

Result:
case hex
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_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Proof state:
case hex
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
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Tactic:
refine ⟨⟨fun X => s X.unop, ?_⟩, fun i => (hs i (𝟙 (Y i))).trans (by simp)⟩

Result:
case hex
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
⊢ (fun X => s (Opposite.unop X)) ∈ F.sections