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

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    X₁.right ◁ (Arrow.Hom.left f₂ ▷ X₃.right ≫ Y₂.left ◁ Arrow.Hom.right f₃) ≫
      X₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) ≫
        Arrow.Hom.right f₁ ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)

Tactic:
whisker_exchange,

Goal state after:
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    X₁.right ◁ (Arrow.Hom.left f₂ ▷ X₃.right ≫ Y₂.left ◁ Arrow.Hom.right f₃) ≫
      Arrow.Hom.right f₁ ▷ (Y₂.left ⊗ Y₃.right) ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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 D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c)))

Tactic:
rw [w₂, ← isIso_iff_bijective]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
w₂ :
  (coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c) =
    ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).hom
⊢ IsIso
    (((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op ((L ⋙ R).1 d)) (Opposite.op d'))).hom ≫
      (coyoneda.map (d' ◁ adj.unit.app d).op).app (R.obj c) ≫
        ((yoneda.obj (R.obj c)).mapIso (β_ (Opposite.op d') (Opposite.op ((𝟭 D).1 d)))).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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ X P Q ◁ η ≫ actRight P Q = (ρ_ (X P Q)).hom

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
  dsimp [X]
  slice_lhs 1 2 => rw [← whisker_exchange]
  slice_lhs 2 3 => rw [π_tensor_id_actRight]
  slice_lhs 1 2 => rw [associator_naturality_right]
  slice_lhs 2 3 => rw [← whiskerLeft_comp, actRight_one]
  simp

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ L.obj (R.obj c) ◁ (adj.counit.app X✝ ≫ x✝) ≫ adj.counit.app c ▷ Y✝ =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝

Tactic:
whisker_exchange,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ adj.counit.app c ▷ L.obj (R.obj X✝) ≫ c ◁ (adj.counit.app X✝ ≫ x✝) =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝
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
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ X.X M.X N₁.X).inv ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one =
    (((α_ X.X M.X N₁.X).inv ≫ (X.X ⊗ M.X) ◁ f.hom) ≫ M.actLeft ▷ N₂.X) ≫
      coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)

Tactic:
slice_rhs 2 3 => rw [whisker_exchange]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ X.X M.X N₁.X).inv ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one =
    (α_ X.X M.X N₁.X).inv ≫
      (M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom) ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
by
  have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
  rw [← prod.lift_fst f g, this, prod.lift_snd]

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

Goal state before:
pp: case e_a
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ (β_ (F.obj x) (H.obj z)).hom ▷ G.obj y ≫
      (unit H F).app (z, x) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((β_ z x).hom ▷ y ≫ (α_ x z y).hom ≫ x ◁ (β_ z y).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)

Tactic:
rw [← BraidedCategory.hexagon_forward, ← comp_whiskerRight_assoc]

Goal state after:
case e_a
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ▷ G.obj y ≫
      (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ z x y).hom ≫ (β_ z (x ⊗ y)).hom ≫ (α_ x y z).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ f ≫ (λ_ Y).inv ≫ ((normalizeIso C).hom.app Y).app { as := NormalMonoidalObject.unit } =
    ((λ_ X).inv ≫ ((normalizeIso C).hom.app X).app { as := NormalMonoidalObject.unit }) ≫ eqToHom ⋯

Tactic:
leftUnitor_inv_naturality_assoc,

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.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.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ 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 A).hom

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 ◁ (β_ A A).hom

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 ◁ 𝒮

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

Tactic:
MonObj.one_mul

Goal state after:
case a.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).hom

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

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ 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 A).hom

case 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).hom

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 ◁ 𝒮

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
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = x * z + y * z

Tactic:
by
      convert! μ[A].hom.map_add (x ⊗ₜ z) (y ⊗ₜ z)
      rw [← TensorProduct.add_tmul]
      rfl

Goal state after:
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 G H : J ⥤ C
j : J
| (α_ (limit F) (limit G) (limit H)).hom ≫
    limit F ◁ { pt := limit G ⊗ limit H, π := { app := fun j ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } }.π.app j ≫
      limit.π F j ▷ (G.obj j ⊗ H.obj j)

Tactic:
whisker_exchange,

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 G H : J ⥤ C
j : J
| (α_ (limit F) (limit G) (limit H)).hom ≫
    limit.π F j ▷ (limit G ⊗ limit H) ≫
      F.obj j ◁ { pt := limit G ⊗ limit H, π := { app := fun j ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } }.π.app 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
| (η ▷ R.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.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

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
| (λ_ (R.X ⊗ P.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
| (α_ (𝟙_ C) R.X P.X).inv

Tactic:
MonObj.one_mul

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
| (λ_ R.X).hom ▷ P.X

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.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.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
| (α_ (𝟙_ C) R.X P.X).inv
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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
y : C
⊢ can ▷ F.obj y ≫ (DayConvolution.unit U F).app (𝟙_ C, y) ≫ (leftUnitor U F).hom.app (𝟙_ C ⊗ y) =
    (λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv

Tactic:
by
  have := congrArg (fun t ↦ t.app (.mk PUnit.unit, y)) <|
      (corepresentableByLeft U F).homEquiv.rightInverse_symm <|
        ((leftUnitorCorepresentingIso F).symm.hom.app F) (𝟙 _)
  dsimp [leftUnitor, Coyoneda.fullyFaithful, corepresentableByLeft,
    leftUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso,
    Functor.corepresentableByEquiv] at this ⊢
  simp only [whiskerLeft_id, Category.comp_id] at this
  simp only [Category.comp_id, this]
  simp [prod.leftUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
    Functor.FullyFaithful.homEquiv]
  rfl

Goal state after:
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✝ : ComonObj A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ A.map f ≫ ε = ε

Tactic:
dsimp; rw [ε[A].naturality, tensorUnit_map]; dsimp; rw [Category.comp_id]

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₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (ι C V D).map (f ⊗ₘ f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

Tactic:
by
  apply DayConvolution.corepresentableBy
    (ι C V D |>.obj d₁) (ι C V D |>.obj d₁') |>.homEquiv.injective
  dsimp
  ext ⟨x, y⟩
  simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj,
    DayConvolution.corepresentableBy_homEquiv_apply_app,
    DayConvolution.unit_app_map_app]
  exact convolutionExtensionUnit_comp_ι_map_tensorHom_app C V _ _ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ P.ind f ↔ P.underObj.ind (CategoryTheory.Under.mk f)

Tactic:
refine ⟨fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦ ?_, fun ⟨J, _, _, pres, hpres⟩ ↦ ?_⟩
  · refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
    · exact { app j := CategoryTheory.Under.homMk (s.app j) (by simp [hst]) }
    · have : Nonempty J := IsFiltered.nonempty
      exact Under.isColimitLiftCocone _ _ _ _ (by simp [hst]) hs
    · simp [underObj, hst]
  · refine ⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun j ↦ ⟨?_, ?_⟩⟩
    · exact { app j := (pres.diag.obj j).hom }
    · exact Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)
    · exact isColimitOfPreserves (CategoryTheory.Under.forget _) pres.isColimit
    · exact hpres j
    · simp

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

Goal state before:
pp: case refine_1.of_iso
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✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : R ∈ K.coverings X✝
h : ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings X'✝, ∀ (U : C) (g_1 : U ⟶ X'✝), R g_1 → P (g_1 ≫ g)

Tactic:
rw [K.mem_iff_exists_zeroHypercover] at hR

Goal state after:
case refine_1.of_iso
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✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
e : Arrow.mk f ≅ Arrow.mk g
hf : sourceLocalClosure K P f
R : Presieve X✝
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
⊢ ∃ R ∈ K.coverings X'✝, ∀ (U : C) (g_1 : U ⟶ X'✝), R g_1 → P (g_1 ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_presieve
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✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih : ∀ (U : C) (g : U ⟶ X✝), R g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)

Tactic:
rw [K.mem_iff_exists_zeroHypercover] at hR

Goal state after:
case refine_1.of_presieve
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✝
R : Presieve X✝
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih : ∀ (U : C) (g : U ⟶ X✝), R g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬Nonempty (X ≅ Y)

Tactic:
← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank 𝕜 (X ⟶ Y) = 1
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a,
      ∑ s,
        if h : a = j then
          if h_1 : ⋯ ▸ s = x then if h_2 : a = j' then if h_3 : ⋯ ▸ s = y then eqToHom ⋯ else 0 else 0 else 0
        else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
simp only [if_true, Finset.sum_dite_irrel, Finset.mem_univ,
                Finset.sum_const_zero, Finset.sum_dite_eq']

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (if h : j = j' then if h_1 : ⋯ ▸ x = y then eqToHom ⋯ else 0 else 0) = (if h : j = j' then eqToHom ⋯ else 0) x y