mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
⊢ ∀ (X_1 : CatCommSqOver F G X),
    { fst := whiskerRight (𝟙 X_1).fst ψ.left, snd := whiskerRight (𝟙 X_1).snd ψ.right, w := ⋯ } =
      𝟙
        { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
          iso :=
            X_1.fst.associator ψ.left F₁ ≪≫
              X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                (X_1.fst.associator F ψ.base).symm ≪≫
                  isoWhiskerRight X_1.iso ψ.base ≪≫
                    X_1.snd.associator G ψ.base ≪≫
                      X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                        (X_1.snd.associator ψ.right G₁).symm }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
⊢ ∀ {X_1 Y Z : CatCommSqOver F G X} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := ⋯ } =
      { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ } ≫
        { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, w := ⋯ }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
⊢ ∀ (X_1 : CatCospanTransform F G F₁ G₁),
    {
        app := fun S ↦
          { fst := { app := fun y ↦ (𝟙 X_1).left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ (𝟙 X_1).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } =
      𝟙
        {
          obj := fun S ↦
            { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
              iso :=
                S.fst.associator X_1.left F₁ ≪≫
                  S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                    (S.fst.associator F X_1.base).symm ≪≫
                      isoWhiskerRight S.iso X_1.base ≪≫
                        S.snd.associator G X_1.base ≪≫
                          S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                            (S.snd.associator X_1.right G₁).symm },
          map := fun {x y} f ↦ { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
          map_id := ⋯, map_comp := ⋯ }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
⊢ ∀ {X_1 Y Z : CatCospanTransform F G F₁ G₁} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    {
        app := fun S ↦
          { fst := { app := fun y ↦ (f ≫ g).left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ (f ≫ g).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } =
      {
          app := fun S ↦
            { fst := { app := fun y ↦ f.left.app (S.fst.obj y), naturality := ⋯ },
              snd := { app := fun y ↦ f.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
          naturality := ⋯ } ≫
        {
          app := fun S ↦
            { fst := { app := fun y ↦ g.left.app (S.fst.obj y), naturality := ⋯ },
              snd := { app := fun y ↦ g.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
          naturality := ⋯ }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
⊢ ∀ (X_1 : CatCommSqOver F G Y),
    { fst := U.whiskerLeft (𝟙 X_1).fst, snd := U.whiskerLeft (𝟙 X_1).snd, w := ⋯ } =
      𝟙
        { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
          iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
⊢ ∀ {X_1 Y_1 Z : CatCommSqOver F G Y} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { fst := U.whiskerLeft (f ≫ g).fst, snd := U.whiskerLeft (f ≫ g).snd, w := ⋯ } =
      { fst := U.whiskerLeft f.fst, snd := U.whiskerLeft f.snd, w := ⋯ } ≫
        { fst := U.whiskerLeft g.fst, snd := U.whiskerLeft g.snd, w := ⋯ }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
⊢ ∀ (X_1 : X ⥤ Y),
    { app := fun x ↦ { fst := whiskerRight (𝟙 X_1) x.fst, snd := whiskerRight (𝟙 X_1) x.snd, w := ⋯ },
        naturality := ⋯ } =
      𝟙
        {
          obj := fun S ↦
            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
              iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm },
          map := fun {S S'} φ ↦ { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ }

Tactic:
intros; ext <;> simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
⊢ ∀ {X_1 Y_1 Z : X ⥤ Y} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { app := fun x ↦ { fst := whiskerRight (f ≫ g) x.fst, snd := whiskerRight (f ≫ g) x.snd, w := ⋯ },
        naturality := ⋯ } =
      { app := fun x ↦ { fst := whiskerRight f x.fst, snd := whiskerRight f x.snd, w := ⋯ }, naturality := ⋯ } ≫
        { app := fun x ↦ { fst := whiskerRight g x.fst, snd := whiskerRight g x.snd, w := ⋯ }, naturality := ⋯ }

Tactic:
intros; ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f = ε

Tactic:
← Category.comp_id f,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f ≫ 𝟙 (𝟙_ C) = ε
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: 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✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso ((comparisonAdjunction adj).unit.app X)

Tactic:
apply
        @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget adj.toMonad) ?_ _

Goal state after:
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✝² : HasReflexiveCoequalizers D
inst✝¹ : G.ReflectsIsomorphisms
inst✝ : PreservesColimitOfIsReflexivePair G
X : adj.toMonad.Algebra
⊢ IsIso (adj.toMonad.forget.map ((comparisonAdjunction adj).unit.app X))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits

Goal state before:
pp: J : Type w
inst✝² : Category.{v_1, w} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
F : J ⥤ Mon C
c : Cone (F ⋙ forget C)
hc : IsLimit c
⊢ hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ▷ c.pt ≫
      hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } =
    (α_ c.pt c.pt c.pt).hom ≫
      c.pt ◁ hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ≫
        hc.lift { pt := c.1 ⊗ c.1, π := { app := fun X ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } }

Tactic:
by
    apply hc.hom_ext
    simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsLimit.fac,
      mon_tauto, implies_true]

Goal state after:
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))))
this✝ : η.app (A ⟹ i.obj B) ≫ q = 𝟙 (A ⟹ i.obj B)
this : IsSplitMono (η.app (A ⟹ i.obj B))
⊢ i.essImage (A ⟹ i.obj B)

Tactic:
apply mem_essImage_of_unit_isSplitMono

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

Goal state before:
pp: case comm1.refine_1
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
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B X : D
⊢ (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X

Tactic:
haveI :=
              Adjunction.rightAdjoint_preservesLimits.{0, 0} (reflectorAdjunction i)
            apply asIso (prodComparison i B X)

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

Goal state before:
pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (η ▷ A ≫ (β_ A A).hom)

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (λ_ A).inv

Tactic:
BraidedCategory.braiding_naturality_left

Goal state after:
case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ ((β_ (𝟙_ C) A).hom ≫ A ◁ η)

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ 𝒮 ▷ A

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).inv

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ ▷ A

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (λ_ A).inv
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (mul' R ↑A)
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑A) 1) x)) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑A) 1) x)

Tactic:
LinearMap.mul'_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(Algebra.linearMap R ↑A))) (1, x).1 * LinearMap.id (1, x).2 =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑A) 1) x)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (mul' R ↑A)
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A))))
        (((TensorProduct.mk R ↑A ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)) =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑A ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)

Tactic:
LinearMap.mul'_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ LinearMap.id (x, 1).1 * (Hom.hom (↟(Algebra.linearMap R ↑A))) (x, 1).2 =
    (Hom.hom (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑A ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R))) x) 1)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))

Tactic:
LinearMap.mul'_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A))) (x ⊗ₜ[R] y, z).1 * LinearMap.id (x ⊗ₜ[R] y, z).2 =
    (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
        ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
          (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)))
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : Mon (ModuleCat R)
⊢ Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) =
    Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ)

Tactic:
refine TensorProduct.ext ?_

Goal state after:
R : Type u
inst✝ : CommRing R
A : Mon (ModuleCat R)
⊢ (TensorProduct.mk R ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
          ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X).compr₂ₛₗ
      (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })) =
    (TensorProduct.mk R ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
          ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X).compr₂ₛₗ
      (Hom.hom
        (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
            (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
          μ))
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P₁ P₂ : MorphismProperty C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
⊢ (P₁ ⊔ P₂).HasCardinalLT κ

Tactic:
by
  dsimp only [MorphismProperty.HasCardinalLT]
  rw [MorphismProperty.toSet_max]
  exact hasCardinalLT_union hκ h₁ h₂

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

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
D : Type u₃
inst✝⁴ : Category.{v₃, u₃} D
inst✝³ : MonoidalCategoryStruct D
inst✝² : LawfulDayConvolutionMonoidalCategoryStruct C V D
d d' d'' : D
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
⊢ (ι C V D).map (α_ d d' d'').hom =
    (DayConvolution.associator ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).hom

Tactic:
apply corepresentableBy₂'
    (ι C V D |>.obj d) (ι C V D |>.obj d') (ι C V D |>.obj d'') |>.homEquiv.injective
  dsimp
  ext ⟨⟨x, y⟩, z⟩
  simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, Functor.prod_obj,
    tensor_obj, Functor.id_obj, Functor.homEquivOfIsLeftKanExtension_apply_app,
    externalProductBifunctor_map_app, Functor.leftUnitor_inv_app, whiskerLeft_id,
    Category.comp_id, corepresentableBy_homEquiv_apply_app,
    DayConvolution.associator_hom_unit_unit]
  exact associator_hom_unit_unit V _ _ _ _ _ _

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

Goal state before:
pp: case refine_2.refine_3
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ IsColimit { pt := Y, ι := Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X) }

pp: case refine_2.refine_4
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P ({ app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j)

pp: case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f

Tactic:
· exact isColimitOfPreserves (CategoryTheory.Under.forget _) pres.isColimit

Goal state after:
case refine_2.refine_4
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P ({ app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j)

case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f
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✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
i : ι
⊢ o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i * o.matrixDecomposition z i

Tactic:
ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩

Goal state after:
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✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property : a ∈ f ⁻¹' {h c}
⊢ o.matrixDecomposition (z ≫ w) (h c) ⟨c, ⋯⟩ ⟨a, j_property⟩ =
    (o.matrixDecomposition w (h c) * o.matrixDecomposition z (h c)) ⟨c, ⋯⟩ ⟨a, j_property⟩
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
X : C
inst✝¹ : IsCardinalPresentable X κ
inst✝ : G.IsCardinalAccessible κ
⊢ IsCardinalPresentable (F.obj X) κ

Tactic:
rw [isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj.{v}]
  exact Functor.isCardinalAccessible_of_natIso
    (show G ⋙ _ ≅ _ from (Adjunction.compUliftCoyonedaIso.{0} adj).symm.app (op X)) κ

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ P.map F ≤ isCardinalPresentable D κ

Tactic:
rintro Y ⟨X, hX, ⟨e⟩⟩

Goal state after:
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
⊢ isCardinalPresentable D κ Y
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
D₁ D₂ : Diagram J κ
⊢ ∀ {i j : J} {f : i ⟶ j}, (D₁.W ⊔ D₂.W) f → (D₁.P ⊔ D₂.P) j

Tactic:
by
    rintro _ _ _ (h | h)
    · exact Or.inl (D₁.tgt h)
    · exact Or.inr (D₂.tgt h)

Goal state after: