mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: G : Type u
inst✝ : Group G
X Y : Action FintypeCat G
f : X ⟶ Y
g : G
y : (FintypeCat.imageComplement f.hom).obj
x : (fun X ↦ X.obj) X.V
h : (ConcreteCategory.hom f.hom) x = (ConcreteCategory.hom (Y.ρ g).hom) ↑y
⊢ (ConcreteCategory.hom (X.ρ g⁻¹ ≫ f.hom)) x = (ConcreteCategory.hom (Y.ρ g⁻¹ * Y.ρ g).hom) ↑y

Tactic:
by rw [f.comm, FintypeCat.comp_apply, h]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: case refine_1
G : Type u
inst✝² : Group G
X : FintypeCat
inst✝¹ : MulAction G X.obj
inst✝ : MulAction.IsPretransitive G X.obj
h : Nonempty X.obj
Y : Action FintypeCat G
i : Y ⟶ Action.FintypeCat.ofMulAction G X
hm : Mono i
hni : ∀ (a : IsInitial Y), False
y : Y.V.obj
⊢ Function.Injective ⇑(ConcreteCategory.hom i.hom)

Tactic:
have : Mono i.hom := map_mono (forget₂ _ _) i
        exact ConcreteCategory.injective_of_mono_of_preservesPullback i.hom

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
x : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom (((autMulEquivAutGalois F).symm { unop' := x }).hom.app A)) a =
    (ConcreteCategory.hom (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a

Tactic:
← autMulEquivAutGalois_π,

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
x : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom
        (F.map
          ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ })
              (MulOpposite.unop ((autMulEquivAutGalois F) ((autMulEquivAutGalois F).symm { unop' := x })))).hom))
      a =
    (ConcreteCategory.hom (F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom)) a
Module: Mathlib.CategoryTheory.Groupoid.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Groupoid C
⊢ Quiver.IsThin C ↔ ∀ (c : C), Subsingleton (c ⟶ c)

Tactic:
refine ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => ?_⟩

Goal state after:
C : Type u_1
inst✝ : Groupoid C
h : ∀ (c : C), Subsingleton (c ⟶ c)
c d : C
f g : c ⟶ d
⊢ f = g
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝ : Quiver V
X✝² Y✝¹ X✝¹ Y✝ X Y : Paths (Symmetrify V)
X✝ Z✝ : Symmetrify V
f : X✝ ⟶ Z✝
XW : X✝² ⟶ (Paths.of (Symmetrify V)).obj X✝
WY : (Paths.of (Symmetrify V)).obj X✝ ⟶ Y✝¹
this :
  HomRel.CompClosure redStep (Path.reverse WY ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ Path.reverse XW)
    (Path.reverse WY ≫ (f.toPath ≫ (reverse f).toPath) ≫ Path.reverse XW)
⊢ HomRel.CompClosure redStep (Path.reverse (XW ≫ 𝟙 ((Paths.of (Symmetrify V)).obj X✝) ≫ WY))
    (Path.reverse (XW ≫ (f.toPath ≫ (reverse f).toPath) ≫ WY))

Tactic:
simpa only [CategoryStruct.comp, CategoryStruct.id, Quiver.Path.reverse, Quiver.Path.nil_comp,
    Quiver.Path.reverse_comp, Quiver.reverse_reverse, Quiver.Path.reverse_toPath,
    Quiver.Path.comp_assoc] using this

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
X Y : Paths (Symmetrify V)
⊢ EqvGen (HomRel.CompClosure redStep) (Path.nil ≫ Path.nil.reverse) (𝟙 X)

Tactic:
apply EqvGen.refl

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.y
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ X ⟶ X

Tactic:
exact q ≫ Quiver.Path.reverse q

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)

Tactic:
apply EqvGen.rel

Goal state after:
case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : generatedNormal X ≤ S
c d : C
h' : generated X ≤ generatedNormal X
⊢ X c d ⊆ S.arrows c d

Tactic:
rw [le_iff] at h h'

Goal state after:
case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
h : ∀ {c d : C}, (generatedNormal X).arrows c d ⊆ S.arrows c d
c d : C
h' : ∀ {c d : C}, (generated X).arrows c d ⊆ (generatedNormal X).arrows c d
⊢ X c d ⊆ S.arrows c d
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ 0 = s.ι.app j

Tactic:
dsimp at c

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cocone (span 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk 0 0 ⋯).ι.app j ≫ 0 = s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case refine_4
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 := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst
hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
k : J
⊢ (m ≫ ((Over.forget F ⋙ (evaluation C D).obj i).mapCone { pt := G, π := α }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k).hom.app i =
    { pt := s.1,
              π := { app := fun k ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }.π.app
        k ≫
      ({ diag := c, π := α, isLimit := hc }.diag.obj k).hom.app i

Tactic:
· simpa [← NatTrans.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
s : Cocone (multispanIndexCoend F).multispan
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : (F.obj (op j'✝)).obj j✝
⊢ (hom (Multicofork.π s ⟨j✝, (Hom.hom ((F.map f.op).app j✝)) x⟩.fst)) ⟨j✝, (Hom.hom ((F.map f.op).app j✝)) x⟩.snd =
    (hom (Multicofork.π s ⟨j'✝, (Hom.hom ((F.obj (op j'✝)).map f)) x⟩.fst))
      ⟨j'✝, (Hom.hom ((F.obj (op j'✝)).map f)) x⟩.snd

Tactic:
| mk f x =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct

Goal state before:
pp: C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
m : s.pt ⟶ (cone f).pt
h : ∀ (j : ℕᵒᵖ), m ≫ (cone f).π.app j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n = m ≫ (cone f).π.app (Opposite.op (n + 1)) ≫ Pi.π (fun i ↦ if i < n + 1 then M i else N i) n ≫ eqToHom ⋯

Tactic:
slice_rhs 2 3 => simp only [← dite_eq_ite, cone_π_app_comp_Pi_π_pos f (n + 1) n (by lia)]

Goal state after:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasCountableProducts C
s : Cone (Functor.ofOpSequence (functorMap f))
m : s.pt ⟶ (cone f).pt
h : ∀ (j : ℕᵒᵖ), m ≫ (cone f).π.app j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n = m ≫ (Pi.π M n ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Types.End

Goal state before:
pp: case mk
J : Type u
inst✝ : Category.{v, u} J
F : Jᵒᵖ ⥤ J ⥤ Type (max w u)
X : Type (max w u)
f✝ : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f✝ i = (F.obj (op j)).map g ≫ f✝ j
x✝ : chosenCoend F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
x : (F.obj (op j'✝)).obj j✝
⊢ (hom (f✝ ⟨j✝, (Hom.hom ((F.map f.op).app j✝)) x⟩.fst)) ⟨j✝, (Hom.hom ((F.map f.op).app j✝)) x⟩.snd =
    (hom (f✝ ⟨j'✝, (Hom.hom ((F.obj (op j'✝)).map f)) x⟩.fst)) ⟨j'✝, (Hom.hom ((F.obj (op j'✝)).map f)) x⟩.snd

Tactic:
| mk f x =>

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

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (g ≫ v) =
    (toOver I).map g ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm v
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✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this✝¹ : HasCoequalizerOfIsSplitPair G
this✝ : PreservesColimitOfIsSplitPair G
this : ReflectsColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G

Tactic:
exact monadicOfHasPreservesReflectsGSplitCoequalizers adj

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
apply pushout.hom_ext

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₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) =
    pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

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₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) =
    pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ≫
      Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom) =
    pushout.inr (((curriedTensor C).map (X ⊗ Y).hom).app Z.left) (((curriedTensor C).obj (X ⊗ Y).left).map Z.hom) ≫
      Arrow.Hom.left ((braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom)

Tactic:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext <;> 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
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:
simp [Hom.smul_def, Category.assoc, IsModHom.smul_hom]

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 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 ?_

Goal state after:
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)
⊢ (tensorRight (𝟙_ C)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      X P Q ◁ η ≫ actRight P Q =
    (tensorRight (𝟙_ C)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      (ρ_ (X P Q)).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) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_

Goal state after:
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)
⊢ (tensorRight (T.X ⊗ T.X)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      X P Q ◁ μ ≫ actRight P Q =
    (tensorRight (T.X ⊗ T.X)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      (α_ (X P Q) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
Module: Mathlib.CategoryTheory.Monoidal.Ring

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c
⊢ R ◁ σ ≫ μ = lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ σ

Tactic:
· replace h := h (fst R (R ⊗ R)) (snd _ _ ≫ fst _ _) (snd _ _ ≫ snd _ _)
    simp only [Hom.mul_def, Hom.add_def] at h
    convert! h using 2
    · cat_disch
    · ext
      · simp only [lift_fst]
        congr 1
        cat_disch
      · simp only [lift_snd]
        congr 1
        cat_disch

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
⊢ (a + b) * c = a * c + b * c

Tactic:
have := lift (lift a b) c ≫= h

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h : σ ▷ R ≫ μ = lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
x✝ : C
a b c : x✝ ⟶ R
this : lift (lift a b) c ≫ σ ▷ R ≫ μ = lift (lift a b) c ≫ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ σ
⊢ (a + b) * c = a * c + b * c
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₂
⊢ (M.tensorBimod N₁).actRight ≫
      colimMap
        (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) =
    colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
        Z.X ≫
      (M.tensorBimod N₂).actRight

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_

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₂
⊢ (tensorRight Z.X).map (coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫
      (M.tensorBimod N₁).actRight ≫
        colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) =
    (tensorRight Z.X).map (coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫
      colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
          Z.X ≫
        (M.tensorBimod N₂).actRight
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₂
⊢ (M.tensorBimod N₁).actRight ≫
      colimMap
        (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) =
    colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
        Z.X ≫
      (M.tensorBimod N₂).actRight

Tactic:
by
    refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
    dsimp
    slice_lhs 1 2 => rw [TensorBimod.π_tensor_id_actRight]
    slice_lhs 3 4 => rw [ι_colimMap, parallelPairHom_app_one]
    slice_lhs 2 3 => rw [← whiskerLeft_comp, Hom.right_act_hom]
    slice_rhs 1 2 =>
      rw [← comp_whiskerRight, ι_colimMap, parallelPairHom_app_one, comp_whiskerRight]
    slice_rhs 2 3 => rw [TensorBimod.π_tensor_id_actRight]
    simp

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
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₁.tensorBimod N).actRight ≫
      colimMap
        (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
          ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) =
    colimMap
          (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
            ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
        Z.X ≫
      (M₂.tensorBimod N).actRight

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_

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₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (tensorRight Z.X).map (coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft)) ≫
      (M₁.tensorBimod N).actRight ≫
        colimMap
          (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
            ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) =
    (tensorRight Z.X).map (coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft)) ≫
      colimMap
            (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
              ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
          Z.X ≫
        (M₂.tensorBimod N).actRight