mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
          g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0

Tactic:
Preadditive.comp_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
            g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
        f.f 1 -
      { X₁ := I.cocomplex.X 0, X₂ := I.cocomplex.X (0 + 1), X₃ := I.cocomplex.X (0 + 2), f := I.cocomplex.d 0 (0 + 1),
            g := I.cocomplex.d (0 + 1) (0 + 2), zero := ⋯ }.f ≫
        descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
    0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) = 0

Tactic:
Preadditive.comp_sub,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
I : InjectiveResolution Y
J : InjectiveResolution Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ pullback.fst q p' ≫ q ≫ g.hom = (pullback.snd q p' ≫ q') ≫ h.hom

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst q p' ≫ q) ≫ g.hom = (pullback.snd q p' ≫ q') ≫ h.hom
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ {
      X₁ :=
        ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj
            ((CochainComplex.single₀ C).obj Z)).X₂,
      X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₂,
      X₃ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).X₃,
      f :=
        ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).map
            (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩)).τ₂,
      g := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1).obj (ofCocomplex Z)).g, zero := ⋯ } ≅
    { X₁ := Z, X₂ := under Z, X₃ := syzygies (Injective.ι Z), f := Injective.ι Z, g := d (Injective.ι Z), zero := ⋯ }

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
          (by simp [ofCocomplex])

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk ((x.hom ≫ f) ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f ≫ kernel.ι (cokernel.π S.f) =
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f)

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (pullback.fst (Abelian.factorThruImage S.f) c ≫ Abelian.factorThruImage S.f) ≫ kernel.ι (cokernel.π S.f) =
    (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f)
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ inv (DerivedCategory.Q.map R.ι') ≫
      (singleFunctor C 0 ⋙ DerivedCategory.Q).map g ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y' =
    DerivedCategory.Q.map φ.hom' ≫
      inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'

Tactic:
← Category.assoc,

Goal state after:
case e_g
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
this✝ : HasDerivedCategory C
this : (f ≫ φ.hom.f n) ≫ (R'.cochainComplexXIso (↑n) n ⋯).inv = (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ≫ φ.hom'.f ↑n
⊢ (inv (DerivedCategory.Q.map R.ι') ≫ (singleFunctor C 0 ⋙ DerivedCategory.Q).map g) ≫
      (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y' =
    DerivedCategory.Q.map φ.hom' ≫
      inv (DerivedCategory.Q.map R'.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y'
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ P ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯)).pt

Tactic:
exact P.prop_kernel f.hom X.property Y.property

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

Goal state before:
pp: case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)

Tactic:
have : X.ρ (f a) = ((res V f).obj X).ρ a := rfl

Goal state after:
case w
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ F.obj X ◁ inv (F.map f)ᘁ ≫ F.map f ▷ (F.obj Y)ᘁ

Tactic:
← Category.assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = (η_ (F.obj X) (F.obj X)ᘁ ≫ F.obj X ◁ inv (F.map f)ᘁ) ≫ F.map f ▷ (F.obj Y)ᘁ
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝ : Abelian D := abelian L P
this : PreservesFiniteLimits L
x✝ : PreservesFiniteLimits (L ⋙ G)
⊢ PreservesFiniteLimits G

Tactic:
have := (Localization.functor_additive_iff L P.isoModSerre G).mpr
    (L ⋙ G).additive_of_preserves_binary_products

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝¹ : Abelian D := abelian L P
this✝ : PreservesFiniteLimits L
x✝ : PreservesFiniteLimits (L ⋙ G)
this : G.Additive
⊢ PreservesFiniteLimits G
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }

Tactic:
have h₁ : (T : C ⥤ C).map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f :=
      congr_arg Monad.Algebra.Hom.f s.condition
    have h₂ : (T : C ⥤ C).map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f := s.π.h
    refine ⟨⟨T.η.app _ ≫ s.π.f, ?_⟩, ?_, ?_⟩
    · dsimp
      rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]
    · ext
      simpa [← T.η.naturality_assoc, T.left_unit_assoc] using! T.η.app ((T : C ⥤ C).obj X.A) ≫= h₁
    · intro m hm
      ext
      dsimp only
      rw [← hm]
      apply (X.unit_assoc _).symm

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

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
g : G
f : Fin n → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f

Tactic:
by
  induction n generalizing g with
  | zero =>
    funext (x : Fin 1)
    simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]
  | succ n hn =>
    funext x
    induction x using Fin.cases with
    | zero => simp; rfl
    | succ i =>
      simpa [diagonalSuccIsoTensorTrivial, types_tensorObj_def, mul_assoc, Fin.partialProd_succ',
        ofMulAction_V] using! congrFun (hn (g * f 0) (Fin.tail f)) i

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ inv (H.map (t.adj₁.unit.app (G.obj X)))

Tactic:
← H.map_inv

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
⊢ t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (G.map (t.adj₁.counit.app X) ≫ 𝟙 (G.obj X)) =
    t.adj₂.unit.app (F.obj (G.obj X)) ≫ H.map (inv (t.adj₁.unit.app (G.obj X)))
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a : B
t : a ⟶ a
inst✝ : Comonad t
⊢ Δ = Δ

Tactic:
change 𝟙 t ≫ Δ = Δ

Goal state after:
B : Type u
inst✝¹ : Bicategory B
a : B
t : a ⟶ a
inst✝ : Comonad t
⊢ 𝟙 t ≫ Δ = Δ
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ F.isoMapOfCommSq ⋯ = F.mapId X₁ ▷ᵢ F.map f ≪≫ λ_ (F.map f) ≪≫ (ρ_ (F.map f)).symm ≪≫ (F.map f ◁ᵢ F.mapId X₂).symm

Tactic:
ext
  rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ : B
f : X₁ ⟶ X₂
⊢ F.isoMapOfCommSq ⋯ = F.map f ◁ᵢ F.mapId X₂ ≪≫ ρ_ (F.map f) ≪≫ (λ_ (F.map f)).symm ≪≫ (F.mapId X₁ ▷ᵢ F.map f).symm

Tactic:
ext
  rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }

Tactic:
have hf : ∀ a : J, a ∈ l → Zigzag a j₂ := by
    intro i hi
    apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
    · intro j k
      apply Relation.ReflTransGen.head
    · apply Relation.ReflTransGen.refl

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₁ j₂ : J
hj₁ : ConnectedComponents.objectProperty (Quotient.mk'' j₂) j₁
h₁₂ : Zigzag j₁ j₂
l : List J
hl₁ : List.IsChain Zag (j₁ :: l)
hl₂ : (j₁ :: l).getLast ⋯ = j₂
f : (x : J) → Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h ↦ { obj := x, property := ⋯ }
hf : ∀ a ∈ l, Zigzag a j₂
⊢ ∃ l,
    List.IsChain Zag ({ obj := j₁, property := hj₁ } :: l) ∧
      ({ obj := j₁, property := hj₁ } :: l).getLast ⋯ = { obj := j₂, property := ⋯ }
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ j' = k'

Tactic:
← hX,

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j' : ConnectedComponents J
X : J
hX : j'.objectProperty X
k' : ConnectedComponents J
Y : J
hY : k'.objectProperty Y
f : X ⟶ Y
⊢ Quotient.mk'' X = k'
Module: Mathlib.Data.PFun

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h✝ : b ∈ f.fix a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
a'' : α
e : Sum.inr a'' ∈ f a'
⊢ C a'

Tactic:
exact hind _ _ (fix_fwd h e) e (ih _ e)

Goal state after:
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✝ Y✝ : J
f : X✝ ⟶ Y✝
g : (hom (limit.π (F ⋙ objects) X✝)) X ⟶ (hom (limit.π (F ⋙ objects) X✝)) Y
⊢ (hom (limit.π (F ⋙ objects) Y✝)) X ⟶ (hom (limit.π (F ⋙ objects) Y✝)) Y

Tactic:
refine eqToHom ?_ ≫ (F.map f).toFunctor.map g ≫ eqToHom ?_
    · exact (congr_hom (limit.w (F ⋙ Cat.objects) f) X).symm
    · exact congr_hom (limit.w (F ⋙ Cat.objects) f) Y

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ pullback.fst g₁ (Sigma.ι X a) ≫ g₁ ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e

Tactic:
← Category.assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a : α
⊢ (pullback.fst g₁ (Sigma.ι X a) ≫ g₁) ≫ Sigma.desc e = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
a b : α
hg : pullback.fst g₁ (Sigma.ι X a) ≫ g₁ ≫ Sigma.desc π = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b

Tactic:
← Category.assoc,

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
a b : α
hg : (pullback.fst g₁ (Sigma.ι X a) ≫ g₁) ≫ Sigma.desc π = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A✝ A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A✝ A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
⊢ F.map (strInv h ≫ A.str) ≫ A.str = (A.str ≫ strInv h) ≫ A.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ h.hom ≫ V₁.str ≫ F.map h.inv = V₀.str

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ (h.hom ≫ V₁.str) ≫ F.map h.inv = V₀.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ f.f ≫ V₁.str ≫ F.map (inv f.f) = V₀.str

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ C
V₀ V₁ : Coalgebra F
f : V₀ ⟶ V₁
inst✝ : IsIso f.f
⊢ (f.f ≫ V₁.str) ≫ F.map (inv f.f) = V₀.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ⟶ G
X✝ Y✝ : Coalgebra F
f : X✝ ⟶ Y✝
⊢ X✝.str ≫ F.map f.f ≫ α.app { V := Y✝.V, str := Y✝.str ≫ α.app Y✝.V }.V =
    f.f ≫ { V := Y✝.V, str := Y✝.str ≫ α.app Y✝.V }.str

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F✝
f✝ : V₀ ⟶ V₁
g : V₁ ⟶ V₂
F G : C ⥤ C
α : F ⟶ G
X✝ Y✝ : Coalgebra F
f : X✝ ⟶ Y✝
⊢ (X✝.str ≫ F.map f.f) ≫ α.app { V := Y✝.V, str := Y✝.str ≫ α.app Y✝.V }.V =
    f.f ≫ { V := Y✝.V, str := Y✝.str ≫ α.app Y✝.V }.str
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ strInv h ≫ A.str = 𝟙 (F.obj A.V)

Tactic:
rw [strInv, ← (h.from ⟨F.obj A.V, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
  congr
  exact right_inv h

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁸ : Category.{v₁, u₁} V
inst✝⁷ : MonoidalCategory V
C : Type u₂
inst✝⁶ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁵ : Category.{v₃, u₃} J
K : Type u₄
inst✝⁴ : Category.{v₄, u₄} K
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
i j : J
f : i ⟶ j
this :
  end_.π (diagram V F₁ F₂) i ≫
      (ρ_ (F₁.obj i ⟶[V] F₂.obj i)).inv ≫
        (F₁.obj i ⟶[V] F₂.obj i) ◁ (eHomEquiv V) (F₂.map f) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j ≫
      (λ_ (F₁.obj j ⟶[V] F₂.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₂.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)
⊢ enrichedHom V F₁ F₂ ◁ end_.π (diagram V F₂ F₃) j ≫
      (end_.π (diagram V F₁ F₂) j ▷ F₂.obj j ⟶[V] F₃.obj j) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ≫
          (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
            ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j) =
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      (λ_ (F₁.obj j ⟶[V] F₃.obj j)).inv ≫
        ((eHomEquiv V) (F₁.map f) ▷ F₁.obj j ⟶[V] F₃.obj j) ≫ eComp V (F₁.obj i) (F₁.obj j) (F₃.obj j)

Tactic:
conv_rhs => rw [assoc, tensorHom_def'_assoc]

Goal state after: