mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B B' : D
⊢ ∀ (g : B ⟶ B') (h : comparisonLeftAdjointObj adj A ⟶ B),
    (comparisonLeftAdjointHomEquiv adj A B') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj A B) h ≫ (comparison adj).map g

Tactic:
g

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
B B' : D
g : B ⟶ B'
⊢ ∀ (h : comparisonLeftAdjointObj adj A ⟶ B),
    (comparisonLeftAdjointHomEquiv adj A B') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj A B) h ≫ (comparison adj).map g
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
x y : C
z z' : D
f : z ⟶ z'
⊢ (x ⊗ y) ⊴ₗ f = (αₗ x y z).hom ≫ x ⊴ₗ y ⊴ₗ f ≫ (αₗ x y z').inv

Tactic:
simp only [← id_actionHom]
  rw [← Category.assoc, ← actionAssocIso_hom_naturality]
  simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalLeftAction C D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝² x✝¹ : D
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun y ↦ X✝ ⊙ₗ y, map := fun {X Y} f ↦ X✝ ⊴ₗ f, map_id := ⋯, map_comp := ⋯ }.map x✝ ≫ f ⊵ₗ x✝¹ =
    f ⊵ₗ x✝² ≫ { obj := fun y ↦ Y✝ ⊙ₗ y, map := fun {X Y} f ↦ Y✝ ⊴ₗ f, map_id := ⋯, map_comp := ⋯ }.map x✝

Tactic:
by simp [action_exchange]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalRightAction C D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝² x✝¹ : D
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun y ↦ y ⊙ᵣ X✝, map := fun {X Y} f ↦ f ⊵ᵣ X✝, map_id := ⋯, map_comp := ⋯ }.map x✝ ≫ x✝¹ ⊴ᵣ f =
    x✝² ⊴ᵣ f ≫ { obj := fun y ↦ y ⊙ᵣ Y✝, map := fun {X Y} f ↦ f ⊵ᵣ Y✝, map_id := ⋯, map_comp := ⋯ }.map x✝

Tactic:
by simp [action_exchange]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left (f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom) =
    pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
        (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom) ≫
      Arrow.Hom.left ((ρ_ X).hom ≫ f)

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actLeft = 𝟙 (X.X ⊗ Q.X) ≫ Q.actLeft

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actLeft = Q.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight = 𝟙 (Q.X ⊗ Y.X) ≫ Q.actRight

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight = Q.actRight
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B✝ A : C
B' : D
iB' : i.obj B' ≅ B✝
⊢ i.essImage (A ⟹ B✝)

Tactic:
exact Functor.essImage.ofIso ((ihom A).mapIso iB') (h B' A)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h₂
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ BinaryFan.snd
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).snd

Tactic:
simp only [BinaryFan.snd, Cone.postcompose, pairComp]

Goal state after:
case h₂
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ ((i.mapCone
              (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
                ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y))).π ≫
          (diagramIsoPair (pair X Y ⋙ i)).hom).app
      { as := WalkingPair.right } =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      𝟙 ((reflector i).obj A ⊗ (reflector i).obj (A ⟹ i.obj B)) ≫
        inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
          (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
q : i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B :=
  curry
    ((ir.homEquiv (A ⊗ i.obj (L.obj (A ⟹ i.obj B))) B)
      ((prodComparison L A (i.obj (L.obj (A ⟹ i.obj B))) ≫
          L.obj A ◁ ε.app (L.obj (A ⟹ i.obj B)) ≫ inv (prodComparison (reflector i) A (A ⟹ i.obj B))) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B))))
