mathlib-initiative/mathlib-tactics huggingface dataset:
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)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
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₂ :
  ⇑(ConcreteCategory.hom ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d'))) =
    ⇑((ihom.adjunction d).homEquiv d' (R.obj c)) ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑((ihom.adjunction ((L ⋙ R).obj d)).homEquiv d' (R.obj c)).symm
⊢ IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d')) ↔
    IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
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)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
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₂ :
  ⇑(ConcreteCategory.hom ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d'))) =
    ⇑((ihom.adjunction d).homEquiv d' (R.obj c)) ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑((ihom.adjunction ((L ⋙ R).obj d)).homEquiv d' (R.obj c)).symm
⊢ Function.Bijective
      ⇑(ConcreteCategory.hom ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d'))) ↔
    IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)
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 T : Mon C
P : Bimod R S
Q : Bimod S T
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.actLeft ▷ Q.X ▷ T.X ≫ (α_ P.X Q.X T.X).hom

pp: case a.a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

pp: case a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X P.X Q.X).inv ▷ T.X

Tactic:
associator_naturality_left

Goal state after:
case a.a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ (R.X ⊗ P.X) Q.X T.X).hom ≫ P.actLeft ▷ (Q.X ⊗ T.X)

case a.a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ Q.actRight

case a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X P.X Q.X).inv ▷ T.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ▷ T.X ≫
    (α_ R.X (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X).hom

pp: case a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ actRight P Q

pp: case a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actLeft P Q

Tactic:
associator_naturality_middle

Goal state after:
case a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| (α_ R.X (P.X ⊗ Q.X) T.X).hom ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X

case a.a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| R.X ◁ actRight P Q

case a
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₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| actLeft P Q
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 A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((curriedTensor C).map f))
⊢ ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((tensoringLeft D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((tensoringLeft C).map f))

Tactic:
← vcomp1,

Goal state after:
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 A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((curriedTensor C).map f))
⊢ (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((tensoringLeft C).map f))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
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
| P.actRight ▷ Q.X ▷ L.X ≫ (α_ P.X Q.X L.X).hom

pp: case a.a
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
| P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)

pp: case a
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
| coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
    ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
      P.X ◁ TensorBimod.actLeft Q L)

Tactic:
associator_naturality_left

Goal state after:
case a.a
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
| (α_ (P.X ⊗ S.X) Q.X L.X).hom ≫ P.actRight ▷ (Q.X ⊗ L.X)

case a.a
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
| P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)

case a
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
| coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
    ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
      P.X ◁ TensorBimod.actLeft Q L)
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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.map
      (i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                      𝟙 (i.obj X')))) ≫
            𝟙 (i.obj X'))) =
    i.map
      (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)) ≫
        g)

Tactic:
rw [Functor.FullyFaithful.map_preimage, i.map_comp,
    Adjunction.homEquiv_unit, Adjunction.homEquiv_unit]

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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
      uncurry
          ((unitCompPartialBijective B ⋯)
            (curry
              ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                uncurry
                    ((unitCompPartialBijective A ⋯)
                      (curry
                        ((β_ A B).inv ≫ ((reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map (f ≫ g)) ≫ 𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X') =
    i.map
        (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry
                              ((β_ A B).inv ≫ ((reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map f) ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X))) ≫
      i.map g
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 : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
⊢ Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j =
    ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c))

Tactic:
Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c)

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j : C
⊢ ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c)) = ℌ.π c j ≫ (ihom (F.obj j)).map (f.app (j ⊗ c))
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ X' ◁ f ≫ (normalizeIsoApp' C (X' ⊗ Y) n).hom =
    (normalizeIsoApp' C (X' ⊗ X) n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
dsimp only [normalizeObj_tensor, normalizeIsoApp'_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]

Goal state after:
C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ X' ◁ f ≫
      (α_ (inclusionObj n) X' Y).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ Y ≫ (normalizeIsoApp' C Y (X'.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ h ▷ η' ≫ (normalizeIsoApp' C (Y ⊗ η') n).hom =
    (normalizeIsoApp' C (X ⊗ η') n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
dsimp only [normalizeObj_tensor, normalizeIsoApp'_tensor, Iso.trans_hom,
      Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]

Goal state after:
C : Type u
X✝ Y✝ X Y : F C
h : X ⟶ Y
η' : F C
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ h ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ inclusionObj n ◁ h ▷ η' ≫
      (α_ (inclusionObj n) Y η').inv ≫
        (normalizeIsoApp' C Y n).hom ▷ η' ≫ (normalizeIsoApp' C η' (Y.normalizeObj n)).hom =
    ((α_ (inclusionObj n) X η').inv ≫
        (normalizeIsoApp' C X n).hom ▷ η' ≫ (normalizeIsoApp' C η' (X.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)
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
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
pres : (i : ι) → ColimitPresentation (J i) (X i)
hpres : ∀ (i : ι) (i_1 : J i), P ((pres i).diag.obj i_1)
hc : IsColimit (coconePointwiseProduct fun i ↦ { pt := X i, ι := (pres i).ι })
⊢ P.ind (∏ᶜ X)

Tactic:
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.LocalClosure

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
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 : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h : IsPullback fst snd (g' ≫ f') g
⊢ snd ≫ g = (fst ≫ g') ≫ f'

Tactic:
simp [h.w.symm]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ IsNoetherianObject X

Tactic:
rw [isNoetherianObject_iff_monotone_chain_condition]
  have := Subobject.subsingleton_of_isZero hX
  intro f
  exact ⟨0, fun m hm ↦ Subsingleton.elim _ _⟩

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

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : ¬IsIso (End.of f - (algebraMap 𝕜 (End X)) c)
⊢ c • 𝟙 X = f

Tactic:
isIso_iff_nonzero,

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
id_nonzero : 𝟙 X ≠ 0
f : X ⟶ X
this✝ : Nontrivial (End X)
this : FiniteDimensional 𝕜 (End X)
c : 𝕜
nu : ¬End.of f - (algebraMap 𝕜 (End X)) c ≠ 0
⊢ c • 𝟙 X = f