mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).map f ≫ ↟(limitπLinearMap F x✝) =
    ↟(limitπLinearMap F x✝¹) ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
j : J
this : Small.{w, max v w}
  ↑((F ⋙ forget₂ (AlgCat R) RingCat ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections :=
  limitπAlgHom._proof_1 F
x : R
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (AlgCat R))).π.app j))
      ((algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) x) =
    (algebraMap R ((F ⋙ forget (AlgCat R)).obj j)) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
j : J
this : Small.{w, max v w}
  ↑((F ⋙ forget₂ (AlgCat R) RingCat ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections :=
  limitπAlgHom._proof_1 F
x : R
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (AlgCat R))).π.app j))
      ((algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) x) =
    (algebraMap R ((F ⋙ forget (AlgCat R)).obj j)) x

Tactic:
by
      simp only [Functor.comp_obj, Types.Small.limitCone_pt, Functor.const_obj_obj,
        Types.Small.limitCone_π_app, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk,
        ← Shrink.algEquiv_apply R, AlgEquiv.commutes]
      rfl

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).map f ≫ ofHom (limitπAlgHom F x✝) =
    ofHom (limitπAlgHom F x✝¹) ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
⊢ IsLimit (limitCone F)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
this : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
⊢ IsLimit c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i : ι
⊢ ↟(f i i ⋯) = 𝟙 (of R (G i))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ ↟(f X✝ Z✝ ⋯) = ↟(f X✝ Y✝ ⋯) ≫ ↟(f Y✝ Z✝ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
⊢ (directLimitDiagram G f).map hij ≫ ↟(DirectLimit.of R ι G f x✝) =
    ↟(DirectLimit.of R ι G f x✝¹) ≫ ((Functor.const ι).obj (of R (Module.DirectLimit G f))).map hij

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i j : ι
h : i ≤ j
x : G i
⊢ (Hom.hom (s.ι.app j)) ((f i j h) x) = (Hom.hom (s.ι.app i)) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i : ι
⊢ (directLimitCocone G f).ι.app i ≫ ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯) = s.ι.app i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
⊢ s.ι.app = fun i ↦ ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
⊢ m = ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
⊢ (bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫ { app := fun X₃ ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ } ≫ (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ } ≫ ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (bifunctorComp₁₂ F₁₂ G).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj Y₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
      (bifunctorComp₁₂ F₁₂ G').map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ (((bifunctorComp₁₂FunctorObj F₁₂).obj G).obj X₁).map f ≫
      { app := fun X₃ ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ } ≫
      (((bifunctorComp₁₂FunctorObj F₁₂').obj G).obj X₁).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
⊢ IsLimit (limitCone F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ ((bifunctorComp₁₂FunctorObj F₁₂).obj G).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
      ((bifunctorComp₁₂FunctorObj F₁₂').obj G).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget GrpCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget GrpCat).map f)) (a⁻¹ j) = a⁻¹ j'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ GrpCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
this : (forget₂ GrpCat MonCat).ReflectsIsomorphisms := reflectsIsomorphisms_forget₂ GrpCat MonCat
c' : Cone (F ⋙ forget₂ GrpCat MonCat)
t : IsLimit c'
⊢ Small.{u, max u v} ↑((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ C₃ ⥤ C₄
f : G ⟶ G'
⊢ (bifunctorComp₁₂FunctorObj F₁₂).map f ≫
      {
        app := fun X₁ ↦
          { app := fun X₂ ↦ { app := fun X₃ ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun X₁ ↦
          { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ },
        naturality := ⋯ } ≫
      (bifunctorComp₁₂FunctorObj F₁₂').map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ GrpCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
this✝¹ : (forget₂ GrpCat MonCat).ReflectsIsomorphisms := reflectsIsomorphisms_forget₂ GrpCat MonCat
c' : Cone (F ⋙ forget₂ GrpCat MonCat)
t : IsLimit c'
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
⊢ (forget₂ GrpCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget GrpCat)).pt,
        π := { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ GrpCat MonCat) j), naturality := ⋯ } } ≅
    c'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ✝ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
⊢ { obj := fun X₃ ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃), map := fun {X Y} φ ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ),
            map_id := ⋯, map_comp := ⋯ }.map
        φ ≫
      (F.obj X₁).map ((G₂₃.map φ✝).app Y₃) =
    (F.obj X₁).map ((G₂₃.map φ✝).app X₃) ≫
      { obj := fun X₃ ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃), map := fun {X Y} φ ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ),
            map_id := ⋯, map_comp := ⋯ }.map
        φ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ CreatesLimit F (forget GrpCat)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f : X₃ ⟶ Y₃
⊢ (((bifunctorComp₂₃ F G₂₃).obj X₁).obj X₂).map f ≫ (F.obj X₁).map ((φ.app X₂).app Y₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (((bifunctorComp₂₃ F G₂₃').obj X₁).obj X₂).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫ { app := fun X₃ ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ } =
    { app := fun X₃ ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ } ≫ ((bifunctorComp₂₃ F G₂₃').obj X₁).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝² : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝¹ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections
⊢ (forget₂ CommGrpCat GrpCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommGrpCat)).pt,
        π :=
          { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) j),
            naturality := ⋯ } } ≅
    c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂₃ ⥤ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ ((bifunctorComp₂₃FunctorObj F).obj G₂₃).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } ≫
      ((bifunctorComp₂₃FunctorObj F').obj G₂₃).map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
this✝² : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
this✝¹ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙ forget MonCat).sections
this : Small.{u, max u v} ↑((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections
⊢ IsLimit
    ((forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommGrpCat)).pt,
        π :=
          { app := fun j ↦ ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) j),
            naturality := ⋯ } })

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone (F ⋙ forget₂ CommGrpCat GrpCat)
hc : IsLimit c
⊢ LiftsToLimit F (forget₂ CommGrpCat GrpCat) c hc

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : L.Faithful
X Y : C
f g : Y ⟶ (𝟭 C).obj X
hfg : f ≫ h.unit.app X = g ≫ h.unit.app X
⊢ (h.homEquiv Y (L.obj X)) (L.map f) = (h.homEquiv Y (L.obj X)) (L.map g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : L.Full
X : C
⊢ L.preimage (h.counit.app (L.obj X)) ≫ h.unit.app X = 𝟙 ((L ⋙ R).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : R.Faithful
X Y : D
f g : (𝟭 D).obj X ⟶ Y
hfg : h.counit.app X ≫ f = h.counit.app X ≫ g
⊢ (h.homEquiv (R.obj X) Y).symm (R.map f) = (h.homEquiv (R.obj X) Y).symm (R.map g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : R.Full
X : D
⊢ h.counit.app X ≫ R.preimage (h.unit.app (R.obj X)) = 𝟙 ((R ⋙ L).obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
this : L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
⊢ L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
⊢ HasLimit (F ⋙ forget₂ CommGrpCat GrpCat)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
c : Cone F
hc : IsLimit c
⊢ IsLimit ((forget₂ CommGrpCat GrpCat).mapCone c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ CreatesLimit F (forget CommGrpCat)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
f : ℕ → AddCommGrpCat
⊢ HasProduct f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ⟨(ConcreteCategory.hom (kernel.ι f)) 0, ⋯⟩ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), IsSplitMono (h.counit.app X)
X Y : D
f : R.obj X ⟶ R.obj Y
this : R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X)
⊢ R.map (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
g g' : ↑(limit.cone (parallelPair f 0)).1
⊢ ⟨(ConcreteCategory.hom (kernel.ι f)) (g + g'), ⋯⟩ =
    ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩ + ⟨(ConcreteCategory.hom (kernel.ι f)) g', ⋯⟩

Tactic:
by

Goal state after: