mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ IsIndObject (colimit F)

Tactic:
refine (isIndObject_iff _).mpr ⟨this, ?_⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ (ConcreteCategory.hom (limit.π (F.op ⋙ G) i))
      ((ConcreteCategory.hom (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).symm.hom)
          ((ConcreteCategory.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom)
            ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))

Tactic:
refine Eq.trans (dsimp% this _) ?_

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type u₁
inst✝³ : Category.{v₁, u₁} I
inst✝² : HasColimitsOfShape I (Type v)
inst✝¹ : HasLimitsOfShape Iᵒᵖ (Type v)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : I ⥤ C
G : Cᵒᵖ ⥤ Type v
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    ((ConcreteCategory.hom
            ((preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)).inv ≫ uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i)))
          a).down =
      ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i)) a).down
⊢ ((ConcreteCategory.hom (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i))
        ((ConcreteCategory.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm).hom)
          ((ConcreteCategory.hom (colimitYonedaHomIsoLimitOp F G).hom) η))).down =
    (ConcreteCategory.hom (η.app (op (F.obj (unop i)))))
      ((ConcreteCategory.hom ((colimit.ι (F ⋙ yoneda) (unop i)).app (op (F.obj (unop i))))) (𝟙 (F.obj (unop i))))
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (yoneda.obj A).map (colimit.ι F (op i)).op

Tactic:
rw [coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, Functor.flip_map_app]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)

Tactic:
have : PreservesFiniteColimits (F C) := by rw [F]; infer_instance

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : PreservesFiniteColimits (F C)
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
⊢ pullback.snd ((finiteSubcoproductsCocone fun x ↦ G).ι.app F) (kernel.ι (d g)) ≫ kernel.ι (d g) ≫ d f = 0

Tactic:
finiteSubcoproductsCocone_ι_app_eq_sum,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
⊢ pullback.snd (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
      kernel.ι (d g) ≫ d f =
    0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case h
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
⊢ (fun g ↦ app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c)) ≈ b

Tactic:
refine ⟨pullback (Abelian.factorThruImage S.f) c, 𝟙 _,
              pullback.snd _ _, inferInstance, inferInstance, ?_⟩

Goal state after:
case h
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 (Abelian.factorThruImage S.f) c) ≫
      ((fun g ↦ app S.f g) (Over.mk (pullback.fst (Abelian.factorThruImage S.f) c))).hom =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasInjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
n : ℕ
X : C
inst✝ : Injective X
⊢ IsZero ((InjectiveResolution.self X).cocomplex.X (n + 1))

Tactic:
by apply isZero_zero

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (P.ι.f 0) ≫ F.map (P.cocomplex.d 0 1) = 0

Tactic:
rw [← F.map_comp, HomologicalComplex.Hom.comm, HomologicalComplex.single_obj_d,
      zero_comp, F.map_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y Z : C
⊢ ∀ (i : X ⟶ Y), isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)

Tactic:
i

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y Z : C
i : X ⟶ Y
⊢ isomorphisms C i → ∀ (f : Y ⟶ Z), ofObjectProperty P Q f → ofObjectProperty P Q (i ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
X Y Z : C
⊢ ∀ (i : Y ⟶ Z), isomorphisms C i → ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q (f ≫ i)

Tactic:
i

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
X Y Z : C
i : Y ⟶ Z
⊢ isomorphisms C i → ∀ (f : X ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q (f ≫ i)
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v g : G
⊢ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯) =
    FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g

Tactic:
ext (x : G ⧸ N)
      induction x using Quotient.inductionOn with | h x
      dsimp
      apply (Quotient.lift_mk _ _ _).trans
      simp only [QuotientGroup.mk_mul, mul_assoc]
      rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
⊢ { hom := FintypeCat.homMk (Quotient.lift (fun σ ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ } = 1

Tactic:
apply Action.hom_ext
    ext (x : G ⧸ N)
    induction x using Quotient.inductionOn
    simp

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : Fintype (G ⧸ H)
h : N ≤ H
g : G
⊢ (ofMulAction G (FintypeCat.of (G ⧸ N))).ρ g ≫ FintypeCat.homMk (Quotient.lift (fun x ↦ ⟦x⟧) ⋯) =
    FintypeCat.homMk (Quotient.lift (fun x ↦ ⟦x⟧) ⋯) ≫ (ofMulAction G (FintypeCat.of (G ⧸ H))).ρ g

Tactic:
by
    ext (x : G ⧸ N)
    induction x using Quotient.inductionOn
    rfl

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
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
⊢ ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

pp: case refine_2
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' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f

Tactic:
· suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Mono (L.map f)),
      ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono f'),
          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
        let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩
    intro X Y f hf
    rw [mono_map_iff L P] at hf
    refine ⟨_, _, Abelian.image.ι f, inferInstance, ⟨Iso.symm ?_⟩⟩
    have := Localization.inverts L P.isoModSerre _ hf.isoModSerre_factorThruImage
    exact Arrow.isoMk (asIso (L.map (Abelian.factorThruImage f))) (Iso.refl _)
      (by simp [← L.map_comp])

Goal state after:
case refine_2
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' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫ otherMap L U' adj₁ adj₂ X = f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X)))) ((adj₂.homEquiv Y (F.obj X)).symm f ≫ F.map (adj₁.unit.app X))

Tactic:
otherMap,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫
        adj₂.unit.app (U'.1 (F.obj X)) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X)))) ((adj₂.homEquiv Y (F.obj X)).symm f ≫ F.map (adj₁.unit.app X))
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ (adj₂.homEquiv (U.obj ((U ⋙ F).obj X)) Y) (otherMap R F' adj₁ adj₂ X ≫ f) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj ((𝟭 B).obj X)) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f

Tactic:
otherMap,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ (adj₂.homEquiv (U.obj ((U ⋙ F).obj X)) Y)
        ((F'.map (U.map (F.map (adj₂.unit.app (U.1 X)) ≫ adj₁.counit.app (R.obj (F'.obj (U.1 X))))) ≫
            adj₂.counit.app (F'.obj (U.1 X))) ≫
          f) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj ((𝟭 B).obj X)) Y) f ↔
    U.map (F.map ((adj₂.homEquiv (U.obj X) Y) f) ≫ adj₁.counit.app (R.obj Y)) =
      U.map (adj₁.counit.app X) ≫ (adj₂.homEquiv (U.obj X) Y) f
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b : B
f g : a ⟶ b
β : f ⟶ g
⊢ 𝟙 (F.map f ≫ η.vCompApp θ b) ⊗≫
      η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map₂ β ▷ θ.app b ≫ θ.naturality g) ⊗≫ 𝟙 ((η.app a ≫ θ.app a) ≫ H.map g) =
    η.vCompNaturality θ f ≫ η.vCompApp θ a ◁ H.map₂ β

Tactic:
rw [θ.naturality_naturality]
      bicategory

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F G H : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
α : F ⟶ G
a : ∫ᶜ F
⊢ { base := (𝟙 a).base,
      fiber :=
        (α.app { as := op a.base }).toFunctor.map (𝟙 a).fiber ≫
          (α.naturality (𝟙 a).base.op.toLoc).hom.toNatTrans.app a.fiber } =
    𝟙 { base := a.base, fiber := (α.app { as := op a.base }).toFunctor.obj a.fiber }

Tactic:
by
    ext1
    · dsimp
    · simp [Cat.Hom.comp_toFunctor, naturality_id_hom_app, Cat.Hom.id_toFunctor, ← Category.assoc,
        ← Functor.map_comp, ← Cat.Hom₂.comp_app]

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
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
f₀₂ : b₀ ⟶ b₂
f₁₃ : b₁ ⟶ b₃
f : b₀ ⟶ b₃
h₀₂ : f₀₁ ≫ f₁₂ = f₀₂
h₁₃ : f₁₂ ≫ f₂₃ = f₁₃
hf : f₀₂ ≫ f₂₃ = f
⊢ (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    (F.mapComp' f₀₁ f₁₃ f ⋯).hom ≫
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
        (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃

Tactic:
by
  simp [← mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc _ _ _ _ _ _ f h₀₂ h₁₃ hf]

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
b₀ b₁ b₂ b₃ : B
f₀₁ : b₀ ⟶ b₁
f₁₂ : b₁ ⟶ b₂
f₂₃ : b₂ ⟶ b₃
this :
  F.mapComp f₀₁ f₁₂ ▷ F.map f₂₃ ≫ F.mapComp (f₀₁ ≫ f₁₂) f₂₃ ≫ F.map₂ (eqToHom ⋯) =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom ≫ F.map f₀₁ ◁ F.mapComp f₁₂ f₂₃ ≫ F.mapComp f₀₁ (f₁₂ ≫ f₂₃)
⊢ F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ (f₁₂ ≫ f₂₃) ⋯ ≫ F.mapComp' f₀₁ (f₁₂ ≫ f₂₃) (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯ =
    (α_ (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv ≫
      F.mapComp' f₀₁ f₁₂ (f₀₁ ≫ f₁₂) ⋯ ▷ F.map f₂₃ ≫ F.mapComp' (f₀₁ ≫ f₁₂) f₂₃ (f₀₁ ≫ f₁₂ ≫ f₂₃) ⋯

Tactic:
simp [LaxFunctor.mapComp', this]

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case h.left
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
x : X
⊢ ∃ y, ((ConcreteCategory.hom (↾f ≫ ↾g)).toFun x, y) ∈ r.rel ∧ (y, (ConcreteCategory.hom (𝟙 X)).toFun x) ∈ (inv r).rel

Tactic:
use f x, (hg _).2, (hf _).2

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
⊢ L.Final

Tactic:
by
  let sA : A ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} A := AsSmall.equiv
  let sB : B ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} B := AsSmall.equiv
  let sT : T ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} T := AsSmall.equiv
  let L' := sA.inverse ⋙ L ⋙ sT.functor
  let R' := sB.inverse ⋙ R ⋙ sT.functor
  have (b : _) : (CostructuredArrow.toOver L' (R'.obj b)).Final := by
    dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢
    let x := (sB.inverse ⋙ R ⋙ sT.functor).obj b
    let F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 _) x :=
      map₂ (F := sA.inverse) (G := sT.inverse) (whiskerLeft (sA.inverse ⋙ L) sT.unit) (𝟙 _) ⋙
      pre L (𝟭 T) (R.obj _) ⋙ map₂ (F := sT.functor) (G := sT.functor) (𝟙 _) (𝟙 _)
    apply final_of_natIso (F := F'')
    have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl
    exact NatIso.ofComponents (fun X => CostructuredArrow.isoMk (Iso.refl _) (by simp [F'', hsT]))
  have := final_of_final_costructuredArrowToOver_small L' R'
  apply final_of_natIso (F := (sA.functor ⋙ L' ⋙ sT.inverse))
  exact (sA.functor.associator (sA.inverse ⋙ L ⋙ sT.functor) sT.inverse).symm ≪≫
    ((sA.functor.associator sA.inverse (L ⋙ sT.functor)).symm ≪≫
      isoWhiskerRight sA.unitIso.symm _ ≪≫ (L ⋙ sT.functor).leftUnitor).compInverseIso

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
⊢ F.map (h.to { a := F.obj A.a, str := F.map A.str }).f ≫ { a := F.obj A.a, str := F.map A.str }.str = F.map (𝟙 A.a)

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
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
⊢ V₀.str ≫ F.map h.hom ≫ F.map h.inv = V₀.str

Tactic:
← F.map_comp

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
⊢ V₀.str ≫ F.map (h.hom ≫ h.inv) = 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
⊢ { V := F.obj A.V, str := F.map A.str }.str ≫ F.map (h.from { V := F.obj A.V, str := F.map A.str }).f = F.map (𝟙 A.V)

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ F.map (A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f) = F.map (𝟙 A.V)
Module: Mathlib.CategoryTheory.Equivalence.Symmetry

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X✝ Y✝ : C ≌ D
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ≌ D)).map x✝ ≫ (Iso.refl ((𝟭 (C ≌ D)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (C ≌ D)).obj X✝)).hom ≫ (symmEquivFunctor C D ⋙ symmEquivInverse C D).map x✝

Tactic:
by
      ext c
      simp [symm, symmEquivInverse]

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (fst✝, x₂')
h₁₂ : snd✝ = fst✝
⊢ ROfRel φ

Tactic:
← h₁₂

Goal state after:
X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (snd✝, x₂')
h₁₂ : snd✝ = fst✝
⊢ ROfRel φ
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
hRS : R = S
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (eqToHom hRS) (𝟙 a)

Tactic:
by
  subst hRS ha; simp

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

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 φ
a' : 𝒳
h : a' = a
⊢ p.IsHomLift f (eqToHom h ≫ φ)

Tactic:
by
  subst h; simp_all

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

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 φ
b' : 𝒳
h : b = b'
⊢ p.IsHomLift f (φ ≫ eqToHom h)

Tactic:
by
  subst h; simp_all

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

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 φ
R' : 𝒮
h : R' = R
⊢ p.IsHomLift (eqToHom h ≫ f) φ

Tactic:
by
  subst h; simp_all

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

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 φ
S' : 𝒮
h : S = S'
⊢ p.IsHomLift (f ≫ eqToHom h) φ

Tactic:
by
  subst h; simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit

Goal state before:
pp: K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
⊢ IsFiltered K

Tactic:
refine IsFiltered.iff_nonempty_limit.2 (fun {J} _ _ F => ?_)

Goal state after:
K : Type v
inst✝ : SmallCategory K
h :
  ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ K ⥤ Type v),
    Nonempty (limit (colimit F.flip) ⟶ colimit (limit F))
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))