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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        (α_ (F.obj W) (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).hom ≫
            F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫
              F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z ≫
                F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom ≫
                    F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom =
    (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (α_ (F.obj (W ⊗ X)) (F.obj Y) (F.obj Z)).hom ≫
        F.obj (W ⊗ X) ◁ (fData.μIso Y Z).hom ≫
          (fData.μIso W X).inv ▷ F.obj (Y ⊗ Z) ≫
            (α_ (F.obj W) (F.obj X) (F.obj (Y ⊗ Z))).hom ≫
              F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom

Tactic:
slice_lhs 5 6 =>
      rw [← whiskerLeft_comp, hom_inv_whiskerRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        (α_ (F.obj W) (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).hom ≫
            (((F.obj W ◁ 𝟙 ((F.obj X ⊗ F.obj Y) ⊗ F.obj Z) ≫ F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom) ≫
                F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom) ≫
              (fData.μIso W (X ⊗ Y ⊗ Z)).hom =
    (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (α_ (F.obj (W ⊗ X)) (F.obj Y) (F.obj Z)).hom ≫
        F.obj (W ⊗ X) ◁ (fData.μIso Y Z).hom ≫
          (fData.μIso W X).inv ▷ F.obj (Y ⊗ Z) ≫
            (α_ (F.obj W) (F.obj X) (F.obj (Y ⊗ Z))).hom ≫
              F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : Linear R F
X : C
⊢ ∀ (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)

Tactic:
r

Goal state after:
case mp
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : Linear R F
X : C
r : R
⊢ F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
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
X Y Z : D
⊢ ∀ (r : R) (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f

Tactic:
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
X Y Z : D
r : R
⊢ ∀ (f : Y ⟶ Z), X ◁ (r • f) = r • X ◁ f
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X : C
j : J
⊢ biproduct.ι f j ▷ X ≫ (rightDistributor f X).hom = biproduct.ι (fun j ↦ f j ⊗ X) j

Tactic:
cases nonempty_fintype J
  simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_whiskerRight_assoc, biproduct.ι_π,
    dite_whiskerRight, dite_comp]

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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom

Tactic:
← cancel_mono (ρ_ (F.obj X)).inv,

Goal state after:
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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (ρ_ (F.obj X)).hom ≫ (ρ_ (F.obj X)).inv =
    (F.obj X ◁ εIso.hom ≫ (μIso X (𝟙_ C)).hom ≫ F.map (ρ_ X).hom) ≫ (ρ_ (F.obj X)).inv
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
inst✝ : HasFiniteWidePushouts C
⊢ HasFiniteWidePullbacks Cᵒᵖ

Tactic:
refine ⟨fun J _ ↦ ?_⟩
  rw [hasLimitsOfShape_opposite_iff]
  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

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✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj X✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ μ G (F.obj x✝¹) (F.obj X✝)) ≫
      F.obj x✝¹ ◁ F.map x✝ =
    F.map (x✝¹ ◁ x✝) ≫
      (adj.homEquiv (x✝¹ ⊗ Y✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
        ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))

Tactic:
rw [← Adjunction.homEquiv_naturality_right_symm,
      ← Adjunction.homEquiv_naturality_left_symm, assoc, ← μ_natural_right]
    simp [← id_tensorHom]

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 : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.right = (pushout.inr f.op g.op).unop

Tactic:
simp [unop_id (X := { unop := Y })]

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

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| 𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ ≫ 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom

Tactic:
rw [← whiskerLeft_comp, ← comp_whiskerRight,
    leftUnitor_inv_braiding]

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| 𝟙_ C ◁ (ρ_ X₁).inv ▷ X₂

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun j ↦
        ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
              (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j)).comp
          AddEquiv.ulift.symm.toAddMonoidHom)
      ((DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j))
      { down := x }

Tactic:
simp only [DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
            (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j)).comp
        AddEquiv.ulift.symm.toAddMonoidHom)
      x =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j ↦ ↑(uliftFunctor.obj (F.obj j))) j))
      { down := 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
x : Quot (F ⋙ uliftFunctor)
⊢ ((quotToQuotUlift F).comp (quotUliftToQuot F)) x = (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) x

Tactic:
Quot.addMonoidHom_ext _ (f := (quotToQuotUlift F).comp
      (quotUliftToQuot F)) (fun j a ↦ ?_)

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
⊢ ?m.150 x = (AddMonoidHom.id (Quot (F ⋙ uliftFunctor))) x

J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
⊢ Quot (F ⋙ uliftFunctor) →+ Quot (F ⋙ uliftFunctor)

J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot (F ⋙ uliftFunctor)
j : J
a : ↑((F ⋙ uliftFunctor).obj j)
⊢ ((quotToQuotUlift F).comp (quotUliftToQuot F)) ((Quot.ι (F ⋙ uliftFunctor) j) a) =
    ?m.150 ((Quot.ι (F ⋙ uliftFunctor) j) a)
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 : ↑c.pt
⊢ (Hom.hom m) x =
    (Hom.hom (ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom))) x

Tactic:
obtain ⟨x, rfl⟩ := h.2 x

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
⊢ (Hom.hom m) ((Quot.desc F c) x) =
    (Hom.hom (ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom)))
      ((Quot.desc F c) x)
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map
            (L₃.map
              ((G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b)))) ≫
                G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
rw [L₃.map_comp, R₃.map_comp]

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b))))) ≫
            R₃.map (L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β)

Tactic:
Equiv.eq_symm_apply,

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₁ adj₃) ((conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α) = α ≫ β
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ ↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ rTensor (A × B) comul ∘ₗ comul = lTensor (A × B) comul ∘ₗ comul

Tactic:
by
    dsimp +instances only [instCoalgebraStruct]
    ext x : 2 <;> dsimp only [comp_apply, LinearEquiv.coe_coe, coe_inl, coe_inr, coprod_apply]
    · simp only [map_zero, add_zero]
      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inl,
        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]
    · simp only [map_zero, zero_add]
      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inr,
        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case refine_2
S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
x : tsze R M
⊢ inr x.snd ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)

Tactic:
exact le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd

Goal state after:
Module: Mathlib.Order.Category.Preord

Goal state before:
pp: X✝ Y✝ : Preord
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : preordToCat.map a₁✝ = preordToCat.map a₂✝
x : ↑X✝
⊢ (Preord.Hom.hom a₁✝) x = (Preord.Hom.hom a₂✝) x

Tactic:
exact Functor.congr_obj congr(($h).toFunctor) x

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] R
g : N →ₗ[R] M'
h : P →ₗ[R] M ⊗[R] N
⊢ λ ∘ₗ f ⊗ₘ g ∘ₗ h = g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id ∘ₗ h

Tactic:
by
  simp only [← LinearMap.comp_assoc, lid_comp_map _ g]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
⊢ f ⊗ₘ ε ∘ₗ δ ∘ₗ g = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

Tactic:
by
  simp_rw [← LinearMap.comp_assoc, map_counit_comp_comul_right]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case a
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (normalize a) (normalizedFactors b)) ≤ emultiplicity a b

Tactic:
rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : N.FG
⊢ Ring.jacobson R • N < N

Tactic:
← Module.Finite.iff_fg

Goal state after:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite R ↥N
⊢ Ring.jacobson R • N < N
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this✝ : IsLocalRing S
this : (Ideal.comap f (maximalIdeal S)).IsMaximal
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)

Tactic:
exact ((maximal_ideal_unique R).unique (inferInstanceAs (maximalIdeal R).IsMaximal) this).le

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ μ = ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ

Tactic:
simp only [Category.id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ μ = ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ

Tactic:
simp only [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'

Tactic:
· simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'

pp: case comminl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'

pp: case comminr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'

Tactic:
· simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

Goal state after:
case comminl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'

case comminr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'