mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
⊢ (∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d) → ∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d

Tactic:
rintro h _ _ g ⟨a, gφS⟩

Goal state after:
case mpr
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
S : Subgroupoid C
T : Subgroupoid D
h : ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
c d : D
c✝ d✝ : C
a : c✝ ⟶ d✝
gφS : a ∈ S.arrows c✝ d✝
⊢ φ.map a ∈ T.arrows (φ.obj c✝) (φ.obj d✝)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
S : Subgroupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
⊢ (map φ hφ S).objs = φ.obj '' S.objs

Tactic:
by
  ext x; convert! mem_map_objs_iff S φ hφ x

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C ⋆ D
f : x.Hom y
⊢ comp x.id f = f

Tactic:
cases x <;> cases y <;> simp only [Hom, id, comp, Category.id_comp] <;> tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
U : FormalCoproduct C
α : Type
inst✝ : HasProductsOfShape α C
s : Fan fun x ↦ U
φ : (i : s.pt.I) → s.pt.obj i ⟶ (U.powerFan α).pt.obj ((fun i a ↦ (s.proj a).f i) i)
hm : ∀ (j : α), { f := fun i a ↦ (s.proj a).f i, φ := φ } ≫ (U.powerFan α).proj j = s.proj j
i : s.pt.I
⊢ { f := fun i a ↦ (s.proj a).f i, φ := φ }.φ i ≫ eqToHom ⋯ =
    { f := fun i a ↦ (s.proj a).f i, φ := fun i ↦ Pi.lift fun a ↦ (s.proj a).φ i }.φ i

Tactic:
· dsimp
        ext a
        specialize hm a
        rw [hom_ext_iff] at hm
        obtain ⟨_, hm⟩ := hm
        simpa using hm i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
i : X.I
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
rw [h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y : FormalCoproduct C
f g : X ⟶ Y
i : X.I
h₁ : f.f i = g.f i
⊢ Y.obj (f.f i) = Y.obj (g.f i)

Tactic:
rw [h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }

Tactic:
let l : s.pt ⟶ G.left.obj i := hcᵢ.lift ⟨_, fun k ↦ (H k f).lift (s.fst ≫ (α.app k).left.app j)
    s.snd (by simp [← s.condition, ← NatTrans.comp_app]), fun k₁ k₂ fk₁k₂ ↦ (H _ f).hom_ext
    (by simp [← NatTrans.naturality, ← NatTrans.comp_app, ← Over.comp_left])
    (by simp [← NatTrans.comp_app])⟩

Goal state after:
J✝ : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : Category.{v_2, u_3} C
inst✝³ : Category.{v_3, u_2} K
inst✝² : Category.{v_4, u_4} D
F : C ⥤ D
inst✝¹ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
hJ : IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ (evaluation C D).obj j).mapCone { pt := G, π := α }) :=
  isLimitOfPreserves (Over.forget F ⋙ (evaluation C D).obj j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1, π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
⊢ { l //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
⊢ ((whiskeringRight (Discrete J) C D).obj L).IsLocalization (W.functorCategory (Discrete J))

Tactic:
let L₁ := Functor.pi (fun (_ : J) => L)

Goal state after:
J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
⊢ ((whiskeringRight (Discrete J) C D).obj L).IsLocalization (W.functorCategory (Discrete J))
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case comp
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g✝ g'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝¹ : HomEquiv f✝ f'✝
a✝ : HomEquiv g✝ g'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
hg : projectMapAux f✝¹ g✝ = projectMapAux f✝¹ g'✝
⊢ projectMapAux f✝¹ (f✝.comp g✝) = projectMapAux f✝¹ (f'✝.comp g'✝)

Tactic:
dsimp only [projectMapAux]; rw [hf, hg]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
⊢ ∀ {X' X : C} {Y : Over I} (f : X' ⟶ X) (g : X ⟶ (sections I).obj Y),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (f ≫ g) =
      (toOver I).map f ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm g

Tactic:
intro A' A X g v
    dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]
    simp only [toOver_map]
    rw [← Over.homMk_comp]
    congr 1
    simp [uncurry_natural_left]

Goal state after:
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✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ ((comparisonAdjunction adj).unit.app A).f = (beckCoequalizer A).desc (unitCofork A)

Tactic:
apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A)

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✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ (beckCofork A).π ≫ ((comparisonAdjunction adj).unit.app A).f =
    (beckCofork A).π ≫ (beckCoequalizer A).desc (unitCofork A)
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₃) ≫
      Arrow.Hom.right f₁ ▷ (Y₂.left ⊗ Y₃.right) ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)

Tactic:
whisker_exchange_assoc,

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) =
    Arrow.Hom.right f₁ ▷ (X₂.left ⊗ X₃.right) ≫
      Y₁.right ◁ (Arrow.Hom.left f₂ ▷ X₃.right ≫ Y₂.left ◁ Arrow.Hom.right f₃) ≫
        Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)
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 X₃.right).inv ≫
      (X₁.right ⊗ X₂.left) ◁ Arrow.Hom.right f₃ ≫
        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) =
    Arrow.Hom.right f₁ ▷ (X₂.left ⊗ X₃.right) ≫
      Y₁.right ◁ (X₂.left ◁ Arrow.Hom.right f₃ ≫ Arrow.Hom.left f₂ ▷ Y₃.right) ≫
        Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)

Tactic:
whisker_exchange_assoc,

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 X₃.right).inv ≫
      Arrow.Hom.right f₁ ▷ X₂.left ▷ X₃.right ≫
        (Y₁.right ⊗ X₂.left) ◁ Arrow.Hom.right f₃ ≫
          (α_ 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) =
    Arrow.Hom.right f₁ ▷ (X₂.left ⊗ X₃.right) ≫
      Y₁.right ◁ (X₂.left ◁ Arrow.Hom.right f₃ ≫ Arrow.Hom.left f₂ ▷ Y₃.right) ≫
        Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
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
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)
| R.X ◁ P.actRight ▷ Q.X ≫ (α_ R.X P.X Q.X).inv

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
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)
| P.actLeft ▷ Q.X

Tactic:
associator_inv_naturality_middle

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

case a
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)
| P.actLeft ▷ Q.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.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)
| R.X ◁ P.actLeft ▷ Q.X ≫ (α_ R.X P.X Q.X).inv

pp: case a.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)
| P.actLeft ▷ Q.X

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)
| 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)
| (α_ R.X R.X (P.X ⊗ Q.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)
| R.X ◁ (α_ R.X P.X Q.X).inv

Tactic:
associator_inv_naturality_middle

Goal state after:
case a.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)
| (α_ R.X (R.X ⊗ P.X) Q.X).inv ≫ (R.X ◁ P.actLeft) ▷ Q.X

case a.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)
| P.actLeft ▷ Q.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)
| 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)
| (α_ R.X R.X (P.X ⊗ Q.X)).hom

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)
| R.X ◁ (α_ R.X P.X Q.X).inv
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
Y : C
inst✝¹ : ModObj M Y
f : X ⟶ Y
inst✝ : IsModHom M f
Z : C
m : Z ⟶ M
x : Z ⟶ X
⊢ (m • x) ≫ f = m • x ≫ f

Tactic:
by
  simp [Hom.smul_def, Category.assoc, IsModHom.smul_hom]

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
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'))
| (∀ (c : C) (d c_1 : D), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op c_1))) ↔
    ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))

Tactic:
rhs

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), IsIso (L.map (adj.unit.app d ▷ d'))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ eHomWhiskerLeft C X g = (ihom X).map g

Tactic:
change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _
  rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))).inv ≫
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
          end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k ▷
              end_ (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) ≫
            ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
                end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k ≫
              eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
                ((Under.forget j ⋙ F₃').obj k)

Tactic:
whisker_exchange_assoc,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))).inv ≫
        end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k ▷ 𝟙_ C ≫
          ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
            ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
                end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k ≫
              eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
                ((Under.forget j ⋙ F₃').obj k)
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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| X.X ◁ f.hom ▷ N.X ≫ (α_ X.X M₂.X N.X).inv

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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| M₂.actLeft ▷ N.X

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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)

Tactic:
associator_inv_naturality_middle

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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| (α_ X.X M₁.X N.X).inv ≫ (X.X ◁ f.hom) ▷ N.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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| M₂.actLeft ▷ N.X

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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
| coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)