-- Mathlib/CategoryTheory/Generator/Sheaf.lean
lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) :
    IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i)))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g

Tactic:
refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => Presheaf.freeYoneda X (S i),
    ∀ (h : G_1 ⟶ (sheafToPresheaf J A).obj F), h ≫ (sheafToPresheaf J A).map f = h ≫ (sheafToPresheaf J A).map g

Proof state:
case intro.mk.a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (fun x =>
        match x with
        | (X, i) => Presheaf.freeYoneda X (S i))
      (X, i) ⟶
    (sheafToPresheaf J A).obj F
⊢ ((sheafificationAdjunction J A).homEquiv
          ((fun x =>
              match x with
              | (X, i) => Presheaf.freeYoneda X (S i))
            (X, i))
          G).symm
      (a ≫ (sheafToPresheaf J A).map f) =
    ((sheafificationAdjunction J A).homEquiv
          ((fun x =>
              match x with
              | (X, i) => Presheaf.freeYoneda X (S i))
            (X, i))
          G).symm
      (a ≫ (sheafToPresheaf J A).map g)

Tactic:
simpa only [← Adjunction.homEquiv_naturality_right_symm] using
  hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
⊢ IsSeparating
    (Set.range fun x =>
      match x with
      | (X, i) => freeYoneda J X (S i))

Tactic:
intro F G f g hfg

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g

Proof state:
case intro.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (fun x =>
        match x with
        | (X, i) => Presheaf.freeYoneda X (S i))
      (X, i) ⟶
    (sheafToPresheaf J A).obj F
⊢ a ≫ (sheafToPresheaf J A).map f = a ≫ (sheafToPresheaf J A).map g

Tactic:
apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective

Result:
case intro.mk.a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (fun x =>
        match x with
        | (X, i) => Presheaf.freeYoneda X (S i))
      (X, i) ⟶
    (sheafToPresheaf J A).obj F
⊢ ((sheafificationAdjunction J A).homEquiv
          ((fun x =>
              match x with
              | (X, i) => Presheaf.freeYoneda X (S i))
            (X, i))
          G).symm
      (a ≫ (sheafToPresheaf J A).map f) =
    ((sheafificationAdjunction J A).homEquiv
          ((fun x =>
              match x with
              | (X, i) => Presheaf.freeYoneda X (S i))
            (X, i))
          G).symm
      (a ≫ (sheafToPresheaf J A).map g)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => Presheaf.freeYoneda X (S i),
    ∀ (h : G_1 ⟶ (sheafToPresheaf J A).obj F), h ≫ (sheafToPresheaf J A).map f = h ≫ (sheafToPresheaf J A).map g

Tactic:
rintro _ ⟨⟨X, i⟩, rfl⟩ a

Result:
case intro.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda J X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (fun x =>
        match x with
        | (X, i) => Presheaf.freeYoneda X (S i))
      (X, i) ⟶
    (sheafToPresheaf J A).obj F
⊢ a ≫ (sheafToPresheaf J A).map f = a ≫ (sheafToPresheaf J A).map g