mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : P ⟶ Q := ⋯
t : P ⟶ Q := ⋯
I : C := ⋯
i : I ⟶ P := ⋯
⊢ G.map i ≫ G.map s = G.map i ≫ G.map t

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ G.map (i ≫ s) = G.map i ≫ G.map t
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ IsColimit (CokernelCofork.ofπ g ⋯)

Tactic:
refine IsColimit.ofIsoColimit (ModuleCat.cokernelIsColimit f) <|
    Cocone.ext (((Submodule.quotEquivOfEq _ _ (LinearMap.exact_iff.mp H)).toModuleIso).symm
    ≪≫ ((LinearMap.quotKerEquivOfSurjective _ H₂).toModuleIso)) ?_
  · rintro ⟨⟩ <;> ext x
    · simpa using! (Function.Exact.apply_apply_eq_zero H x).symm
    · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (Fork.ι c) ≫ G.map f = 0

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (Fork.ι c ≫ f) = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (f ≫ q) = G.map p ≫ G.map g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map f ≫ G.map (Cofork.π c) = 0

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (f ≫ Cofork.π c) = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (f ≫ q) = G.map p ≫ G.map g
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ G.map s ≫ G.map i = G.map t ≫ G.map i

Tactic:
← G.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f ↦ colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ G.map (s ≫ i) = G.map t ≫ G.map i
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
⊢ Mono (r A)

Tactic:
apply NormalEpiCategory.mono_of_cancel_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) := ⋯
⊢ ∀ (Z : C) (g : Z ⟶ A), g ≫ r A = 0 → g = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ - -b - (0 - a) = b - -a

Tactic:
neg_neg b,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ b - (0 - a) = b - -a
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (imageMonoFactorisation f).e

Tactic:
imageMonoFactorisation_e'

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (cokernel.π (kernel.ι f) ≫ coimageImageComparison f)
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := Arrow.Hom.left e.inv
β : S₂ ⟶ S₄ := Arrow.Hom.right e.hom
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso φ'

Tactic:
rw [this]
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Tactic:
dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl, leftHomologyMapIso', leftHomologyIso,
    RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', rightHomologyIso]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫
      (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S) S.rightHomologyData h₂
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.homologyπ ≫ homologyMap φ ≫ S₂.homologyι = S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles

Tactic:
by
  simp only [homologyι_naturality, homology_π_ι_assoc, p_opcyclesMap]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h₁.IsPreservedBy F
inst✝ : h₂.IsPreservedBy F
⊢ F.map ψ.φH ≫ (h₂.map F).ι = (h₁.map F).ι ≫ F.map ψ.φQ

Tactic:
by simpa only [F.map_comp] using! F.congr_map ψ.commι

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) = (π₁.mapCocone s).ι.app j
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
⊢ (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) ≫ s.pt.f =
    (π₁.mapCocone c).ι.app j ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)

Tactic:
have eq₁₂ := fun j => (c.ι.app j).comm₁₂

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) = (π₁.mapCocone s).ι.app j
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ (((const J).obj c.pt).obj j).f = (F.obj j).f ≫ (c.ι.app j).τ₂
⊢ (π₁.mapCocone c).ι.app j ≫ h₁.desc (π₁.mapCocone s) ≫ s.pt.f =
    (π₁.mapCocone c).ι.app j ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map γ.φH = (γ.map F).φH

Tactic:
ShortComplex.LeftHomologyMapData.map_φH

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
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map γ.φH = F.map γ.φH
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ adj.unit.app X ≫ G.map (F.map g) ≫ G.map w = f

Tactic:
← G.map_comp,

Goal state after:
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.PreservesMonomorphisms
I : D
hI : Injective I
X Y : C
f : X ⟶ G.obj I
g : X ⟶ Y
inst✝ : Mono g
w : F.obj Y ⟶ I
h : F.map g ≫ w = F.map f ≫ adj.counit.app I
⊢ adj.unit.app X ≫ G.map (F.map g ≫ w) = f
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Epi S₂.g

Tactic:
by
    suffices Epi (e.hom.τ₂ ≫ S₂.g) by
      exact epi_of_epi e.hom.τ₂ _
    have := h.epi_g
    rw [e.hom.comm₂₃]
    apply epi_comp

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
i : D ⥤ C
inst✝¹ : Reflective i
A : C
inst✝ : IsSplitMono ((reflectorAdjunction i).unit.app A)
η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
this : IsIso (η.app (i.obj ((reflector i).obj A)))
⊢ Epi (η.app ((reflector i ⋙ i).obj A) ≫ (reflector i ⋙ i).map (retraction (η.app A)))

Tactic:
apply epi_comp (η.app (i.obj ((reflector i).obj A)))

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
a✝ : Epi S.f
⊢ S.Exact

Tactic:
rw [(HomologyData.ofIsColimitCokernelCofork S hg _
      (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (0 : S.X₂ ⟶ 0) comp_zero)
        inferInstance (isZero_zero C))).exact_iff]

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
a✝ : Epi S.f
⊢ IsZero
    (HomologyData.ofIsColimitCokernelCofork S hg (CokernelCofork.ofπ 0 ⋯)
          (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ 0 ⋯) ⋯ ⋯)).left.H
Module: Mathlib.CategoryTheory.Subobject.FactorThru

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
⊢ P.factorThru f h = 0 → f = 0

Tactic:
intro w
    replace w := w =≫ P.arrow
    simpa using w

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
X Y : Subobject B
h : X ≤ Y
⊢ Mono (X.ofLE Y h)

Tactic:
fconstructor
  intro Z f g w
  replace w := w =≫ Y.arrow
  ext
  simpa using w

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

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Mono f
inst✝ : Mono g
t : MonoOver X
⊢ (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))

Tactic:
exact Quotient.sound ⟨(MonoOver.mapComp _ _).app t⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A B : C
X : Subobject B
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ underlying.obj X
w : h ≫ X.arrow = f
⊢ (imageSubobjectIso f).hom ≫ image.ι f = (imageSubobject f).arrow

Tactic:
imageSubobject_arrow

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A B : C
X : Subobject B
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ underlying.obj X
w : h ≫ X.arrow = f
⊢ (imageSubobject f).arrow = (imageSubobject f).arrow
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : S.Exact
⊢ IsLimit (KernelFork.ofι (Abelian.image.ι S.f) ⋯)

Tactic:
by
  rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
  exact KernelFork.IsLimit.ofι _ _
    (fun u hu ↦ kernel.lift (cokernel.π S.f) u
      (by rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero])) (by simp)
    (fun _ _ _ hm => by rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι])

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
g'✝ : S.X₂ ⟶ Z'✝
eq'✝ : S.f ≫ g'✝ = 0
m✝ : Abelian.coimage S.g ⟶ Z'✝
hm : Abelian.coimage.π S.g ≫ m✝ = g'✝
⊢ coequalizer.π (kernel.ι S.g) 0 ≫ m✝ = coequalizer.π (kernel.ι S.g) 0 ≫ cokernel.desc (kernel.ι S.g) g'✝ ⋯

Tactic:
rw [hm, cokernel.π_desc]

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ x✝ : Subobject A
⊢ f₁ ⊓ x✝ = (inf.obj (Quotient.mk'' (representative.obj f₁))).obj x✝

Tactic:
← thinSkeleton_mk_representative_eq_self f₁

Goal state after:
case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ f₂ x✝ : Subobject A
⊢ ThinSkeleton.mk (representative.obj f₁) ⊓ x✝ = (inf.obj (Quotient.mk'' (representative.obj f₁))).obj x✝
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (kernel.ι α).app X = kernelComparison α ((evaluation C D).obj X) ≫ kernel.ι (α.app X)

Tactic:
exact (kernelComparison_comp_ι _ ((evaluation C D).obj X)).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ IsIso (coimageImageComparison α)

Tactic:
by
  have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) := by
    intros
    rw [coimageImageComparison_app']
    infer_instance
  apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝² : Category.{v_3, u_3} H
inst✝¹ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
X : D
f : StructuredArrow X L
⊢ (L.ranObjObjIsoLimit F X).hom ≫ limit.π (StructuredArrow.proj X L ⋙ F) f =
    (L.ran.obj F).map f.hom ≫ (L.ranCounit.app F).app f.right

Tactic:
by
  simp [ranObjObjIsoLimit, ran, ranCounit]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ (CostructuredArrow.left G).map φ ≫ (G.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X

Tactic:
simpa using ((h Y₁).fac (coneAt G Y₁) ((StructuredArrow.map φ).obj X)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
⊢ (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).ι.app j ≫
      (Iso.refl (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).pt).hom =
    ((LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).coconeAt X).ι.app j

Tactic:
dsimp
    simp only [comp_id, colimit.ι_desc, CostructuredArrow.map_mk]
    congr 1
    rw [id_comp, ← CostructuredArrow.eq_mk]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
· simpa [unitForward, unitBackward] using congrArg yonedaEquiv.symm p.snd.app_val

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ colim ⋙ e.functor ≅ colim

Tactic:
apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
this : HasColimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.symm.congrRight.functor.obj (e.congrRight.inverse ⋙ colim ⋙ e.functor) ≅ e.symm.congrRight.functor.obj colim