mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Linear

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
⊢ ∀ (r : R) {Y Z : D} (f : Y ⟶ Z) (X : D), (r • f) ▷ X = r • f ▷ X

Tactic:
intro r

Goal state after:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{v_1, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
r : R
⊢ ∀ {Y Z : D} (f : Y ⟶ Z) (X : D), (r • f) ▷ X = r • f ▷ X
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.associator x✝² x✝¹ x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝² x✝¹))
                  (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
            MonoidalCategory.tensorIso
              (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                    (equivalenceSemimoduleCat.functor.obj x✝¹))).symm
              (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
          MonoidalCategoryStruct.associator (equivalenceSemimoduleCat.functor.obj x✝²)
              (equivalenceSemimoduleCat.functor.obj x✝¹) (equivalenceSemimoduleCat.functor.obj x✝) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝²))
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝¹)
                    (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝¹ x✝)))).hom

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.associator x✝² x✝¹ x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝² x✝¹))
                  (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
            MonoidalCategory.tensorIso
              (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                    (equivalenceSemimoduleCat.functor.obj x✝¹))).symm
              (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
          MonoidalCategoryStruct.associator (equivalenceSemimoduleCat.functor.obj x✝²)
              (equivalenceSemimoduleCat.functor.obj x✝¹) (equivalenceSemimoduleCat.functor.obj x✝) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝²))
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝¹)
                    (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝¹ x✝)))).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.leftUnitor x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                  (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
            MonoidalCategory.tensorIso (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
              (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
          MonoidalCategoryStruct.leftUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.leftUnitor x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                  (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
            MonoidalCategory.tensorIso (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
              (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
          MonoidalCategoryStruct.leftUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.rightUnitor x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝)
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R))))).symm ≪≫
            MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))
              (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm) ≪≫
          MonoidalCategoryStruct.rightUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.rightUnitor x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝)
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R))))).symm ≪≫
            MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))
              (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm) ≪≫
          MonoidalCategoryStruct.rightUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : M₁ ⊗ M₂ ⟶ M₃
h : ∀ (m : ↑M₁) (n : ↑M₂), (Hom.hom f) (m ⊗ₜ[R] n) = (Hom.hom g) (m ⊗ₜ[R] n)
x✝¹ : ↑M₁
x✝ : ↑M₂
⊢ (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom f)) x✝¹) x✝ =
    (((TensorProduct.mk R ↑M₁ ↑M₂).compr₂ₛₗ (Hom.hom g)) x✝¹) x✝
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ (unop W ◁ (α_ (unop X) (unop Y) (unop Z)).inv ≫ (α_ (unop W) (unop X ⊗ unop Y) (unop Z)).inv) ≫
      (α_ (unop W) (unop X) (unop Y)).inv ▷ unop Z =
    (α_ (unop W) (unop X) (unop Y ⊗ unop Z)).inv ≫ (α_ (unop W ⊗ unop X) (unop Y) (unop Z)).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ (unop W ◁ (α_ (unop X) (unop Y) (unop Z)).inv ≫ (α_ (unop W) (unop X ⊗ unop Y) (unop Z)).inv) ≫
      (α_ (unop W) (unop X) (unop Y)).inv ▷ unop Z =
    (α_ (unop W) (unop X) (unop Y ⊗ unop Z)).inv ≫ (α_ (unop W ⊗ unop X) (unop Y) (unop Z)).inv
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ unop X ◁ (λ_ (unop Y)).inv ≫ (α_ (unop X) (𝟙_ C) (unop Y)).inv = (ρ_ (unop X)).inv ▷ unop Y

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ unop X ◁ (λ_ (unop Y)).inv ≫ (α_ (unop X) (𝟙_ C) (unop Y)).inv = (ρ_ (unop X)).inv ▷ unop Y
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ Z.unmop ◁ (α_ Y.unmop X.unmop W.unmop).inv ≫
      (α_ Z.unmop (Y.unmop ⊗ X.unmop) W.unmop).inv ≫ (α_ Z.unmop Y.unmop X.unmop).inv ▷ W.unmop =
    (α_ Z.unmop Y.unmop (X.unmop ⊗ W.unmop)).inv ≫ (α_ (Z.unmop ⊗ Y.unmop) X.unmop W.unmop).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ Z.unmop ◁ (α_ Y.unmop X.unmop W.unmop).inv ≫
      (α_ Z.unmop (Y.unmop ⊗ X.unmop) W.unmop).inv ≫ (α_ Z.unmop Y.unmop X.unmop).inv ▷ W.unmop =
    (α_ Z.unmop Y.unmop (X.unmop ⊗ W.unmop)).inv ≫ (α_ (Z.unmop ⊗ Y.unmop) X.unmop W.unmop).inv
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ (α_ Y.unmop (𝟙_ C) X.unmop).inv ≫ (ρ_ Y.unmop).hom ▷ X.unmop = Y.unmop ◁ (λ_ X.unmop).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ (α_ Y.unmop (𝟙_ C) X.unmop).inv ≫ (ρ_ Y.unmop).hom ▷ X.unmop = Y.unmop ◁ (λ_ X.unmop).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case η
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ η F = η F

Tactic:
← cancel_epi (εIso _).hom

Goal state after:
case η
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ (εIso F).hom ≫ η F = (εIso F).hom ≫ η F
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η η' : g ⟶ h
θ : f ⊗ g ⟶ f ⊗ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
by
  simp [e_η, e_θ]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η η' : f ⟶ g
θ : f ⊗ h ⟶ g ⊗ h
e_η : η = η'
e_θ : η' ▷ h = θ
⊢ η ▷ h = θ

Tactic:
by
  simp [e_η, e_θ]

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
h : F.CoreMonoidal
inst✝² : F.OplaxMonoidal
inst✝¹ : IsIso (η F)
inst✝ : ∀ (X Y : C), IsIso (δ F X Y)
X Y Z : C
⊢ (asIso (δ F X Y)).symm.hom ▷ F.obj Z ≫ (asIso (δ F (X ⊗ Y) Z)).symm.hom ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ (asIso (δ F Y Z)).symm.hom ≫ (asIso (δ F X (Y ⊗ Z))).symm.hom

Tactic:
simp [← cancel_epi (δ F X Y ▷ F.obj Z), ← cancel_epi (δ F (X ⊗ Y) Z)]

Goal state after:
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✝ : HasColimit F
j : J
⊢ (limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop

Tactic:
by
  simp [limitUnopIsoUnopColimit]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) ⋯))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm _

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
i : IsIso (pullbackComparison G f g)
⊢ IsLimit (PullbackCone.mk (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) ⋯)
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✝
⊢ W (𝟙 X✝)

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.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫
      (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Tactic:
rw [← braiding_tensor_right_hom_assoc X Y Z, ← cancel_mono (α_ Z Y X).inv]
  repeat rw [assoc]
  rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]

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)
φ : X✝ ⟶ Y✝
x : X✝.left
⊢ (hom (Arrow.Hom.right φ)) ↑⟨(TypeCat.Hom.hom X✝.hom) x, ⋯⟩ ∈ Set.range ⇑(TypeCat.Hom.hom Y✝.hom)

Tactic:
;

Goal state after:
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)
φ : X✝ ⟶ Y✝
x : X✝.left
⊢ (hom (Arrow.Hom.right φ)) ↑⟨(TypeCat.Hom.hom X✝.hom) x, ⋯⟩ ∈ Set.range ⇑(TypeCat.Hom.hom Y✝.hom)
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:
;

Goal state after:
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✝
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:

Tactic:
;

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
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom) ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom) ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv
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) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom
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) (𝟙_ C) X).inv ≫ ((ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ ((ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
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:
;

Goal state after:
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✝ }
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₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ Y₂ Z₁).hom ≫ (β_ X₂ Y₁).hom ▷ (Z₁ ⊗ Y₂)) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁
                ((α_ X₂ Y₁ Z₁).inv ≫
                    (β_ X₂ Y₁).hom ▷ Z₁ ≫ (α_ Y₁ X₂ Z₁).hom ≫ Y₁ ◁ (β_ X₂ Z₁).hom ≫ (α_ Y₁ Z₁ X₂).inv) ▷
                  (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ Y₂ Z₁).hom ≫ (β_ X₂ Y₁).hom ▷ (Z₁ ⊗ Y₂)) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁
                ((α_ X₂ Y₁ Z₁).inv ≫
                    (β_ X₂ Y₁).hom ▷ Z₁ ≫ (α_ Y₁ X₂ Z₁).hom ≫ Y₁ ◁ (β_ X₂ Z₁).hom ≫ (α_ Y₁ Z₁ X₂).inv) ▷
                  (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) =
    ((Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h)) x

Tactic:
;

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : Quot F
eq : (Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h) = Quot.desc F s
⊢ (Hom.hom m) ((AddEquiv.ofBijective (Quot.desc F c) h) x) =
    ((Hom.hom m).comp ↑(AddEquiv.ofBijective (Quot.desc F c) h)) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max u w} (Quot F)
⊢ IsColimit (colimitCocone F)

Tactic:
refine isColimit_of_bijective_desc F _ ?_
  rw [Quot.desc_colimitCocone]
  exact Shrink.addEquiv.symm.bijective

Goal state after: