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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
f : φ.obj cm.X₂ ⟶ φ.obj Y
⊢ φ.map ((ConcreteCategory.hom f) (𝟙 G)) = f

Tactic:
by cat_disch

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

Goal state before:
pp: case max.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.max ⋯ ⋯ x y)⟩ =
    {
        obj :=
          max (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
            (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
      rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
      rfl

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

Goal state before:
pp: case coeq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (FilteredClosureSmall.bundledAbstractFilteredClosure f n).fst
hj₁ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (FilteredClosureSmall.bundledAbstractFilteredClosure f m).fst
hj₂ : filteredClosure f (FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩)
g g' :
  FilteredClosureSmall.abstractFilteredClosureRealization f ⟨n, x⟩ ⟶
    FilteredClosureSmall.abstractFilteredClosureRealization f ⟨m, y⟩
⊢ FilteredClosureSmall.abstractFilteredClosureRealization f
      ⟨(Max.max n m).succ, ⋯.mpr (FilteredClosureSmall.InductiveStep.coeq ⋯ ⋯ x y g g')⟩ =
    { obj := coeq g g', property := ⋯ }.obj

Tactic:
simp only [FilteredClosureSmall.abstractFilteredClosureRealization]
      rw! [FilteredClosureSmall.bundledAbstractFilteredClosure]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : (fun X ↦ X)
  (limit
    (colimit
      (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)))) :=
  (ConcreteCategory.hom (limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom)) t
t₃ : (fun X ↦ X)
  (colimit
    (limit
      (H ⋙
          yoneda ⋙
            (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
              (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip)) :=
  (ConcreteCategory.hom
      (colimitLimitIso
          (H ⋙
              yoneda ⋙
                (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                  (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).inv)
    t₂
k : K
y :
  (limit
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).obj
    k
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
refine ⟨k, ⟨?_⟩⟩

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
t : limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (colimit H))
t₂ : (fun X ↦ X)
  (limit
    (colimit
      (H ⋙
        yoneda ⋙
          (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
            (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)))) :=
  (ConcreteCategory.hom (limMap (compYonedaColimitIsoColimitCompYoneda F G H).hom)) t
t₃ : (fun X ↦ X)
  (colimit
    (limit
      (H ⋙
          yoneda ⋙
            (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
              (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip)) :=
  (ConcreteCategory.hom
      (colimitLimitIso
          (H ⋙
              yoneda ⋙
                (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                  (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).inv)
    t₂
k : K
y :
  (limit
        (H ⋙
            yoneda ⋙
              (whiskeringLeft Jᵒᵖ (Over (colimit F))ᵒᵖ (Type (max u v))).obj
                (G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op)).flip).obj
    k
⊢ limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k))
Module: Mathlib.CategoryTheory.Comma.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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
Q : CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToLeft j₁.right j₂.right) = L.map va₂ ≫ j₁.hom
ib : A
vb₁ : ib ⟶ Q.left
vb₂ : ib ⟶ j₂.left
heqb : L.map vb₁ ≫ Q.hom ≫ R.map (IsCofiltered.minToRight j₁.right j₂.right) = L.map vb₂ ≫ j₂.hom
i₀ : A
il₀ : i₀ ⟶ ia
ir₀ : i₀ ⟶ ib
heq : il₀ ≫ va₁ = ir₀ ≫ vb₁
⊢ L.map (ir₀ ≫ vb₂) ≫ j₂.hom =
    { left := i₀, right := IsCofiltered.min j₁.right j₂.right, hom := L.map (il₀ ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.minToRight j₁.right j₂.right)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
this : IsCofiltered.eqHom u.right v.right ≫ u.right = IsCofiltered.eqHom u.right v.right ≫ v.right
⊢ L.map (β ≫ va₂) ≫ j₁.hom =
    { left := i₀, right := IsCofiltered.eq u.right v.right, hom := L.map (β ≫ va₁) ≫ Q.hom }.hom ≫
      R.map (IsCofiltered.eqHom u.right v.right)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
u v : j₁ ⟶ j₂
Q : CostructuredArrow L (R.obj (IsCofiltered.eq u.right v.right))
ia : A
va₁ : ia ⟶ Q.left
va₂ : ia ⟶ j₁.left
heqa : L.map va₁ ≫ Q.hom ≫ R.map (IsCofiltered.eqHom u.right v.right) = L.map va₂ ≫ j₁.hom
i₀ : A
α : i₀ ⟶ j₁.left
β : i₀ ⟶ ia
hα : α ≫ u.left = β ≫ va₂ ≫ v.left
hβ : α ≫ 𝟙 j₁.left = β ≫ va₂
this : IsCofiltered.eqHom u.right v.right ≫ u.right = IsCofiltered.eqHom u.right v.right ≫ v.right
⊢ { left := β ≫ va₂, right := IsCofiltered.eqHom u.right v.right, w := ⋯ } ≫ u =
    { left := β ≫ va₂, right := IsCofiltered.eqHom u.right v.right, w := ⋯ } ≫ v

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Comma.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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : L.Initial
⊢ IsCofiltered (Comma L R)

Tactic:
by
  have := L.initial_iff_isCofiltered_costructuredArrow.mp inferInstance
  exact isCofiltered_of_isCofiltered_costructuredArrow L R

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
⊢ HasColimit F

Tactic:
let I : α → Type v := fun s => (F.obj ⟨s⟩).presentation.I

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimitsOfShape WalkingParallelPair C
F : WalkingParallelPair ⥤ Ind C
P :
  IndParallelPairPresentation ((Ind.inclusion C).map (F.map WalkingParallelPairHom.left))
    ((Ind.inclusion C).map (F.map WalkingParallelPairHom.right))
⊢ HasColimit F

Tactic:
exact hasColimit_of_iso (diagramIsoParallelPair _ ≪≫ P.parallelPairIsoParallelPairCompIndYoneda)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

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
α : Type u_3
I : α → Type u_4
inst✝¹ : (i : α) → Category.{?u.15, u_4} (I i)
inst✝ : HasLimitsOfShape (Discrete α) C
F : (i : α) → I i ⥤ D ⥤ C
d : D
X✝ Y✝ : (i : α) → I i
f : X✝ ⟶ Y✝
⊢ ∀ (b : α),
    ((pointwiseProduct F ⋙ (evaluation D C).obj d).map f ≫ (piObjIso ((Functor.pi F).obj Y✝) d).hom) ≫
        Pi.π ((Functor.pi fun s ↦ F s ⋙ (evaluation D C).obj d).obj Y✝) b =
      ((piObjIso ((Functor.pi F).obj X✝) d).hom ≫ (pointwiseProduct fun s ↦ F s ⋙ (evaluation D C).obj d).map f) ≫
        Pi.π ((Functor.pi fun s ↦ F s ⋙ (evaluation D C).obj d).obj Y✝) b

Tactic:
by simp [Functor.pi, ← NatTrans.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
Z' : C
I' : InjectiveResolution Z'
f : Z ⟶ Z'
φ : I.Hom I' f
⊢ I.ι ≫ φ.hom = (single₀ C).map f ≫ I'.ι

Tactic:
by cat_disch

Goal state after:
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
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ ∀ (x y : ↥M), MulOpposite.unop ↑(x + y) = MulOpposite.unop ↑x + MulOpposite.unop ↑y

Tactic:
by cat_disch

Goal state after:
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
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ ∀ (m : (End G)ᵐᵒᵖ) (x : ↥M),
    { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯ }.toFun (m • x) =
      (RingHom.id (End G)ᵐᵒᵖ) m • { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯ }.toFun x

Tactic:
by cat_disch

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 Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
erw [(F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.naturality]

Goal state after:
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 Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ ((kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0) ≫ t =
    (𝟙 (kernel t) ≫ equalizer.ι t 0) ≫ t

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ ((kernel.map t b l r ⋯ ≫ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) ≫ equalizer.ι t 0) ≫ l =
    (𝟙 (kernel t) ≫ equalizer.ι t 0) ≫ l

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasKernel t
inst✝ : HasKernel b
sq : IsPullback t l r b
⊢ kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯ ≫ kernel.map t b l r ⋯ = 𝟙 (kernel b)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ cokernel.map t b l r ⋯ ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ = 𝟙 (cokernel t)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ r ≫ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    r ≫ coequalizer.π b 0 ≫ 𝟙 (cokernel b)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst✝¹ : HasCokernel t
inst✝ : HasCokernel b
sq : IsPushout t l r b
⊢ b ≫ coequalizer.π b 0 ≫ cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯ ≫ cokernel.map t b l r ⋯ =
    b ≫ coequalizer.π b 0 ≫ 𝟙 (cokernel b)

Tactic:
by cat_disch

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
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₁ :
  I.toRightDerivedZero' F =
    (injectiveResolution X).toRightDerivedZero' F ≫
      HomologicalComplex.cyclesMap
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) =
    I.toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv

Tactic:
have h₂ : (I.isoRightDerivedToHomotopyCategoryObj F).hom =
    (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (desc (𝟙 X) _ _) :=
    comp_id _

Goal state after:
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
I : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
h₁ :
  I.toRightDerivedZero' F =
    (injectiveResolution X).toRightDerivedZero' F ≫
      HomologicalComplex.cyclesMap
        ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0
h₂ :
  (I.isoRightDerivedToHomotopyCategoryObj F).hom =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
      (desc (𝟙 X) I (injectiveResolution X))
⊢ (injectiveResolution X).toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) =
    I.toRightDerivedZero' F ≫
      ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
Module: Mathlib.CategoryTheory.Abelian.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝⁴ : Abelian C
inst✝³ : P.ContainsZero
inst✝² : P.IsClosedUnderKernels
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : Mono f
this : P.ι.PreservesMonomorphisms
⊢ f ≫ homMk (cokernel.π f.hom) = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝⁴ : Abelian C
inst✝³ : P.ContainsZero
inst✝² : P.IsClosedUnderKernels
inst✝¹ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : Epi f
this : P.ι.PreservesEpimorphisms
⊢ homMk (kernel.ι f.hom) ≫ f = 0

Tactic:
by cat_disch

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.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE

Tactic:
tfae_have 2 → 3 := fun hf ↦ by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_epiModSerre_comp_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    refine ⟨_, s ≫ f, MorphismProperty.comp_mem _ _ _ hs hf, by simpa⟩

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 : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
tfae_2_to_3 : P.epiModSerre f → ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0
⊢ [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), L.map f ≫ L.map z = 0 → L.map z = 0].TFAE
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.PreservesEpimorphisms
this✝ : L.mapArrow.EssSurj
x✝ : Epi f
this :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    Epi (L.map f) → ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f))
⊢ ∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

Tactic:
let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
        obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
          (((MorphismProperty.epimorphisms D).arrow_iso_iff e).2 (.infer_property f))
        exact ⟨_, _, f', inferInstance, ⟨e' ≪≫ e⟩⟩

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
X : Action V PUnit.{?u.12 + 1}
x✝ : PUnit.{?u.12 + 1}
⊢ ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).ρ PUnit.unit ≫ (Iso.refl ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).V).hom =
    (Iso.refl ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).V).hom ≫
      ((forget V PUnit.{?u.12 + 1} ⋙
                { obj := fun X ↦ { V := X, ρ := 1 }, map := fun {X Y} f ↦ { hom := f, comm := ⋯ }, map_id := ⋯,
                  map_comp := ⋯ }).obj
            X).ρ
        PUnit.unit

Tactic:
by
      simp only [Functor.id_obj, MonoidHom.one_apply, End.one_def, Functor.comp_obj,
        forget_obj, Iso.refl_hom, Category.comp_id]
      exact ρ_one X

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y : Action V G
⊢ ∀ (P Q R : Action V G) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g

Tactic:
by intros; ext; exact Preadditive.add_comp _ _ _ _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s : BinaryCofan a b
⊢ pushout.desc (underlying.map (s.ι.app { as := WalkingPair.left }))
        (underlying.map (s.ι.app { as := WalkingPair.right })) ⋯ ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow =
    pushout.desc a.arrow b.arrow ⋯

Tactic:
by cat_disch

Goal state after: