mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
⊢ ∀ [inst : Mono f] [inst_1 : Mono g] (i : P ≅ Q),
    i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op

Tactic:
hf

Goal state after:
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
⊢ ∀ [inst : Mono g] (i : P ≅ Q), i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
i : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (Hom.id i) ≫
      WalkingParallelFamily.casesOn i ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (Hom.id i)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
i : WalkingParallelFamily J
⊢ (parallelFamily f).map (Hom.id i) ≫ WalkingParallelFamily.casesOn i (f (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn i (f (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map (Hom.id i)

Tactic:
simp

Goal state after:
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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ (Subobject.mk f.unop.left.op).arrow).unop ≫ (unop P).hom = A.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsSeparating
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ ∀ (G : C), ⊥ G → ∀ (h : G ⟶ x✝³), h ≫ x✝¹ = h ≫ x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsCoseparating
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ ∀ (G : C), ⊥ G → ∀ (h : x✝² ⟶ G), x✝¹ ≫ h = x✝ ≫ h

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsDetecting
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ∀ (G : C), ⊥ G → ∀ (h : G ⟶ Y✝), ∃! h', h' ≫ f = h

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : ⊥.IsCodetecting
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ∀ (G : C), ⊥ G → ∀ (h : X✝ ⟶ G), ∃! h', f ≫ h' = h

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

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

Tactic:
← s.app_one (Classical.arbitrary J),

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ k = (f (Classical.arbitrary J) ≫ s.ι.app one) ≫ l
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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
⊢ ∀ [inst : 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),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f

Tactic:
hf

Goal state after:
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),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Trident f
ht : IsLimit t
Z : C
k : Z ⟶ t.pt
⊢ ∀ (j₁ j₂ : J), (k ≫ t.ι) ≫ f j₁ = (k ≫ t.ι) ≫ f j₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Cotrident f
ht : IsColimit t
Z : C
k : t.pt ⟶ Z
⊢ ∀ (j₁ j₂ : J), f j₁ ≫ t.π ≫ k = f j₂ ≫ t.π ≫ k

Tactic:
simp

Goal state after:
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 [← Category.assoc, ← S.map_comp] using hq

Goal state after:
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
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
⊢ ((isoMk (Subobject.underlyingIso f.unop.left.op).unop ⋯).op.hom ≫ f).unop =
    (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq).op.unop

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
⊢ HasInitial C

Tactic:
have := hasFiniteLimits_of_hasLimitsOfSize C

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this : HasFiniteLimits C
⊢ HasInitial C
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
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
⊢ ∀ [inst : Mono f] [inst_1 : Mono g],
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g

Tactic:
hf

Goal state after:
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
⊢ ∀ [inst : Mono g],
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝¹ : HasWideEqualizer f
inst✝ : Nonempty J
W : C
k : W ⟶ X
h : ∀ (j₁ j₂ : J), k ≫ f j₁ = k ≫ f j₂
⊢ lift k h ≫ ι f = k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝¹ : HasWideCoequalizer f
inst✝ : Nonempty J
W : C
k : Y ⟶ W
h : ∀ (j₁ j₂ : J), f j₁ ≫ k = f j₂ ≫ k
⊢ π f ≫ desc k h = k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
⊢ ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, (fun x ↦ (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h

Tactic:
intro B h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ ∃ i g, (fun x ↦ (Adjunction.ofIsRightAdjoint G).unit.app A) i ≫ G.map g = h
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx : (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) = 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
← map_zero (colimit.ι S.X₃ j).hom

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ j)) y ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f g : Subobject.underlying.obj ⊥ ⟶ A
b✝ : Subtype P
⊢ ((⊥.ofLEMk (equalizer.ι f g ≫ ⊥.arrow) ⋯ ≫ equalizer.ι f g) ≫ ⊥.arrow) ≫ Pi.π Subtype.val b✝ =
    (𝟙 (Subobject.underlying.obj ⊥) ≫ ⊥.arrow) ≫ Pi.π Subtype.val b✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ inv (P.ofLE Q h₁) ≫ P.arrow = Q.arrow

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : IsSeparator G
α : C ≌ D
⊢ IsSeparator (α.functor.obj G)

Tactic:
simpa using! ObjectProperty.IsSeparating.of_equivalence h α

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : G_1 ⟶ x✝⁴), h ≫ x✝² = h ≫ x✝¹
x✝ : G ⟶ x✝⁴
⊢ ObjectProperty.singleton G G

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
x✝⁴ x✝³ : C
x✝² x✝¹ : x✝⁴ ⟶ x✝³
hfg : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : x✝³ ⟶ G_1), x✝² ≫ h = x✝¹ ≫ h
x✝ : x✝³ ⟶ G
⊢ ObjectProperty.singleton G G

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h) → IsIso f
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
hf : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : G_1 ⟶ x✝²), ∃! h', h' ≫ x✝¹ = h
x✝ : G ⟶ x✝²
⊢ ObjectProperty.singleton G G

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : X ⟶ G), ∃! h', f ≫ h' = h) → IsIso f
x✝³ x✝² : C
x✝¹ : x✝³ ⟶ x✝²
hf : ∀ (G_1 : C), ObjectProperty.singleton G G_1 → ∀ (h : x✝³ ⟶ G_1), ∃! h', x✝¹ ≫ h' = h
x✝ : x✝³ ⟶ G
⊢ ObjectProperty.singleton G G

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
h : IsSeparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : c.pt ⟶ X
b : Discrete β
⊢ ObjectProperty.ofObj f (f b.as)

Tactic:
simp

Goal state after:
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
g : (i : J) → ↑(X.obj { as := i })
j : J
⊢ (ConcreteCategory.hom (f.app { as := j })) (g j) =
    (ConcreteCategory.hom
        (limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
            { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
              π :=
                Discrete.natTrans fun j ↦
                  AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) } ≫
          limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)) ≫ limit.π Y { as := j }))
      g

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hG : IsSeparator G
⊢ ObjectProperty.singleton G ≤ ObjectProperty.pair G H

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hH : IsSeparator H
⊢ ObjectProperty.singleton H ≤ ObjectProperty.pair G H

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
b : β
hb : IsSeparator (f b)
⊢ ObjectProperty.singleton (f b) ≤ ObjectProperty.ofObj f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Fan f
hc : IsLimit c
h : IsCoseparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ c.pt
b : Discrete β
⊢ ObjectProperty.ofObj f (f b.as)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hG : IsCoseparator G
⊢ ObjectProperty.singleton G ≤ ObjectProperty.pair G H

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hH : IsCoseparator H
⊢ ObjectProperty.singleton H ≤ ObjectProperty.pair G H

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
b : β
hb : IsCoseparator (f b)
⊢ ObjectProperty.singleton (f b) ≤ ObjectProperty.ofObj f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
i : I
⊢ c.ι.app i ≫
      (hc.coconePointUniqueUpToIso isc).hom ≫
        (colimit
            ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
              CostructuredArrow.toOver yoneda c.pt)).hom =
    c.ι.app i ≫ (Over.mk (𝟙 c.pt)).hom

Tactic:
simp

Goal state after:
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
x : F i
⊢ (equivOfIsColimit hc) ((equivOfIsColimit hc).symm (c.inj i x)) = (equivOfIsColimit hc) ⟨i, x⟩

Tactic:
simp

Goal state after:
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
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ιColimitType (op (F.elementsMk X x))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    x

Tactic:
simp

Goal state after:
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
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).map f ≫
            (coconeπOpCompShrinkYonedaObj F Y).ι.app u)).toFun
      (shrinkYonedaObjObjEquiv.symm x) =
    (ConcreteCategory.hom
          ((coconeπOpCompShrinkYonedaObj F X).ι.app u ≫ (((const F.Elementsᵒᵖ).obj F).obj u).map f)).toFun
      (shrinkYonedaObjObjEquiv.symm x)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' Set.range Sum.inl =
    ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) '' (Set.range Sum.inr)ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := left }
⊢ (ConcreteCategory.hom
          (c.inl ≫
            ↾fun x ↦
              if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
                (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
              else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))).toFun
      x =
    (ConcreteCategory.hom f).toFun x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul ((z₁ + z₂) • au) = Additive.toMul (z₁ • au + z₂ • au)

Tactic:
dsimp only [ZMod.smul_units_def, toMul_nsmul, toMul_add]

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ + z₂).val = Additive.toMul au ^ z₁.val * Additive.toMul au ^ z₂.val
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: 𝕜 : Type ?u.3
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
q : 𝕜
⊢ q / ↑0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
⊢ (match n with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      n =
    a

Tactic:
cases n
    · rw [Int.ofNat_eq_natCast, Nat.cast_ne_zero] at hn
      simp [RootableBy.root_cancel _ hn]
    · simp [RootableBy.root_cancel _ (Nat.add_one_ne_zero _)]

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
hl : ∀ f ∈ [], Periodic f c
⊢ Periodic [].prod c

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
⊢ f m = ↑(LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) ⋯) ⟨i m, ⋯⟩

Tactic:
refine Eq.trans (hnonempty.some.is_extension m) ?_
      symm
      generalize_proofs _ _ h1
      exact
        LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
          ((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f x = (-1) ^ (2 * k) • f x

Tactic:
simp

Goal state after: