mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
· refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op
    refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩
    exact Quiver.Hom.unop_inj (by simpa only using! hy)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
· refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)
    obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op
    refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩
    exact Quiver.Hom.unop_inj (by simpa only using! hy)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : HasCoequalizers C
⊢ P.IsCodetecting → P.IsCoseparating

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : HasCoequalizers C
⊢ P.op.IsDetecting → P.op.IsSeparating
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
x✝⁴ : Mono f
x✝³ : C
x✝² : P x✝³
x✝¹ x✝ : x✝³ ⟶ X
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
x✝⁴ : Mono f
x✝³ : C
x✝² : P x✝³
x✝¹ x✝ : x✝³ ⟶ X
h : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : C
f : X ⟶ Y
x✝⁴ : Epi f
x✝³ : C
x✝² : P x✝³
x✝¹ x✝ : Y ⟶ x✝³
h : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : C
f : X ⟶ Y
x✝⁴ : Epi f
x✝³ : C
x✝² : P x✝³
x✝¹ x✝ : Y ⟶ x✝³
h : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
⊢ P.IsCoseparating → P.IsCodetecting

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
⊢ P.op.IsSeparating → P.op.IsDetecting
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ X
h✝ : Epi p
i : ι
⊢ c.inj i ≫ p ≫ f = c.inj i ≫ p ≫ g

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan s
hc : IsColimit c
p : c.pt ⟶ X
h✝ : Epi p
i : ι
⊢ c.inj i ≫ p ≫ f = c.inj i ≫ p ≫ g
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case i.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ S.map f.unop.left ≫ S.map (Subobject.underlyingIso f.unop.left.op).unop.hom ≫ (mk q).hom =
    S.map f.unop.left ≫ (unop P).hom

Tactic:
simpa using

Goal state after:
case i.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ S.map (Subobject.mk f.unop.left.op).arrow.unop ≫ q = A.hom
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan s
hc : IsLimit c
j : Y ⟶ c.pt
h✝ : Mono j
i : ι
⊢ (f ≫ j) ≫ c.proj i = (g ≫ j) ≫ c.proj i

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan s
hc : IsLimit c
j : Y ⟶ c.pt
h✝ : Mono j
i : ι
⊢ f ≫ j ≫ c.proj i = g ≫ j ≫ c.proj i
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
conv_lhs =>
    congr
    rw [← Quiver.Hom.unop_op g.unop.left]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X : C
inst✝ : HasCoproduct (P.coproductFromFamily X)
Z✝ : C
u v : X ⟶ Z✝
huv : P.coproductFrom X ≫ u = P.coproductFrom X ≫ v
G : C
hG : P G
h : G ⟶ X
⊢ h ≫ u = h ≫ v

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X : C
inst✝ : HasCoproduct (P.coproductFromFamily X)
Z✝ : C
u v : X ⟶ Z✝
huv : P.coproductFrom X ≫ u = P.coproductFrom X ≫ v
G : C
hG : P G
h : G ⟶ X
⊢ h ≫ u = h ≫ v
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X : C
inst✝ : HasProduct (P.productToFamily X)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ P.productTo X = v ≫ P.productTo X
G : C
hG : P G
h : X ⟶ G
⊢ u ≫ h = v ≫ h

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X : C
inst✝ : HasProduct (P.productToFamily X)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ P.productTo X = v ≫ P.productTo X
G : C
hG : P G
h : X ⟶ G
⊢ u ≫ h = v ≫ h
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one

Tactic:
simpa using

Goal state after:
case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app zero ≫ k = t.ι.app zero

Tactic:
simpa using

Goal state after:
case zero
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app zero ≫ k = t.ι.app zero
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app zero ≫ k = t.ι.app zero

pp: case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one

Tactic:
· simpa using f (Classical.arbitrary J) ≫= w

Goal state after:
case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ s.ι.app one ≫ k = t.ι.app one
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
this : (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop
⊢ ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op).unop =
    (MonoOver.mk f).arrow.unop.left.op.unop

Tactic:
simpa using

Goal state after:
case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
this : (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f g h).unop.left = f.unop.left
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
𝒢 : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v₁, u₁} 𝒢
inst✝ : LocallySmall.{w, v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h : (fun P ↦ {f | P.Factors f.snd}) P = (fun P ↦ {f | P.Factors f.snd}) Q
⊢ ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
𝒢 : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v₁, u₁} 𝒢
inst✝ : LocallySmall.{w, v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h : (fun P ↦ {f | P.Factors f.snd}) P = (fun P ↦ {f | P.Factors f.snd}) Q
⊢ ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
⊢ IsSeparator G ↔ ∀ (A : C), Epi (Sigma.desc fun f ↦ f)

Tactic:
isSeparator_def

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔ ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
A Z✝ : C
u v : A ⟶ Z✝
huv : (Sigma.desc fun f ↦ f) ≫ u = (Sigma.desc fun f ↦ f) ≫ v
i : G ⟶ A
⊢ i ≫ u = i ≫ v

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
A Z✝ : C
u v : A ⟶ Z✝
huv : (Sigma.desc fun f ↦ f) ≫ u = (Sigma.desc fun f ↦ f) ≫ v
i : G ⟶ A
⊢ i ≫ u = i ≫ v
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f ↦ f)
j : Discrete (G ⟶ X)
⊢ colimit.ι (Discrete.functor fun f ↦ G) j ≫ (Sigma.desc fun f ↦ f) ≫ f =
    colimit.ι (Discrete.functor fun f ↦ G) j ≫ (Sigma.desc fun f ↦ f) ≫ g

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f ↦ f)
j : Discrete (G ⟶ X)
⊢ j.as ≫ f = j.as ≫ g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z✝ : C
u v : Z✝ ⟶ A
huv : (u ≫ Pi.lift fun f ↦ f) = v ≫ Pi.lift fun f ↦ f
i : A ⟶ G
⊢ u ≫ i = v ≫ i

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z✝ : C
u v : Z✝ ⟶ A
huv : (u ≫ Pi.lift fun f ↦ f) = v ≫ Pi.lift fun f ↦ f
i : A ⟶ G
⊢ u ≫ i = v ≫ i
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f ↦ f)
j : Discrete (Y ⟶ G)
⊢ (f ≫ Pi.lift fun f ↦ f) ≫ limit.π (Discrete.functor fun f ↦ G) j =
    (g ≫ Pi.lift fun f ↦ f) ≫ limit.π (Discrete.functor fun f ↦ G) j

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f ↦ f)
j : Discrete (Y ⟶ G)
⊢ f ≫ j.as = g ≫ j.as
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
⊢ IsSeparator c.pt

Tactic:
isSeparator_def

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : c.pt ⟶ X), h ≫ f_1 = h ≫ g) → f_1 = g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : c.pt ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝
b : β
g : f b ⟶ x✝³
⊢ g ≫ x✝¹ = g ≫ x✝

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsSeparating
c : Cofan f
hc : IsColimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : c.pt ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝
b : β
g : f b ⟶ x✝³
⊢ g ≫ x✝¹ = g ≫ x✝
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this✝ :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
this : Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv)
⊢ Epi (lim.map f)

Tactic:
simpa using

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this✝ :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
this : Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv)
⊢ Epi (limMap f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : x✝² ⟶ c.pt), x✝¹ ≫ h = x✝ ≫ h
b : β
g : x✝² ⟶ f b
⊢ x✝¹ ≫ g = x✝ ≫ g

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
huv : ∀ (h : x✝² ⟶ c.pt), x✝¹ ≫ h = x✝ ≫ h
b : β
g : x✝² ⟶ f b
⊢ x✝¹ ≫ g = x✝ ≫ g
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j

Tactic:
simpa using

Goal state after:
C : Type u
F : C → Type v
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : ((sigma F).inj x✝² x✝¹).fst = ((sigma F).inj x✝² x✝).fst ∧ ((sigma F).inj x✝² x✝¹).snd ≍ ((sigma F).inj x✝² x✝).snd
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : ((sigma F).inj x✝² x✝¹).fst = ((sigma F).inj x✝² x✝).fst ∧ ((sigma F).inj x✝² x✝¹).snd ≍ ((sigma F).inj x✝² x✝).snd
⊢ x✝¹ = x✝
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
h : c.inj i y₁ = c.inj i y₂
⊢ y₁ = y₂

Tactic:
simpa using

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
h : c.inj i y₁ = c.inj i y₂
⊢ y₁ = y₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j

Tactic:
simpa using

Goal state after:
C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective
        ⇑(ConcreteCategory.hom
            ((binaryCoproductCocone X Y).ι.app { as := right } ≫
              (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := right } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective ⇑(ConcreteCategory.hom c.inl) ∧
    Injective ⇑(ConcreteCategory.hom c.inr) ∧
      IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))

Tactic:
rw [← show _ = c.inl from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩,
        ← show _ = c.inr from
          h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ⇑(ConcreteCategory.hom
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
    Injective
        ⇑(ConcreteCategory.hom
            ((binaryCoproductCocone X Y).ι.app { as := right } ≫
              (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) ∧
      IsCompl
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := left } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
        (Set.range
          ⇑(ConcreteCategory.hom
              ((binaryCoproductCocone X Y).ι.app { as := right } ≫
                (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
this :
  (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
      (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
    colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))))

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
this :
  (coconeπOpCompShrinkYonedaObj F u.fst).ι.app (op u) ≫
      (shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst =
    colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 u.fst))