⊢ prodComparison (reflector i) A (A ⟹ i.obj B) ≫
      inv (prodComparison (reflector i) A (A ⟹ i.obj B)) ≫
        (ir.homEquiv ((ihom A ⋙ tensorLeft A).obj (i.obj B)) B).symm ((ihom.ev A).app (i.obj B)) =
    (ir.homEquiv (A ⊗ (A ⟹ i.obj B)) B).symm ((ihom.ev A).app (i.obj B))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ 𝟙 ((reflector i).obj A ⊗ (reflector i).obj B) ≫
      (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B)))

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Reflective i
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B))) =
    (bijection i A B ((reflector i).obj (A ⊗ B))) (𝟙 ((reflector i).obj (A ⊗ B)))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      (MonoidalClosed.pre (F.map f)).app ((F ⊛ G).obj (c'' ⊗ c))

Tactic:
simp [MonoidalClosed.curry_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  MonoidalClosed.curry (F.obj j ◁ G.map f) ≫ (ihom (F.obj j)).map ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry (F.obj j ◁ G.map f) ≫ (ihom (F.obj j)).map ((DayConvolution.unit F G).app (j, c'))

Tactic:
simp [MonoidalClosed.curry_eq]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (A ⊗ A) ◁ Δ ≫
        (α_ A A (A ⊗ A)).hom ≫
          A ◁ (α_ A A A).inv ≫
            A ◁ (β_ A A).hom ▷ A ≫
              A ◁ (α_ A A A).hom ≫
                (((((((𝟙 (A ⊗ A ⊗ A ⊗ A) ≫ A ◁ A ◁ (β_ A A).hom) ≫ (α_ A A (A ⊗ A)).inv) ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮)) ≫
                          (α_ (A ⊗ A) A A).inv) ≫
                        (α_ A A A).hom ▷ A) ≫
                      (A ◁ μ) ▷ A) ≫
                    μ ▷ A) ≫
                  μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ▷ A ≫
      (A ⊗ A) ◁ Δ ≫
        (α_ A A (A ⊗ A)).hom ≫
          A ◁ (α_ A A A).inv ≫
            A ◁ (β_ A A).hom ▷ A ≫
              A ◁ (α_ A A A).hom ≫
                ((((((A ◁ A ◁ (β_ A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫ (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮)) ≫ (α_ (A ⊗ A) A A).inv) ≫
                        (α_ A A A).hom ▷ A) ≫
                      (A ◁ μ) ▷ A) ≫
                    μ ▷ A) ≫
                  μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j = 𝟙 (𝟙_ C ⊗ limit F) ≫ (λ_ (limit F)).hom ≫ limit.π F j

Tactic:
Category.id_comp

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j = (λ_ (limit F)).hom ≫ limit.π F j
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j = 𝟙 (limit F ⊗ 𝟙_ C) ≫ (ρ_ (limit F)).hom ≫ limit.π F j

Tactic:
Category.id_comp

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j = (ρ_ (limit F)).hom ≫ limit.π F j
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.X ◁ S.X ◁ η ≫ P.X ◁ μ

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (ρ_ (P.X ⊗ S.X)).inv

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ P.X S.X (𝟙_ C)).hom

Tactic:
rw [← whiskerLeft_comp, MonObj.mul_one]

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.X ◁ (ρ_ S.X).hom

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (ρ_ (P.X ⊗ S.X)).inv

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (α_ P.X S.X (𝟙_ C)).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ P.actRight =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight

Tactic:
slice_lhs 2 3 => rw [right_assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ P.X S.X S.X).hom ≫ (α_ P.X S.X S.X).inv ≫ P.actRight ▷ S.X ≫ P.actRight =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ 𝟙 (𝟙_ D) ≫ η.app Y✝ = η.app Y✝

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ η.app Y✝ = η.app Y✝
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
ι : Type w
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, w, v, u} ι C
X : ι → C
hc : ∀ (i : ι), P.ind (X i)
⊢ P.ind (∏ᶜ X)

Tactic:
by
  choose J _ _ pres hpres using hc
  obtain ⟨hc⟩ := IsIPCOfShape.nonempty_isColimit fun i ↦ (pres i).isColimit
  exact ⟨∀ j, J j, inferInstance, inferInstance,
    { diag := _, ι := _, isColimit := hc }, fun i ↦ P.prop_limit _ fun a ↦ hpres a.1 _⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ t.app j ≫ (s ≫ (Functor.const J).map i).app j = f ≫ i

Tactic:
simp [reassoc_of% (hst j).2]

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

Goal state before:
pp: case refine_1.comp
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g : U✝ ⟶ X✝
hg : R g
ih : ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings U✝, ∀ (U : C) (g_1 : U ⟶ U✝), R g_1 → P (g_1 ≫ g ≫ f)

Tactic:
obtain ⟨S, hS, h⟩ := ih

Goal state after:
case refine_1.comp
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g : U✝ ⟶ X✝
hg : R g
S : Presieve X✝
hS : S ∈ K.coverings X✝
h : ∀ (U : C) (g : U ⟶ X✝), S g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings U✝, ∀ (U : C) (g_1 : U ⟶ U✝), R g_1 → P (g_1 ≫ g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ (∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

Tactic:
refine ⟨fun H Z p g hp hpg ↦ ?_, fun H Z g hZ ↦ ?_⟩
    · have : IsFinitelyPresentable (CategoryTheory.Under.mk p) := hp
      obtain ⟨W, u, v, huv, hW⟩ := H (CategoryTheory.Under.homMk (U := CategoryTheory.Under.mk p)
        (V := CategoryTheory.Under.mk f) g hpg)
      use W.right, u.right, v.right, congr($(huv).right)
      rwa [show p ≫ u.right = W.hom from CategoryTheory.Under.w u]
    · obtain ⟨W, u, v, huv, hW⟩ := H Z.hom g.right hZ (CategoryTheory.Under.w g)
      exact ⟨CategoryTheory.Under.mk (Z.hom ≫ u), CategoryTheory.Under.homMk u,
          CategoryTheory.Under.homMk v, by ext; simpa, hW⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f - β.f) ≫ A₂.str = A₁.str ≫ (α.f - β.f)

Tactic:
simp only [Functor.map_sub, sub_comp, Endofunctor.Algebra.Hom.h, comp_sub]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
⊢ o.matrixDecomposition.toFun (w + z) = o.matrixDecomposition.toFun w + o.matrixDecomposition.toFun z

Tactic:
ext
      dsimp [biproduct.components]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w : R
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
⊢ o.matrixDecompositionAddEquiv.toFun (w • z) = (RingHom.id R) w • o.matrixDecompositionAddEquiv.toFun z

Tactic:
ext
      dsimp [biproduct.components]
      simp

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
s : Cocone F
x y : CoconePt hc
⊢ { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ } x ≤
      { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ } y ↔
    x ≤ y

Tactic:
by
    obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y
    have hx := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x'
    have hy := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) y'
    simp only [Functor.mapCocone_pt, Functor.comp_obj, Functor.const_obj_obj,
      CategoryTheory.comp_apply, Functor.mapCocone_ι_app, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, Function.Embedding.coeFn_mk] at hx hy ⊢
    rw [hx, hy, OrderEmbedding.le_iff_le]
    refine ⟨fun h ↦ ⟨j, _, _, rfl, rfl, h⟩, fun ⟨k, x, y, hx', hy', h⟩ ↦ ?_⟩
    obtain ⟨l, f, g, hl⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx'
    obtain ⟨l', f', g', hl'⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy'
    obtain ⟨m, a, b, h₁, h₂⟩ := bowtie f f' g g'
    dsimp at hl hl'
    rw [← (F.map (f ≫ a)).le_iff_le] at h
    rw [← (F.map (g ≫ a)).le_iff_le]
    exact le_of_eq_of_le (by simp [hl]) (le_of_le_of_eq h (by simp [h₁, h₂, hl']))

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : (FintypeCat.of X✝.ι).obj
j✝ : (FintypeCat.of Z✝.ι).obj
⊢ MulOpposite.unop (∑ j, f i✝ j ≫ g j j✝) = ∑ j, MulOpposite.unop (f i✝ j) * MulOpposite.unop (g j j✝)

Tactic:
convert! Finset.unop_sum _ _

Goal state after: