-- Mathlib/CategoryTheory/Generator/HomologicalComplex.lean
lemma isSeparating_separatingFamily :
    IsSeparating (Set.range (separatingFamily c X))

Proof state:
case h.a
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
⊢ ∀ G ∈ Set.range X, ∀ (h : G ⟶ K.X j), h ≫ f.f j = h ≫ g.f j

Tactic:
rintro _ ⟨a, rfl⟩ p

Result:
case h.a.intro
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
⊢ p ≫ f.f j = p ≫ g.f j

Proof state:
case h.a.intro
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ p ≫ f.f j = p ≫ g.f j

Tactic:
apply H.homEquiv.symm.injective

Result:
case h.a.intro.a
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ H.homEquiv.symm (p ≫ f.f j) = H.homEquiv.symm (p ≫ g.f j)

Proof state:
case h.a.intro
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
⊢ p ≫ f.f j = p ≫ g.f j

Tactic:
have H := evalCompCoyonedaCorepresentable c (X a) j

Result:
case h.a.intro
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ p ≫ f.f j = p ≫ g.f j

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
⊢ f = g

Tactic:
ext j

Result:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
⊢ f.f j = g.f j

Proof state:
case h.a.intro.a
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).CorepresentableBy (evalCompCoyonedaCorepresentative c (X a) j)
⊢ H.homEquiv.symm (p ≫ f.f j) = H.homEquiv.symm (p ≫ g.f j)

Tactic:
simpa only [H.homEquiv_symm_comp] using h _ ⟨⟨a, j⟩, rfl⟩ (H.homEquiv.symm p)

Result:
no goals

Proof state:
case h
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
⊢ f.f j = g.f j

Tactic:
apply hX

Result:
case h.a
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
⊢ ∀ G ∈ Set.range X, ∀ (h : G ⟶ K.X j), h ≫ f.f j = h ≫ g.f j

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
⊢ IsSeparating (Set.range (separatingFamily c X))

Tactic:
intro K L f g h

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type w
inst✝³ : DecidableEq ι
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : IsSeparating (Set.range X)
K L : HomologicalComplex C c
f g : K ⟶ L
h : ∀ G ∈ Set.range (separatingFamily c X), ∀ (h : G ⟶ K), h ≫ f = h ≫ g
⊢ f = g