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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (functor C).Faithful

Tactic:
by
  rw [functor]
  have : (F C).Faithful := by rw [F]; infer_instance
  have : (G C).Faithful := by rw [G]; infer_instance
  have : (H C).Faithful := IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding _
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: 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
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      ((ShiftedHom.map
            ((singleFunctor C 0).map g ≫
              Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
← ShiftedHom.mk₀_comp 0 rfl,

Goal state after:
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
X' : C
g : X' ⟶ X
this : HasDerivedCategory C
⊢ (ShiftedHom.mk₀ 0 Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯
            (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
          ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X')).comp
      ((((ShiftedHom.mk₀ 0 ⋯ ((singleFunctor C 0).map g)).comp
                (Cocycle.equivHomShift.symm (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯))
                ⋯).map
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯
            ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
      ((ShiftedHom.map
            (φ.hom' ≫
              Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯

Tactic:
← ShiftedHom.mk₀_comp 0 rfl,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ (ShiftedHom.mk₀ (↑0) Ext.mk₀._proof_1 ((DerivedCategory.singleFunctor C 0).map g)).comp
      ((ShiftedHom.mk₀ 0 ⋯
            ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X ≫ inv (DerivedCategory.Q.map R.π'))).comp
        ((ShiftedHom.map
              (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
              DerivedCategory.Q).comp
          (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
        ⋯)
      ⋯ =
    (ShiftedHom.mk₀ 0 ⋯
          ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X' ≫ inv (DerivedCategory.Q.map R'.π'))).comp
      ((((ShiftedHom.mk₀ 0 ⋯ φ.hom').comp
                (Cocycle.equivHomShift.symm (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯))
                ⋯).map
            DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y)) ⋯)
      ⋯
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ X' s, ∃ (_ : P.isoModSerre s), s ≫ f = 0) → P (Abelian.image f)

Tactic:
rintro ⟨Y', s, hs, eq⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y' ⟶ X
hs : P.isoModSerre s
eq : s ≫ f = 0
⊢ P (Abelian.image f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ X' s, ∃ (_ : P.isoModSerre s), s ≫ f = 0

Tactic:
refine ⟨_, kernel.ι f, ?_, by simp⟩
    simpa only [isoModSerre_iff_of_mono] using!
      P.prop_of_iso (Abelian.coimageIsoImage f).symm hf

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0) → P (Abelian.image f)

Tactic:
rintro ⟨Y', s, hs, eq⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.monoModSerre s
eq : f ≫ s = 0
⊢ P (Abelian.image f)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
⊢ (∃ Y' s, ∃ (_ : P.isoModSerre s), f ≫ s = 0) → P (Abelian.image f)

Tactic:
rintro ⟨Y', s, hs, eq⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
Y' : C
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f ≫ s = 0
⊢ P (Abelian.image f)
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Mono f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Mono (L.map f) → ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
e : L.mapArrow.obj (L.mapArrow.objPreimage (Arrow.mk f)) ≅ Arrow.mk f := L.mapArrow.objObjPreimageIso (Arrow.mk f)
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e' : Arrow.mk (L.map f') ≅ Arrow.mk (L.map (L.mapArrow.objPreimage (Arrow.mk f)).hom)
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
x✝¹ y✝ : R
b✝ : F ⟶ G
x✝ : C
⊢ ((x✝¹ * y✝) • b✝).app x✝ = (x✝¹ • y✝ • b✝).app x✝

Tactic:
apply mul_smul

Goal state after:
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
Z : C
z : Z ⟶ X
Z' : C
t : Z' ⟶ Z
ht : P.isoModSerre t
fac : (t ≫ z) ≫ f = 0
this : IsIso (L.map t)
⊢ ∃ l, l ≫ L.map (kernel.ι f) = eqToHom ⋯ ≫ L.map z

Tactic:
exact ⟨inv (L.map t) ≫ L.map (kernel.lift _ _ fac), by simp [← Functor.map_comp]⟩

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ⟨ConcreteCategory.hom { hom := ConcreteCategory.ofHom ↑x✝, comm := ⋯ }.hom, ⋯⟩ = x✝

Tactic:
dsimp; ext; simp [ConcreteCategory.hom_ofHom]

Goal state after:
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
⊢ (𝟙_ (C ⥤ D)).map f ≫
      η_ (F.obj Y)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj Y) =
    η_ (F.obj X)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj X) ≫
      (F ⊗ { obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }).map f

Tactic:
dsimp
            rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id,
              id_tensorHom, tensorHom_id, ← Category.assoc,
              coevaluation_comp_rightAdjointMate, Category.assoc, ← comp_whiskerRight,
              IsIso.inv_hom_id, id_whiskerRight, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.End

Goal state before:
pp: C : Type u
inst✝ : Bicategory C
X : C
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : X ⟶ X
f₁✝ : X₁✝ ⟶ Y₁✝
f₂✝ : X₂✝ ⟶ Y₂✝
g₁✝ : Y₁✝ ⟶ Z₁✝
g₂✝ : Y₂✝ ⟶ Z₂✝
⊢ (f₁✝ ▷ X₂✝ ≫ Y₁✝ ◁ f₂✝) ≫ g₁✝ ▷ Y₂✝ ≫ Z₁✝ ◁ g₂✝ = (f₁✝ ≫ g₁✝) ▷ X₂✝ ≫ Z₁✝ ◁ (f₂✝ ≫ g₂✝)

Tactic:
rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
      Bicategory.whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
| (preinclusion B).map { as := p } ◁ η.mk ≫ (normalizeIso p g✝).hom

pp: case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
| (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
rw [ihf]

Goal state after:
case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
| (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

case a
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
| (preinclusion B).map₂ (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t : LeftExtension f g
i : s ≅ t
x : B
h : c ⟶ x
⊢ StructuredArrow.Hom.right (whiskerHom i.hom h ≫ whiskerHom i.inv h) = StructuredArrow.Hom.right (i.hom ≫ i.inv) ▷ h

Tactic:
simp [-Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ StructuredArrow.Hom.right (whiskerHom i.hom h ≫ whiskerHom i.inv h) = h ◁ StructuredArrow.Hom.right (i.hom ≫ i.inv)

Tactic:
simp [-Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : RightLift f g
i : s ≅ t
x : B
h : x ⟶ c
⊢ (whiskerHom i.hom h ≫ whiskerHom i.inv h).left = h ◁ (i.hom ≫ i.inv).left

Tactic:
simp [-Iso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
⊢ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    ((LeftLift.mk h η').whisker t.extension).unit ≫
      H'.desc
          (LeftLift.mk s'.extension
            ((ρ_ t.extension).hom ≫
              H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))) ▷
        u

Tactic:
(H' _).fac

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
t : LeftExtension f g
H : t.IsKan
x : B
h : c ⟶ x
u : x ⟶ c
adj : h ⊣ u
η' : 𝟙 c ⟶ h ≫ u := adj.unit
H' : (LeftLift.mk h η').IsAbsKan := fun {x_1} ↦ adj.isAbsoluteLeftKanLift
s' : LeftExtension f (g ≫ h)
τ₀' : t.whisker h ⟶ s'
τ' : t.extension ≫ h ⟶ s'.extension := StructuredArrow.Hom.right τ₀'
Hτ' : t.unit ▷ h ⊗≫ f ◁ τ' = s'.unit
⊢ ((LeftLift.mk h η').whisker t.extension).unit ≫ StructuredArrow.Hom.right τ₀' ▷ u =
    (LeftLift.mk s'.extension
        ((ρ_ t.extension).hom ≫
          H.desc (mk (s'.extension ≫ u) (𝟙 g ⊗≫ g ◁ η' ⊗≫ s'.unit ▷ u ⊗≫ 𝟙 (f ≫ s'.extension ≫ u))))).unit
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
⊢ (connectedComponents.obj C ⟶ X) ≃ (C ⟶ typeToCat.obj X)

Tactic:
refine TypeCat.homEquiv.trans ?_

Goal state after:
X✝ : Type u
C✝ : Cat
C : Cat
X : Type u
⊢ (connectedComponents.obj C → X) ≃ (C ⟶ typeToCat.obj X)
Module: Mathlib.CategoryTheory.ConnectedComponents

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ ∀ {X Y : Decomposed J}, Function.Injective (decomposedTo J).map

Tactic:
rintro ⟨_, j, rfl⟩ ⟨_, k, hY⟩ ⟨⟨f⟩⟩ ⟨⟨_⟩⟩ rfl

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j k : J
hY : ConnectedComponents.objectProperty (Quotient.mk'' j) k
f : { obj := j, property := ⋯ }.obj ⟶ { obj := k, property := hY }.obj
⊢ Sigma.SigmaHom.mk { hom := f } = Sigma.SigmaHom.mk { hom := (decomposedTo J).map (Sigma.SigmaHom.mk { hom := f }) }
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
⊢ opFunctor.IsEquivalence

Tactic:
by
  change opEquivalence.functor.IsEquivalence
  infer_instance

Goal state after:
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
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
x✝⁴ : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
m : (Cofan.mk B π).pt ⟶ W✝
hm : hc.desc (Cofan.mk B π) ≫ m = e
Z✝ : C
x✝³ x✝² : α
x✝¹ : Z✝ ⟶ X x✝³
x✝ : Z✝ ⟶ X x✝²
hg : x✝¹ ≫ π x✝³ = x✝ ≫ π x✝²
⊢ x✝¹ ≫ c.ι.app { as := x✝³ } ≫ e = x✝ ≫ c.ι.app { as := x✝² } ≫ e

Tactic:
by simp [← hm, reassoc_of% hg]

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

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

Tactic:
rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
  congr
  exact left_inv h

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
V₁ V₂ : Coalgebra G
f : V₁ ⟶ V₂
⊢ F.map f.f ≫ (adj.homEquiv V₂.V V₂.V).symm V₂.str = (adj.homEquiv V₁.V V₁.V).symm V₁.str ≫ f.f

Tactic:
by
  rw [← Adjunction.homEquiv_naturality_left_symm, ← Adjunction.homEquiv_naturality_right_symm,
    f.h]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
⊢ ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ.hom = φ'

Tactic:
intro a' g τ hτ

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst✝ : p.IsHomLift f φ.hom
a' : 𝒳
g : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (g ≫ f) τ
⊢ ∃! χ, p.IsHomLift g χ ∧ χ ≫ φ.hom = τ
Module: Mathlib.CategoryTheory.FiberedCategory.Fiber

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
S : 𝒮
X✝ Y✝ : p.Fiber S
φ : X✝ ⟶ Y✝
⊢ (fiberInclusion ⋙ p).map φ ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ ((const (p.Fiber S)).obj S).map φ

Tactic:
by simp [IsHomLift.fac' p (𝟙 S) (fiberInclusion.map φ)]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
⊢ ShortComplex.QuasiIso f ↔ ∀ (i : I), ShortComplex.QuasiIso ((F i).mapShortComplex.map f)

Tactic:
refine ⟨fun hf i ↦ inferInstance, fun hf ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S₁ S₂ : ShortComplex C
f : S₁ ⟶ S₂
hf : ∀ (i : I), ShortComplex.QuasiIso ((F i).mapShortComplex.map f)
⊢ ShortComplex.QuasiIso f
Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Goal state before:
pp: G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
| (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y

Tactic:
rw [Setoid.comm']

Goal state after:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
| (MulAction.orbitRel G (J.obj (SingleObj.star G))) y x
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
g h : G
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom ((NatIso.ofComponents (isoOnObj F (g * h)) ⋯).hom.app X)) x =
    (ConcreteCategory.hom ((NatIso.ofComponents (isoOnObj F g) ⋯ * NatIso.ofComponents (isoOnObj F h) ⋯).hom.app X)) x

Tactic:
apply mul_smul

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
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).obj
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨t, ht⟩ := MulAction.exists_smul_eq (Aut F) x y
    obtain ⟨g, rfl⟩ := h t
    exact ⟨g, ht⟩

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Over

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : ∀ (Y : C), HasBinaryProduct X Y
inst✝ : ∀ (Y : C), PreservesLimit (pair X Y) F
W : Over (F.obj X)
Z : C
g : (Over.forget (F.obj X)).obj W ⟶ F.obj Z
P : (TwoSquare.overPost F X).StructuredArrowRightwards g := ⋯
this : Nonempty ((TwoSquare.overPost F X).StructuredArrowRightwards g)
Q : (TwoSquare.overPost F X).StructuredArrowRightwards g
⊢ ((Over.Hom.left (StructuredArrow.hom Q).left ≫
          F.map (prod.lift (StructuredArrow.right Q).left.hom (StructuredArrow.right Q).hom)) ≫
        prodComparison F X Z) ≫
      prod.fst =
    (Over.Hom.left (StructuredArrow.hom P).left ≫ prodComparison F X Z) ≫ prod.fst

Tactic:
simpa [← Functor.map_comp, P] using Over.w Q.hom.left

Goal state after: