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

Goal state before:
pp: case 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
x✝¹ : J
x✝ :
  ((Functor.const J).obj
        ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).pt).obj
    x✝¹
⊢ (limitπMonoidHom F x✝¹) x✝ = (ConcreteCategory.hom ((Types.coneOfSection ⋯).π.app x✝¹)) PUnit.unit

Tactic:
rfl

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

Goal state before:
pp: 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
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1

Tactic:
rfl

Goal state after:
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
⊢ (equivShrink ↑(F ⋙ forget MonCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x * (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩ =
    (equivShrink ↑(F ⋙ forget MonCat).sections)
      (⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) x, ⋯⟩ * ⟨fun j ↦ (ConcreteCategory.hom (s✝.π.app j)) y, ⋯⟩)

Tactic:
rfl

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
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹ +
          (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝)
      j =
    ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝¹) j +
      ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j

Tactic:
rfl

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
j : J
x✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ ↑(x✝¹ • (equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j =
    x✝¹ • ↑((equivShrink ↑(F ⋙ forget (ModuleCat R)).sections).symm x✝) j

Tactic:
rfl

Goal state after:
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
⊢ ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x + (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩ =
    ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ + ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩

Tactic:
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
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
⊢ ↑((algebraMap R ↑(F ⋙ forget (AlgCat R)).sections) x) j = (algebraMap R (ToType (F.obj j))) x

Tactic:
rfl

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

Goal state before:
pp: case refine_2
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
r : R
x : ↑s.1
⊢ ⟨fun j ↦ r • (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ = r • ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩

Tactic:
rfl

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 ((directLimitDiagram G f).map (homOfLE h) ≫ s.ι.app j)) x

Tactic:
rfl

Goal state after:
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
j : J
⊢ (ConcreteCategory.hom (s.π.app j)) x * (ConcreteCategory.hom (s.π.app j)) y =
    ↑(⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ * ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩) j

Tactic:
rfl

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

Goal state before:
pp: case refine_3
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
j : J
⊢ 0 = ↑0 j

Tactic:
rfl

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

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

Tactic:
ext j
    simp
    rfl

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
i : ι
⊢ (directLimitCocone G f).ι.app i ≫ m = ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m

Tactic:
rfl

Goal state after:
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
j : J
⊢ (ConcreteCategory.hom (s.π.app j)) x + (ConcreteCategory.hom (s.π.app j)) y =
    ↑(⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ + ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩) j

Tactic:
rfl

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

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype)) x✝ = (Hom.hom (kernel.ι f)) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv

Tactic:
by
  rw [← assoc, ← leftUnitor_naturality]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ X ◁ f h✝ = X ◁ f h✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ X ◁ f' h✝ = X ◁ f' h✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : P
⊢ f h✝ ▷ Z = f h✝ ▷ Z

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h✝ : ¬P
⊢ f' h✝ ▷ Z = f' h✝ ▷ Z

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ f ⊗ₘ g h✝ = f ⊗ₘ g h✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ f ⊗ₘ g' h✝ = f ⊗ₘ g' h✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : P
⊢ g h✝ ⊗ₘ f = g h✝ ⊗ₘ f

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
P : Prop
inst✝ : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h✝ : ¬P
⊢ g' h✝ ⊗ₘ f = g' h✝ ⊗ₘ f

Tactic:
rfl

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

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ (equivShrink ↑(F ⋙ forget SemiRingCat).sections) ⟨fun j ↦ 1, ⋯⟩ = 1

Tactic:
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
⊢ ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x * (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩ =
    ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ * ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case refine_3
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
⊢ (equivShrink ↑(F ⋙ forget SemiRingCat).sections) ⟨fun j ↦ 0, ⋯⟩ = 0

Tactic:
rfl

Goal state after:
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
⊢ ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x + (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩ =
    ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ + ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
hom✝ : F.toFunctor ⟶ G.toFunctor
isMonoidal✝¹ : NatTrans.IsMonoidal hom✝
isMonoidal✝ : NatTrans.IsMonoidal { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom
⊢ { hom := hom✝, isMonoidal := isMonoidal✝¹ } =
    { hom := { hom := hom✝, isMonoidal := isMonoidal✝¹ }.hom, isMonoidal := isMonoidal✝ }

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M : SemimoduleCat R
N : SemimoduleCat R
⊢ (mk R ↑M ↑N).compr₂ₛₗ (Hom.hom (tensorHom (𝟙 M) (𝟙 N))) = (mk R ↑M ↑N).compr₂ₛₗ (Hom.hom (𝟙 (of R (↑M ⊗[R] ↑N))))

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ Y₁ Z₁ : SemimoduleCat R
X₂ Y₂ Z₂ : SemimoduleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (mk R ↑X₁ ↑X₂).compr₂ₛₗ (Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)) =
    (mk R ↑X₁ ↑X₂).compr₂ₛₗ (Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)))

Tactic:
rfl

Goal state after:
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:
rfl

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
W : SemimoduleCat R
X : SemimoduleCat R
Y : SemimoduleCat R
Z : SemimoduleCat R
w : ↑W
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom
        (whiskerRight (associator W X Y).hom Z ≫
          (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
      (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) =
    (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)) (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)

Tactic:
rfl

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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 = ε F

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 = ε G

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = μ F X Y

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = μ G X Y

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).1 = η F

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
⊢ (η (F.prod G)).2 = η G

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y

Tactic:
rfl

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).2 = δ G X Y

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ identities C f✝ → W f✝

Tactic:
⟨_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x✝ : W.ContainsIdentities
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W (𝟙 X✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
⊢ identities C ≤ identities C

Tactic:
rfl

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

Goal state before:
pp: case leftAdjoint_ε
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
this : G.LaxMonoidal := ⋯
⊢ autoParam (ε G = adj.unit.app (𝟙_ C) ≫ G.map (η F)) IsMonoidal.leftAdjoint_ε._autoParam

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ : Arrow (Type u)
f✝ : X✝ ⟶ Y✝
⊢ ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
            map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
            map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
            map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.map
        f✝ ≫
      ↾fun y ↦ ↑y) =
    (↾fun y ↦ ↑y) ≫ Arrow.rightFunc.map f✝

Tactic:
rfl

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

Goal state before:
pp: case leftAdjoint_μ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
X✝ Y✝ : D
⊢ μ G X✝ Y✝ =
    adj.unit.app (G.obj X✝ ⊗ G.obj Y✝) ≫ G.map (δ F (G.obj X✝) (G.obj Y✝) ≫ (adj.counit.app X✝ ⊗ₘ adj.counit.app Y✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ x₁ = x₂

Tactic:
rw [Subtype.ext_iff]
    exact h

Goal state after:
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
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ≫ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G)) ⊗ₘ
          adj.unit.app x✝ ≫ 𝟙 (G.obj (F.obj x✝))) ≫
        μ G (𝟙_ D) (F.obj x✝)

Tactic:
simp [tensorHom_def', homEquiv_unit, homEquiv_counit]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)

Tactic:
braiding_tensorUnit_left

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).hom ≫ (ρ_ X).inv) ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ D
toMonoidal✝ : F.Monoidal
braided✝¹ : ∀ (X Y : C), μ F X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
braided✝ : ∀ (X Y : C), μ F X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
⊢ { toMonoidal := toMonoidal✝, braided := braided✝¹ } =
    { toMonoidal := { toMonoidal := toMonoidal✝, braided := braided✝¹ }.toMonoidal, braided := braided✝ }

Tactic:
rfl

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom ((colimitCocone F).ι.app j ≫ m))

Tactic:
rfl

Goal state after: