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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
h : F.map f = F.map g
⊢ f = g

Tactic:
by
    have : IsIso (equalizer.ι (F.map f) (F.map g)) := equalizer.ι_of_eq h
    have : IsIso (F.map (equalizer.ι f g)) := by
      rw [← equalizerComparison_comp_π f g F]
      exact IsIso.comp_isIso
    have : IsIso (equalizer.ι f g) := isIso_of_reflects_iso _ F
    exact eq_of_epi_equalizer

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

Goal state before:
pp: G : Type v
inst✝¹ : Group G
inst✝ : Finite G
G' : Type ?u.14
hg : Group G'
hf : Fintype G'
e : Nonempty (G ≃* G')
⊢ PreservesColimitsOfShape (SingleObj G) FintypeCat.incl

Tactic:
exact Limits.preservesColimitsOfShape_of_equiv (Classical.choice e).toSingleObjEquiv.symm _

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
⊢ ∃ a, (functorToAction F).map a = f

Tactic:
by
    let u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
      prod.lift (𝟙 _) f
    let i : (functorToAction F).obj X ⟶ (functorToAction F).obj (X ⨯ Y) :=
      u ≫ (PreservesLimitPair.iso (functorToAction F) X Y).inv
    have : Mono i := by
      have : Mono (u ≫ prod.fst) := prod.lift_fst (𝟙 _) f ▸ inferInstance
      have : Mono u := mono_of_mono u prod.fst
      apply mono_comp u _
    obtain ⟨Z, g, v, _, hvgi⟩ := exists_lift_of_mono F (Limits.prod X Y)
      ((functorToAction F).obj X) i
    let ψ : Z ⟶ X := g ≫ prod.fst
    have hgvi : (functorToAction F).map g = v.inv ≫ i := by simp [← hvgi]
    have : IsIso ((functorToAction F).map ψ) := by
      simp only [map_comp, hgvi, Category.assoc, ψ]
      have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance
      apply IsIso.comp_isIso
    have : IsIso ψ := isIso_of_reflects_iso ψ (functorToAction F)
    use inv ψ ≫ g ≫ prod.snd
    rw [← cancel_epi ((functorToAction F).map ψ)]
    ext (z : F.obj Z)
    simp [-FintypeCat.comp_apply, -Action.comp_hom, i, u, ψ, hgvi]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
⊢ Function.Injective ⇑(toAut F G)

Tactic:
← MonoidHom.ker_eq_bot_iff,

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).obj
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1
⊢ (toAut F G).ker = ⊥
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c d e : C
f : c ⟶ d
g : d ⟶ e
hg : g ∈ S.arrows d e
⊢ f ≫ g ∈ S.arrows c e → f ∈ S.arrows c d

Tactic:
rintro h
    suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
      simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
    apply S.mul h (S.inv hg)

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasPullbacks C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty X.hom (Opposite.op Y ⋔ Z).hom

Tactic:
rw [← hasLiftingProperty_iff]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasPullbacks C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y Z : Arrow C
⊢ HasLiftingProperty (X □ Y).hom Z.hom ↔ HasLiftingProperty (Y □ X).hom Z.hom
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Function.Bijective (Types.sectionOfCone (P.mapCone c)) ↔ Function.Bijective fun g ↦ coconePtToShrinkYoneda c hc' ≫ g

Tactic:
← Function.Bijective.of_comp_iff' (coconeCompShrinkYonedaHomEquiv hc').symm.bijective,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
⊢ Function.Bijective (⇑(coconeCompShrinkYonedaHomEquiv hc').symm ∘ Types.sectionOfCone (P.mapCone c)) ↔
    Function.Bijective fun g ↦ coconePtToShrinkYoneda c hc' ≫ g
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option.refine_2.none
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
⊢ (W none).IsInvertedBy (L none)

Tactic:
apply Localization.inverts

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_option.refine_2.some
J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
this : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L) (Pi.optionEquivalence D).symm.functor
i : J
⊢ (W (some i)).IsInvertedBy (L (some i))

Tactic:
apply Localization.inverts

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ (((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)) ▷
        F.obj (L.obj X₃) ≫
      ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁ ⊗ L.obj X₂)).app (L.obj X₃) ≫
        F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      F.obj (L.obj X₁) ◁
          (((Lifting.iso L W G F).hom.app X₂ ⊗ₘ (Lifting.iso L W G F).hom.app X₃) ≫
            μ G X₂ X₃ ≫ (Lifting.iso L W G F).inv.app (X₂ ⊗ X₃) ≫ F.map (δ L X₂ X₃)) ≫
        ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂ ⊗ L.obj X₃)

Tactic:
curriedTensorPreIsoPost_hom_app_app' L W F G (μIso L _ _) (Iso.refl _),

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ (((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)) ▷
        F.obj (L.obj X₃) ≫
      ((F.map (μIso L X₁ X₂).hom ≫ (Lifting.iso L W G F).hom.app (X₁ ⊗ X₂) ⊗ₘ
            F.map (Iso.refl (L.obj X₃)).hom ≫ (Lifting.iso L W G F).hom.app X₃) ≫
          μ G (X₁ ⊗ X₂) X₃ ≫
            (Lifting.iso L W G F).inv.app ((X₁ ⊗ X₂) ⊗ X₃) ≫
              F.map (δ L (X₁ ⊗ X₂) X₃ ≫ ((μIso L X₁ X₂).inv ⊗ₘ (Iso.refl (L.obj X₃)).inv))) ≫
        F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      F.obj (L.obj X₁) ◁
          (((Lifting.iso L W G F).hom.app X₂ ⊗ₘ (Lifting.iso L W G F).hom.app X₃) ≫
            μ G X₂ X₃ ≫ (Lifting.iso L W G F).inv.app (X₂ ⊗ X₃) ≫ F.map (δ L X₂ X₃)) ≫
        ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂ ⊗ L.obj X₃)
Module: Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Goal state before:
pp: D : Type u_1
D' : Type u_2
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : Category.{v_2, u_2} D'
F : D ⥤ D'
C : Type u_3
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalRightAction C D
inst✝¹ : MonoidalRightAction C D'
inst✝ : F.OplaxRightLinear C
d : D
⊢ δᵣ F d (𝟙_ C) ≫ (ρᵣ (F.obj d)).hom = F.map (ρᵣ d).hom

Tactic:
by
  simpa [-δᵣ_unitality_inv] using
    F.map (ρᵣ[C] d).hom ≫=
      (δᵣ_unitality_inv F d).symm =≫
      (ρᵣ[C] (F.obj d)).hom

Goal state after:
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
L : D ⥤ C
h : L ⊣ F
A : C
inst✝² : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L
inst✝¹ : F.Full
inst✝ : F.Faithful
B : D
⊢ IsIso ((frobeniusMorphism F h A).natTrans.app B)

Tactic:
dsimp [frobeniusMorphism]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_snd
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
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B ≫ snd ((reflector i).obj A) ((reflector i).obj B))

Tactic:
prodComparison_snd

Goal state after:
case h_snd
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
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (snd A B))
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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
⊢ ∀ (j : (multicospanShapeEnd C).L),
    (G.map f ≫
          Wedge.IsLimit.lift (ℌ.isLimitWedge c')
            (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯) ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
      (Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
          H.map f) ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j

Tactic:
intro (j : 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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ (G.map f ≫
        Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯) ≫
      Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
    (Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
        H.map f) ≫
      Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((X.tensor Y).tensor Z).normalizeObj' ⟶ (X.tensor (Y.tensor Z)).normalizeObj'

Tactic:
dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (X✝.tensor (Y✝.tensor Z✝)).normalizeObj' ⟶ ((X✝.tensor Y✝).tensor Z✝).normalizeObj'

Tactic:
dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (unit.tensor a✝).normalizeObj' ⟶ a✝.normalizeObj'

Tactic:
dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ a✝.normalizeObj' ⟶ (unit.tensor a✝).normalizeObj'

Tactic:
dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (a✝.tensor unit).normalizeObj' ⟶ a✝.normalizeObj'

Tactic:
dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ a✝.normalizeObj' ⟶ (a✝.tensor unit).normalizeObj'

Tactic:
dsimp; exact Discrete.natTrans (fun _ => 𝟙 _)

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
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 Q.X L.X).hom ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)

Tactic:
slice_lhs 1 3 => rw [Iso.hom_inv_id_assoc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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 ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (limit F)).hom ≫ limit.π F j =
    { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }.π.app j ▷ limit F ≫
      (λ_ (limit F)).hom ≫ limit.π F j

Tactic:
rw [id_whiskerRight, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
⊢ Function.Surjective fun i ↦ ⟨Arrow.mk (f i), ⋯⟩

Tactic:
by
    rintro ⟨f, hf⟩
    rw [MorphismProperty.mem_toSet_iff, MorphismProperty.ofHoms_iff] at hf
    obtain ⟨i, hf⟩ := hf
    obtain rfl : f = _ := hf
    exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
i : I j
i' : I j'
hom : Total.mk Q j i ⟶ Total.mk Q j' i'
⊢ (Q j).ι.app i ≫
      P.diag.map hom.base ≫
        (Q j').isColimit.desc { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } } =
    c.ι.app ⟨j, i⟩

Tactic:
rw [reassoc_of% hom.w, (Q j').isColimit.fac]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁵ : Category.{v_1, u_1} J✝
inst✝⁴ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝¹ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝³ : SmallCategory J
inst✝² : (j : J) → SmallCategory (I j)
D : J ⥤ C
P✝ : (j : J) → ColimitPresentation (I j) (D.obj j)
X : C
P : ColimitPresentation J X
Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)
c : Cocone { obj := fun k ↦ (Q k.fst).diag.obj k.snd, map := fun {k l} f ↦ f.hom, map_id := ⋯, map_comp := ⋯ }
j j' : J
i : I j
i' : I j'
hom : Total.mk Q j i ⟶ Total.mk Q j' i'
⊢ hom.hom ≫ { pt := c.pt, ι := { app := fun i ↦ c.ι.app ⟨j', i⟩, naturality := ⋯ } }.ι.app i' = c.ι.app ⟨j, i⟩
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
⊢ ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)

Tactic:
obtain ⟨Q₁, _, h₁, h₁'⟩ := EssentiallySmall.exists_small_le.{w} P₁

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

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

Tactic:
by
    rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR
    obtain ⟨𝒰, rfl⟩ := hR
    rw [H 𝒰]
    intro i
    exact h ⟨i⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
f : X ⟶ Y
⊢ rightAdd X Y f 0 = f

Tactic:
by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]

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

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ (∑ j_1,
      (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    0

Tactic:
apply Finset.sum_eq_zero

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ∀ x ∈ Finset.univ,
    ((if h : i = b then if h' : h ▸ j = x then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = b then if h' : h ▸ j' = x then eqToHom ⋯ else 0 else 0) =
      0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₁
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
hi : i ∉ Finset.univ
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    0

Tactic:
simp at hi

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app x✝)), inj' := ⋯, map_rel_iff' := ⋯ } =
    ofHom { toFun := ⇑(ConcreteCategory.hom (c.ι.app x✝¹)), inj' := ⋯, map_rel_iff' := ⋯ } ≫
      ((Functor.const J).obj { carrier := CoconePt hc, str := instPartialOrderCoconePt hc }).map f

Tactic:
ext x; exact ConcreteCategory.congr_hom (c.w f) x

Goal state after: