mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
⊢ L.Final

Tactic:
rw [final_iff_isIso_colimit_pre]

Goal state after:
A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
⊢ ∀ (G : T ⥤ Type u₁), IsIso (colimit.pre G L)
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ Types.Limit.mk (homDiagram X✝ Y✝)
      (fun j ↦
        (hom (limit.π (homDiagram X✝ X✝) j))
            (Types.Limit.mk (homDiagram X✝ X✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) X✝)) ⋯) ≫
          (hom (limit.π (homDiagram X✝ Y✝) j)) x✝)
      ⋯ =
    x✝

Tactic:
apply Types.limit_ext.{v, v}

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ ∀ (j : J),
    (hom (limit.π (homDiagram X✝ Y✝) j))
        (Types.Limit.mk (homDiagram X✝ Y✝)
          (fun j ↦
            (hom (limit.π (homDiagram X✝ X✝) j))
                (Types.Limit.mk (homDiagram X✝ X✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) X✝)) ⋯) ≫
              (hom (limit.π (homDiagram X✝ Y✝) j)) x✝)
          ⋯) =
      (hom (limit.π (homDiagram X✝ Y✝) j)) x✝
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ Types.Limit.mk (homDiagram X✝ Y✝)
      (fun j ↦
        (hom (limit.π (homDiagram X✝ Y✝) j)) x✝ ≫
          (hom (limit.π (homDiagram Y✝ Y✝) j))
            (Types.Limit.mk (homDiagram Y✝ Y✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) Y✝)) ⋯))
      ⋯ =
    x✝

Tactic:
apply Types.limit_ext.{v, v}

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ ∀ (j : J),
    (hom (limit.π (homDiagram X✝ Y✝) j))
        (Types.Limit.mk (homDiagram X✝ Y✝)
          (fun j ↦
            (hom (limit.π (homDiagram X✝ Y✝) j)) x✝ ≫
              (hom (limit.π (homDiagram Y✝ Y✝) j))
                (Types.Limit.mk (homDiagram Y✝ Y✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) Y✝)) ⋯))
          ⋯) =
      (hom (limit.π (homDiagram X✝ Y✝) j)) x✝
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
W✝ X✝ Y✝ Z✝ : limit (F ⋙ objects)
x✝² : limit (homDiagram W✝ X✝)
x✝¹ : limit (homDiagram X✝ Y✝)
x✝ : limit (homDiagram Y✝ Z✝)
⊢ Types.Limit.mk (homDiagram W✝ Z✝)
      (fun j ↦
        (hom (limit.π (homDiagram W✝ Y✝) j))
            (Types.Limit.mk (homDiagram W✝ Y✝)
              (fun j ↦ (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹) ⋯) ≫
          (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝)
      ⋯ =
    Types.Limit.mk (homDiagram W✝ Z✝)
      (fun j ↦
        (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫
          (hom (limit.π (homDiagram X✝ Z✝) j))
            (Types.Limit.mk (homDiagram X✝ Z✝)
              (fun j ↦ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹ ≫ (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝) ⋯))
      ⋯

Tactic:
apply Types.limit_ext.{v, v}

Goal state after:
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
W✝ X✝ Y✝ Z✝ : limit (F ⋙ objects)
x✝² : limit (homDiagram W✝ X✝)
x✝¹ : limit (homDiagram X✝ Y✝)
x✝ : limit (homDiagram Y✝ Z✝)
⊢ ∀ (j : J),
    (hom (limit.π (homDiagram W✝ Z✝) j))
        (Types.Limit.mk (homDiagram W✝ Z✝)
          (fun j ↦
            (hom (limit.π (homDiagram W✝ Y✝) j))
                (Types.Limit.mk (homDiagram W✝ Y✝)
                  (fun j ↦ (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹) ⋯) ≫
              (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝)
          ⋯) =
      (hom (limit.π (homDiagram W✝ Z✝) j))
        (Types.Limit.mk (homDiagram W✝ Z✝)
          (fun j ↦
            (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫
              (hom (limit.π (homDiagram X✝ Z✝) j))
                (Types.Limit.mk (homDiagram X✝ Z✝)
                  (fun j ↦ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹ ≫ (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝) ⋯))
          ⋯)
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : ↑s.pt
⊢ (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X

Tactic:
apply Types.limit_ext.{v, v}

Goal state after:
case refine_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : ↑s.pt
⊢ ∀ (j : J),
    (hom (limit.π (F ⋙ objects) j)) ((limitConeLift F s).toFunctor.obj X) =
      (hom (limit.π (F ⋙ objects) j)) (m.toFunctor.obj X)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ τ ≫ φ = ψ ≫ φ'.inv

Tactic:
rw [Iso.eq_comp_inv]

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
τ : c ⟶ a
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ ≫ φ'.hom = ψ
⊢ (τ ≫ φ) ≫ φ'.hom = ψ
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ τ = IsCartesian.map p f φ ψ ≫ φ'.inv

Tactic:
rw [Iso.eq_comp_inv]

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝¹ : p.IsCartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : c ⟶ b
hψ : p.IsHomLift f ψ
τ : c ⟶ a'
hτ₁ : p.IsHomLift (𝟙 R) τ
hτ₂ : τ ≫ φ'.hom ≫ φ = ψ
⊢ τ ≫ φ'.hom = IsCartesian.map p f φ ψ
Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory

Goal state before:
pp: 𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (F.toFunctor ⋙ 𝒴.p).map φ ≫ eqToHom ⋯

Tactic:
congr_hom F.w

Goal state after:
𝒮 : Type u₁
inst✝¹ : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory 𝒮
𝒴 : BasedCategory 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst✝ : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow

Goal state before:
pp: A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
b : B
⊢ PreservesLimitsOfShape J colim

Tactic:
exact filtered_colim_preservesFiniteLimits

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

Goal state before:
pp: M G : Type v
inst✝¹ : Monoid M
inst✝ : Group G
J : SingleObj M ⥤ Type u
g h : M
x : J.obj (SingleObj.star M)
⊢ (g * h) • x = g • h • x

Tactic:
change J.map (g * h) x = (J.map h ≫ J.map g) x
    rw [← SingleObj.comp_as_mul]
    · simp
      rfl

Goal state after:
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
⊢ (ConcreteCategory.hom (Y.ρ g).hom) ↑y ∈ (Set.range ⇑(ConcreteCategory.hom f.hom))ᶜ

Tactic:
intro ⟨x, h⟩

Goal state after:
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
⊢ False
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case neg
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : ¬IsConnected X
nhi : ¬∀ (a : IsInitial X), False
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
simp only [not_forall, not_false_eq_true] at nhi
    obtain ⟨hi⟩ := nhi
    exact has_decomp_connected_components_aux_initial X hi

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map u)) b) =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map (selfProdPermIncl h b))) a)

Tactic:
convert_to F.map (selfProdProj u t) b = _

Goal state after:
case e'_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map u)) b) =
    (ConcreteCategory.hom (F.map (selfProdProj u t))) b

case convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x ↦ X) t))) ((ConcreteCategory.hom (F.map (selfProdPermIncl h b))) a)
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
t : (AutGalois F)ᵐᵒᵖ
⊢ ((↑(endMulEquivAutGalois F)).comp (Aut.toEnd F)) ((fun t ↦ asIso ((endMulEquivAutGalois F).symm t)) t) = t

Tactic:
simp only [MonoidHom.coe_comp, MonoidHom.coe_coe]
    exact (MulEquiv.eq_symm_apply (endMulEquivAutGalois F)).mp rfl

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ⋯
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
⊢ t ∈ U

Tactic:
apply hmem

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ⋯
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
⊢ ∀ (X : ↑I), t.hom.app ↑X = 𝟙 (F.obj ↑X)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ∀ (j : Discrete WalkingPair),
    ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
              (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (pairComp F G ((evaluation D C).obj d)).symm.hom).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCone).pt).hom ≫
        (((evaluation D C).obj d).mapCone (pointwiseBinaryBicone F G).toCone).π.app j

Tactic:
rintro (_ | _ | _) <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : D ⥤ C
d : D
⊢ ∀ (j : Discrete WalkingPair),
    ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (pairComp F G ((evaluation D C).obj d)).symm.inv).obj
                (BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt).hom =
      (((evaluation D C).obj d).mapCocone (pointwiseBinaryBicone F G).toCocone).ι.app j

Tactic:
rintro (_ | _ | _) <;> cat_disch

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
c : C
d✝ y✝ : D
f : d✝ ⟶ y✝
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d))
      (edge c d✝ ≫ (inclRight C D).map f) =
    homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (edge c d✝) ≫
      homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) ((inclRight C D).map f)

Tactic:
simpa using! α.naturality <| (Prod.sectR c _).map f

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⋆ D ⥤ E
eₗ : inclLeft C D ⋙ F ≅ inclLeft C D ⋙ G
eᵣ : inclRight C D ⋙ F ≅ inclRight C D ⋙ G
h :
  whiskerRight (edgeTransform C D) F ≫ ((Prod.snd C D).isoWhiskerLeft eᵣ).hom =
    ((Prod.fst C D).isoWhiskerLeft eₗ).hom ≫ whiskerRight (edgeTransform C D) G
⊢ whiskerRight (edgeTransform C D) F ≫ (Prod.snd C D).whiskerLeft eᵣ.hom =
    (Prod.fst C D).whiskerLeft eₗ.hom ≫ whiskerRight (edgeTransform C D) G

Tactic:
simpa using h

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalLeftAction C D
w x : C
y z : D
f : w ⟶ x
g : y ⟶ z
⊢ w ⊴ₗ g ≫ f ⊵ₗ z = f ⊵ₗ y ≫ x ⊴ₗ g

Tactic:
by
  simp only [← id_actionHom, ← actionHom_id, ← actionHom_comp, id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

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 C
inst✝ : MonoidalRightAction C D
w x : D
y z : C
f : w ⟶ x
g : y ⟶ z
⊢ w ⊴ᵣ g ≫ f ⊵ᵣ z = f ⊵ᵣ y ≫ x ⊴ᵣ g

Tactic:
by
  simp only [← id_actionHom, ← actionHom_id, ← actionHom_comp, id_comp, comp_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
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
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft

Tactic:
by
        rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]

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
⊢ IsIso (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m, m • x = y

Tactic:
have H (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) :
      lift m x ≫ leftSMul M X = lift (m • x) x := by
    ext <;> simp [Hom.smul_def]

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
⊢ IsIso (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m, m • x = y
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).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) ⋯ ⋯) =
    X.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) ⋯ ⋯) ≫
      (M₂.tensorBimod N).actLeft

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

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫
              (α_ A A A).inv ▷ A ≫ μ ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ (β_ A A).hom ≫ A ◁ (𝒮 ⊗ₘ 𝒮) ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
by
  slice_lhs 7 8 =>
    rw [associator_naturality_left]
  slice_lhs 8 9 =>
    rw [← whisker_exchange]
  slice_lhs 9 10 =>
    rw [← whisker_exchange]
  slice_lhs 11 12 =>
    rw [MonObj.mul_assoc_flip]
  slice_lhs 10 11 =>
    rw [associator_inv_naturality_left]
  slice_lhs 11 12 =>
    simp only [← comp_whiskerRight]
    rw [MonObj.mul_assoc]
    simp only [comp_whiskerRight]
  rw [tensorHom_def]
  rw [tensor_whiskerLeft _ _ (β_ A A).hom]
  rw [pentagon_inv_inv_hom_hom_inv_assoc]
  slice_lhs 7 8 =>
    rw [Iso.inv_hom_id]
  rw [Category.id_comp]
  slice_lhs 5 7 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.hexagon_forward]
    simp only [whiskerLeft_comp]
  simp only [tensor_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc, pentagon_inv_inv_hom_inv_inv,
    whisker_assoc, MonObj.mul_assoc, whiskerLeft_inv_hom_assoc]
  slice_lhs 3 4 =>
    simp only [← whiskerLeft_comp]
    rw [BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]
  rw [tensorHom_def']
  simp only [whiskerLeft_comp]
  slice_lhs 5 6 =>
    simp only [← whiskerLeft_comp]
    rw [← associator_naturality_right]
    simp only [whiskerLeft_comp]
  slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [← whisker_exchange]
    simp only [whiskerLeft_comp]
  slice_lhs 5 9 =>
    simp only [← whiskerLeft_comp]
    rw [associator_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]
  slice_lhs 6 7 =>
    simp only [← whiskerLeft_comp]
    rw [MonObj.one_mul]
  slice_lhs 3 4 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_left]
    simp only [whiskerLeft_comp]
  slice_lhs 4 5 =>
    simp only [← whiskerLeft_comp]
    rw [← BraidedCategory.braiding_naturality_right]
    simp only [whiskerLeft_comp]
  rw [← associator_naturality_middle_assoc]
  simp only [braiding_tensorUnit_right, whiskerLeft_comp]
  slice_lhs 6 7 =>
    simp only [← whiskerLeft_comp]
    rw [Iso.inv_hom_id]
  simp only [whiskerLeft_id, Category.id_comp]
  slice_lhs 5 6 =>
    rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]
  rw [associator_inv_naturality_right_assoc, Iso.hom_inv_id_assoc]
  slice_lhs 3 4 =>
    rw [whisker_exchange]
  slice_lhs 1 3 =>
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
  slice_lhs 2 3 =>
    rw [← whisker_exchange]
  slice_lhs 1 2 =>
    rw [← tensorHom_def]
  slice_lhs 2 3 =>
    rw [rightUnitor_naturality]
  monoidal

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

Goal state before:
pp: case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) (x ⊗ₜ[R] z + y ⊗ₜ[R] z)

Tactic:
rw [← TensorProduct.add_tmul]

Goal state after:
case e'_2
R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x y z : ↑A
⊢ (x + y) * z = (Hom.hom μ) ((x + y) ⊗ₜ[R] z)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)) ∘ₗ Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)

Tactic:
LinearMap.comp_apply

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)