-- 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 φ.op (s Y₂)

Tactic:
rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]

Result:
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₁)

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₁
⊢ ∀ ⦃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₂)

Tactic:
rintro Z φ ⟨i, ⟨g⟩⟩

Result:
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 φ.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) ⋯
X : C
i : I
f : X ⟶ Y i
⊢ s X = F.map f.op (x i)

Tactic:
have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
    (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩

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

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

Tactic:
intro y₁ y₂ hy₁ hy₂

Result:
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₂

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, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i

Tactic:
apply existsUnique_of_exists_of_unique

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

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

Tactic:
rw [hs 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) = F.map b.op (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) ⋯
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Tactic:
have hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = F.map f.op (x i) := fun {X} i f => by
  have h := Presieve.IsSheafFor.valid_glue (H _ (hY X))
      (hx.familyOfElements_isCompatible _) (𝟙 _) ⟨i, ⟨f⟩⟩
  simp only [op_id, F.map_id, types_id_apply] at h
  exact h.trans (hx.familyOfElements_apply _ _ _)

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