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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
d₁✝ d₂✝ : Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
f : unop d₂✝ ⟶ unop d₁✝
g : unop c₂✝ ⟶ unop c₁✝
h : unop c₄✝ ⟶ unop c₃✝
⊢ (Quiver.Hom.unop (op f) ⊙ᵣₘ (op g ⊗ₘ op h).unop).op ≫ (αᵣ (unop d₂✝) (unop c₂✝) (unop c₄✝)).symm.op.hom =
    (αᵣ (unop d₁✝) (unop c₁✝) (unop c₃✝)).symm.op.hom ≫
      ((Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop ⊙ᵣₘ Quiver.Hom.unop (op h)).op

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
d₁✝ d₂✝ : Dᵒᵖ
c₁✝ c₂✝ c₃✝ c₄✝ : Cᵒᵖ
f : unop d₂✝ ⟶ unop d₁✝
g : unop c₂✝ ⟶ unop c₁✝
h : unop c₄✝ ⟶ unop c₃✝
⊢ ((Quiver.Hom.unop (op f) ⊙ᵣₘ (op g ⊗ₘ op h).unop).op ≫ (αᵣ (unop d₂✝) (unop c₂✝) (unop c₄✝)).symm.op.hom).unop =
    ((αᵣ (unop d₁✝) (unop c₁✝) (unop c₃✝)).symm.op.hom ≫
        ((Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)).op.unop ⊙ᵣₘ Quiver.Hom.unop (op h)).op).unop
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
d✝ d'✝ : Dᵒᵖ
x✝ : d✝ ⟶ d'✝
⊢ (ρᵣ (unop d✝)).symm.op.hom ≫ x✝ = (x✝.unop ⊵ᵣ unop (𝟙_ Cᵒᵖ)).op ≫ (ρᵣ (unop d'✝)).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
d✝ d'✝ : Dᵒᵖ
x✝ : d✝ ⟶ d'✝
⊢ ((ρᵣ (unop d✝)).symm.op.hom ≫ x✝).unop = ((x✝.unop ⊵ᵣ unop (𝟙_ Cᵒᵖ)).op ≫ (ρᵣ (unop d'✝)).symm.op.hom).unop
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝⁴ x✝³ x✝² : Cᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).unop).op =
    (αᵣ (unop x✝) (unop x✝⁴) (unop x✝³)).symm.op.hom ≫
      (unop (op (unop x✝ ⊙ᵣ unop x✝⁴)) ⊴ᵣ x✝¹.unop).op ≫ (αᵣ (unop x✝) (unop x✝⁴) (unop x✝²)).symm.op.inv

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝⁴ x✝³ x✝² : Cᵒᵖ
x✝¹ : x✝³ ⟶ x✝²
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (x✝⁴ ◁ x✝¹).unop).op.unop =
    ((αᵣ (unop x✝) (unop x✝⁴) (unop x✝³)).symm.op.hom ≫
        (unop (op (unop x✝ ⊙ᵣ unop x✝⁴)) ⊴ᵣ x✝¹.unop).op ≫ (αᵣ (unop x✝) (unop x✝⁴) (unop x✝²)).symm.op.inv).unop
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.unop).op ≫
      (αᵣ (unop x✝) (unop x✝³) (unop (x✝² ⊗ x✝¹))).symm.op.hom ≫
        (αᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝³))) (unop x✝²) (unop x✝¹)).symm.op.hom =
    (αᵣ (unop x✝) (unop (x✝³ ⊗ x✝²)) (unop x✝¹)).symm.op.hom ≫
      ((αᵣ (unop x✝) (unop x✝³) (unop x✝²)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝³ x✝² x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ ((unop x✝ ⊴ᵣ (α_ x✝³ x✝² x✝¹).hom.unop).op ≫
        (αᵣ (unop x✝) (unop x✝³) (unop (x✝² ⊗ x✝¹))).symm.op.hom ≫
          (αᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝³))) (unop x✝²) (unop x✝¹)).symm.op.hom).unop =
    ((αᵣ (unop x✝) (unop (x✝³ ⊗ x✝²)) (unop x✝¹)).symm.op.hom ≫
        ((αᵣ (unop x✝) (unop x✝³) (unop x✝²)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op).unop
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (λ_ x✝¹).hom.unop).op =
    (αᵣ (unop x✝) (unop (𝟙_ Cᵒᵖ)) (unop x✝¹)).symm.op.hom ≫ ((ρᵣ (unop x✝)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (λ_ x✝¹).hom.unop).op.unop =
    ((αᵣ (unop x✝) (unop (𝟙_ Cᵒᵖ)) (unop x✝¹)).symm.op.hom ≫ ((ρᵣ (unop x✝)).symm.op.hom.unop ⊵ᵣ unop x✝¹).op).unop
Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (ρ_ x✝¹).hom.unop).op =
    (αᵣ (unop x✝) (unop x✝¹) (unop (𝟙_ Cᵒᵖ))).symm.op.hom ≫ (ρᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝¹)))).symm.op.hom

Tactic:
apply Quiver.Hom.unop_inj

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalRightAction C D
x✝¹ : Cᵒᵖ
x✝ : Dᵒᵖ
⊢ (unop x✝ ⊴ᵣ (ρ_ x✝¹).hom.unop).op.unop =
    ((αᵣ (unop x✝) (unop x✝¹) (unop (𝟙_ Cᵒᵖ))).symm.op.hom ≫ (ρᵣ (unop (op (unop x✝ ⊙ᵣ unop x✝¹)))).symm.op.hom).unop
Module: Mathlib.CategoryTheory.Monoidal.Bimon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon C
⊢ Δ.hom ≫ ε.hom ▷ M.X.X = (λ_ M.X.X).inv

Tactic:
rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]

Goal state after:
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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
this : adj.unit.app d ⊗ₘ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'
⊢ IsIso (L.map (adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'))

Tactic:
map_comp

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
x✝ : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
h : ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d')) := x✝
h' : ∀ (d d' : D), IsIso (L.map (d ◁ adj.unit.app d'))
d d' : D
this : adj.unit.app d ⊗ₘ adj.unit.app d' = adj.unit.app d ▷ d' ≫ (L ⋙ R).obj d ◁ adj.unit.app d'
⊢ IsIso (L.map (adj.unit.app d ▷ d') ≫ L.map ((L ⋙ R).obj d ◁ adj.unit.app d'))
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
⊢ { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ } ≫ { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ } =
    𝟙 P

Tactic:
by ext; dsimp; rw [Iso.hom_inv_id]

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
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₁} (tensorLeft X)
⊢ (tensorLeft R.X).map ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X =
    ((α_ R.X (P.X ⊗ S.X) Q.X).inv ≫ (α_ R.X P.X S.X).inv ▷ Q.X ≫ P.actLeft ▷ S.X ▷ Q.X) ≫
      (α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft

Tactic:
by
          dsimp
          slice_lhs 1 1 => rw [whiskerLeft_comp]
          slice_lhs 2 3 => rw [associator_inv_naturality_right]
          slice_lhs 3 4 => rw [whisker_exchange]
          simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ (Function.Bijective fun x ↦ x ≫ leftSMul M X) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y

Tactic:
rw [← Function.Bijective.of_comp_iff _ liftEquiv.bijective, Function.bijective_iff_existsUnique]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ (∀ (b : Z ⟶ X ⊗ X), ∃! a, ((fun x ↦ x ≫ leftSMul M X) ∘ ⇑liftEquiv) a = b) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ uncurry ((expComparison F A).natTrans.app B) = inv (prodComparison F A ((ihom A).obj B)) ≫ F.map ((ihom.ev A).app B)

Tactic:
rw [uncurry_eq, expComparison_ev]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
⊢ σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ

Tactic:
RingObj.add_mul R

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
⊢ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
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)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (tensorLeft P.X).map (Q.actRight ▷ L.X) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
            ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) =
    (tensorLeft P.X).map ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
            ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)

Tactic:
dsimp; dsimp [TensorBimod.X]
        slice_lhs 1 2 => rw [associator_inv_naturality_middle]
        rw [← Iso.inv_hom_id_assoc (α_ _ _ _) (P.X ◁ Q.actRight), comp_whiskerRight]
        slice_lhs 3 4 =>
          rw [← comp_whiskerRight, Category.assoc, ← TensorBimod.π_tensor_id_actRight,
            comp_whiskerRight]
        slice_lhs 4 5 => rw [coequalizer.condition]
        slice_lhs 3 4 => rw [associator_naturality_left]
        slice_rhs 1 2 => rw [whiskerLeft_comp]
        slice_rhs 2 3 => rw [associator_inv_naturality_right]
        slice_rhs 3 4 => rw [whisker_exchange]
        simp

Goal state after:
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)
| R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
    (PreservesCoequalizer.iso (tensorLeft R.X) (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
      colimMap
          (parallelPairHom (R.X ◁ μ ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (μ ▷ P.X)
            ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
            ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ μ ▷ R.X ▷ P.X) ((α_ R.X R.X P.X).inv ≫ μ ▷ P.X)
            ⋯ ⋯) ≫
        coequalizer.desc P.actLeft ⋯

Tactic:
rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]

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)
| ((α_ R.X R.X P.X).inv ≫ μ ▷ P.X) ≫ P.actLeft
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
F G : C ⥤ V
inst✝¹⁴ : DayConvolution F G
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)
inst✝¹¹ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
H K : C ⥤ V
inst✝¹⁰ : DayConvolution G H
inst✝⁹ : DayConvolution (F ⊛ G) H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution H K
inst✝⁶ : DayConvolution G (H ⊛ K)
inst✝⁵ : DayConvolution (G ⊛ H) K
inst✝⁴ : DayConvolution ((F ⊛ G) ⊛ H) K
inst✝³ : DayConvolution (F ⊛ G) (H ⊛ K)
inst✝² : DayConvolution (F ⊛ G ⊛ H) K
inst✝¹ : DayConvolution F (G ⊛ H ⊛ K)
inst✝ : DayConvolution F ((G ⊛ H) ⊛ K)
⊢ map (associator F G H).hom (𝟙 K) ≫ (associator F (G ⊛ H) K).hom ≫ map (𝟙 F) (associator G H K).hom =
    (associator (F ⊛ G) H K).hom ≫ (associator F G (H ⊛ K)).hom

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension (α := unit ((F ⊛ G) ⊛ H) K)

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : MonoidalCategory V
F G : C ⥤ V
inst✝¹⁴ : DayConvolution F G
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)
inst✝¹¹ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
H K : C ⥤ V
inst✝¹⁰ : DayConvolution G H
inst✝⁹ : DayConvolution (F ⊛ G) H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution H K
inst✝⁶ : DayConvolution G (H ⊛ K)
inst✝⁵ : DayConvolution (G ⊛ H) K
inst✝⁴ : DayConvolution ((F ⊛ G) ⊛ H) K
inst✝³ : DayConvolution (F ⊛ G) (H ⊛ K)
inst✝² : DayConvolution (F ⊛ G ⊛ H) K
inst✝¹ : DayConvolution F (G ⊛ H ⊛ K)
inst✝ : DayConvolution F ((G ⊛ H) ⊛ K)
⊢ unit ((F ⊛ G) ⊛ H) K ≫
      (tensor C).whiskerLeft
        (map (associator F G H).hom (𝟙 K) ≫ (associator F (G ⊛ H) K).hom ≫ map (𝟙 F) (associator G H K).hom) =
    unit ((F ⊛ G) ⊛ H) K ≫ (tensor C).whiskerLeft ((associator (F ⊛ G) H K).hom ≫ (associator F G (H ⊛ K)).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)
| R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
    (PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
      colimMap
          (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)) (P.actRight ▷ S.X)
            ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
            ((α_ R.X (P.X ⊗ S.X) S.X).inv ≫ (α_ R.X P.X S.X).inv ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X)
            ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ⋯ ⋯) ≫
        coequalizer.desc P.actRight ⋯

Tactic:
rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]

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)
| ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ≫ P.actRight
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
X₁ : C₁
hX₁ : Q₁ X₁
e₁ : f.left ≅ X₁
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f

Tactic:
obtain ⟨X₂, hX₂, ⟨e₂⟩⟩ := h₂' _ hf.2

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
X₁ : C₁
hX₁ : Q₁ X₁
e₁ : f.left ≅ X₁
X₂ : C₂
hX₂ : Q₂ X₂
e₂ : f.right ≅ X₂
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : R ∈ K.coverings X
Y : C
f : Y ⟶ X
hf : R f
hX : P X
⊢ P Y

Tactic:
rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
Y : C
f : Y ⟶ X
hf : R f
hX : P X
⊢ P Y
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : R ∈ K.coverings X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
⊢ P X

Tactic:
rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y
⊢ P X
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g✝¹ : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
w : Arrow V
g✝ : v ⟶ w
h : RightHomotopy (f ≫ g✝) 0
A✝ : RightFreyd V
g : v ⟶ A✝.as
hg : (quotient V).map f ≫ (quotient V).map g = 0
⊢ (quotient V).map (π f) ≫ (quotient V).map (desc f g (homotopyOfEq (f ≫ g) 0 hg)) = (quotient V).map g

Tactic:
by simp [← Functor.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
⊢ (fun x x_1 ↦ 𝟙 x✝) = 𝟙 { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ }

Tactic:
ext ⟨⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
x✝ : C
j✝ : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ }.ι
⊢ 𝟙 x✝ = 𝟙 { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ x✝ } PUnit.unit j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (fun x x_1 ↦ x✝¹ ≫ x✝) = (fun x x_1 ↦ x✝¹) ≫ fun x x_1 ↦ x✝

Tactic:
ext ⟨⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
j✝ : { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun x ↦ Z✝ }.ι
⊢ x✝¹ ≫ x✝ = ((fun x x_1 ↦ x✝¹) ≫ fun x x_1 ↦ x✝) PUnit.unit j✝
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : (fun g ↦ toSucc W Z ≫ g) φ₁ = (fun g ↦ toSucc W Z ≫ g) φ₂
⊢ φ₁ = φ₂

Tactic:
ext ⟨⟩

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : (fun g ↦ toSucc W Z ≫ g) φ₁ = (fun g ↦ toSucc W Z ≫ g) φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ f ≫ toSucc W Z = 𝟙 (succ W Z)

Tactic:
ext ⟨⟩

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ToType X → J
a : (x : ToType X) → j ⟶ k x
hk : ∀ (x : ToType X), (hom (F.map (a x))) ((hom f) x) = (hom (F.map (a x))) ((hom g) x)
φ : X → (j ⟶ IsCardinalFiltered.max k hX) := fun x ↦ a x ≫ IsCardinalFiltered.toMax k hX x
x : ToType X
⊢ a x ≫ (fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX) x = IsCardinalFiltered.toCoeq φ hX

Tactic:
simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x

Goal state after: