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

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

Tactic:
intro F G f g h

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

Proof state:
case w.h.op.intro.a
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ freeYonedaHomEquiv.symm (α ≫ f.app (op X)) = freeYonedaHomEquiv.symm (α ≫ g.app (op X))

Tactic:
simpa only [freeYonedaHomEquiv_symm_comp] using
  h _ ⟨⟨X, i⟩, rfl⟩ (freeYonedaHomEquiv.symm α)

Result:
no goals

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

Tactic:
ext ⟨X⟩

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

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

Tactic:
refine hS _ _ ?_

Result:
case w.h.op
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
⊢ ∀ G_1 ∈ Set.range S, ∀ (h : G_1 ⟶ F.obj (op X)), h ≫ f.app (op X) = h ≫ g.app (op X)

Proof state:
case w.h.op.intro
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ α ≫ f.app (op X) = α ≫ g.app (op X)

Tactic:
apply freeYonedaHomEquiv.symm.injective

Result:
case w.h.op.intro.a
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ freeYonedaHomEquiv.symm (α ≫ f.app (op X)) = freeYonedaHomEquiv.symm (α ≫ g.app (op X))

Proof state:
case w.h.op
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
⊢ ∀ G_1 ∈ Set.range S, ∀ (h : G_1 ⟶ F.obj (op X)), h ≫ f.app (op X) = h ≫ g.app (op X)

Tactic:
rintro _ ⟨i, rfl⟩ α

Result:
case w.h.op.intro
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
ι : Type w
S : ι → A
hS : IsSeparating (Set.range S)
F G : Cᵒᵖ ⥤ A
f g : F ⟶ G
h :
  ∀
    G_1 ∈
      Set.range fun x =>
        match x with
        | (X, i) => freeYoneda X (S i),
    ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ α ≫ f.app (op X) = α ≫ g.app (op X)