mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), (hom (F.map f)) (x j) = x j'
j : J
⊢ (hom (limit.π F j)) (mk F x h) = x j

Tactic:
dsimp [Limit.mk]

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasLimit F
x : (j : J) → F.obj j
h : ∀ (j j' : J) (f : j ⟶ j'), (hom (F.map f)) (x j) = x j'
j : J
⊢ (hom (limit.π F j)) ((limitEquivSections F).symm ⟨x, ⋯⟩) = x j
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a +
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c =
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c

Tactic:
intro x

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ ∀ (b c : (j : J) × ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x +
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) *
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c =
      Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel x *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c +
        Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b *
          Quot.mk ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel c
Module: Mathlib.CategoryTheory.Limits.Preserves.Limits

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    colimit.ι (X✝ ⋙ G) j ≫ colimMap (Functor.whiskerRight f G) ≫ (preservesColimitIso G Y✝).inv

Tactic:
ι_colimMap_assoc

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    (Functor.whiskerRight f G).app j ≫ colimit.ι (Y✝ ⋙ G) j ≫ (preservesColimitIso G Y✝).inv
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ Finset.univ.powerset with 2 ≤ #x_1, f (x_1.piecewise h x) +
      ∑ x_1 ∈ Finset.univ.powerset with ¬2 ≤ #x_1, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ s ∈ Finset.univ.powerset with 2 ≤ #s, f (s.piecewise h x)

Tactic:
simp_rw [not_le, Nat.lt_succ_iff, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
    ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
    powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
    Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]

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

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : F₁.flip = F₂.flip
⊢ F₁ = F₂

Tactic:
← flip_flip F₁,

Goal state after:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F₁ F₂ : B ⥤ C ⥤ D
h : F₁.flip = F₂.flip
⊢ F₁.flip.flip = F₂
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ (s.pt.map f ≫ (t Y).lift { pt := s.pt.obj Y, π := whiskerRight s.π ((evaluation K C).obj Y) }) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j =
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π ((evaluation K C).obj X) } ≫ c.pt.map f) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j

Tactic:
by
          rw [assoc, (t Y).fac _ j]
          simpa using
            ((t X).fac_assoc ⟨s.pt.obj X, whiskerRight s.π ((evaluation K C).obj X)⟩ j _).symm

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
P : C ⥤ Type w
f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) =
    (ConcreteCategory.hom (f.app (unop Y))) (shrinkCoyonedaObjObjEquiv.symm g.unop)

Tactic:
by
  simp [shrinkYonedaObjObjEquiv, shrinkCoyonedaEquiv, shrinkYoneda,
    ← comp_apply, ← NatTrans.naturality]

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s : Cone F
x : ↑s.1
⊢ ∀ (y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget MonCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget MonCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ ∀ (x y : ↑s✝.1),
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
        (x * y) =
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
        (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y

Tactic:
intro x

Goal state after:
case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
x : ↑s✝.1
⊢ ∀ (y : ↑s✝.1),
    (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝)))
        (x * y) =
      (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) x *
        (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) y
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_1
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
s : Cone F
⊢ ∀ (x y : ↑s.1),
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        (x + y) =
      (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          x +
        (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          y

Tactic:
intro x

Goal state after:
case refine_1
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
s : Cone F
x : ↑s.1
⊢ ∀ (y : ↑s.1),
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        (x + y) =
      (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          x +
        (ConcreteCategory.hom
            ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
          y
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_2
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
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_2
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
s : Cone F
x : ↑s.1
⊢ ∀ (y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_4
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
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_4
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
s : Cone F
x : ↑s.1
⊢ ∀ (y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩
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
    have : HasLimit _ := ⟨_, hc⟩
    have : Small.{u} (F ⋙ forget CommGrpCat).sections :=
      Concrete.small_sections_of_hasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
    have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙
      forget MonCat).sections := this
    have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections := this
    exact
      { liftedCone :=
          { pt := CommGrpCat.of (Types.Small.limitCone.{v, u} (F ⋙ forget CommGrpCat)).pt
            π :=
              { app j := ofHom <| MonCat.limitπMonoidHom
                  (F ⋙ forget₂ CommGrpCat GrpCat.{u} ⋙ forget₂ GrpCat MonCat.{u}) j
                naturality i j h := hom_ext <| congr_arg MonCat.Hom.hom <|
                  (MonCat.HasLimits.limitCone _).π.naturality h } }
        validLift := by apply IsLimit.uniqueUpToIso (GrpCat.limitConeIsLimit _) hc
        makesLimit :=
          IsLimit.ofFaithful (forget₂ _ GrpCat.{u} ⋙ forget₂ _ MonCat.{u})
            (by apply MonCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }

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

Goal state before:
pp: case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
x : ↑s.1
⊢ ∀ (y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x * y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ *
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
x : ↑s.1
⊢ ∀ (y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
⊢ IsLimit ((forget₂ RingCat AddCommGrpCat).mapCone (limitCone F))

Tactic:
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ RingCat.{u} AddCommGrpCat.{u}) ⋙ forget _)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
x✝ : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat AddCommGrpCat) ⋙ forget AddCommGrpCat).sections :=
  forget₂AddCommGroupPreservesLimitsAux._proof_1 F
⊢ IsLimit ((forget₂ RingCat AddCommGrpCat).mapCone (limitCone F))
Module: Mathlib.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
⊢ { as := X₁✝.as * X₂✝.as } = { as := Y₁✝.as * Y₂✝.as }

Tactic:
eq_of_hom f,

Goal state after:
M : Type u
inst✝ : Monoid M
X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
⊢ { as := Y₁✝.as * X₂✝.as } = { as := Y₁✝.as * Y₂✝.as }
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ∀ (x : ↑X₁) (y : ↑X₂) (z : ↑X₃),
    (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ : SemimoduleCat R
X₂ : SemimoduleCat R
X₃ : SemimoduleCat R
Y₁ : SemimoduleCat R
Y₂ : SemimoduleCat R
Y₃ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
x : ↑X₁
⊢ ∀ (y : ↑X₂) (z : ↑X₃),
    (Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence

Goal state before:
pp: case ih_η
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : p ⊗ f₁ ≅ pf₁
η_g₁ : p ⊗ g₁ ≅ pf₁
η_f₂ : pf₁ ⊗ f₂ ≅ pf₁f₂
η_g₂ : pf₁ ⊗ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ η ▷ f₂ ≪≫ ?η_g = normalizeIsoComp η_f₁ η_f₂

Tactic:
apply naturality_whiskerRight _ _ _ ih_η

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
x : ↑M
⊢ ∀ (y : ↑(of R R)) (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
⊢ CategoryTheory.inv (μ F X Y) = δ F X Y

Tactic:
by
  rw [← Monoidal.μIso_inv, ← CategoryTheory.IsIso.inv_eq_inv]
  simp only [IsIso.inv_inv, IsIso.Iso.inv_inv, μIso_hom]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂),
    (Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))) (x ⊗ₜ[R] y)

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : ↑X₁
⊢ ∀ (y : ↑X₂),
    (Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))) (x ⊗ₜ[R] y)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
x : ↑X
⊢ ∀ (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom)) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
⊢ ∀ (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) (x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
intro x

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
x : ↑X
⊢ ∀ (y : ↑Y) (z : ↑Z),
    (Hom.hom ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv)) (x ⊗ₜ[R] y ⊗ₜ[R] z) =
      (Hom.hom ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y)) (x ⊗ₜ[R] y ⊗ₜ[R] z)
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : Jᵒᵖ
⊢ colimit.ι F.leftOp j ≫ (colimitLeftOpIsoUnopLimit F).hom = (limit.π F (unop j)).unop

Tactic:
simp [colimitLeftOpIsoUnopLimit]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op).unop = (pushout.inr f g).op.unop

Tactic:
simp [← pushoutIsoUnopPullback_inr_hom]

Goal state after: