mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.fromOpcycles.op ≫ S.cyclesOpIso.inv = S.op.toCycles

Tactic:
dsimp [cyclesOpIso, fromOpcycles]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasRightHomology
⊢ S.rightHomologyData.g'.op ≫ S.rightHomologyData.op.cyclesIso.inv = S.op.toCycles
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 (cyclesMap' φ hl₁ hl₂) = cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + φ₁.τ₁

Tactic:
by rw [h.comm₁, comp_neg]; abel

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
this : ((S.isoCyclesOfIsLimit hkf).inv ≫ π) ≫ ι ≫ (S.isoOpcyclesOfIsColimit hcc).hom = S.iCycles ≫ S.pOpcycles
⊢ H ≅ image (S.iCycles ≫ S.pOpcycles)

Tactic:
exact image.isoStrongEpiMono _ _ this

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + φ₃.τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂.τ₃ + φ₄.τ₃)

Tactic:
h'.comm₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂.τ₃ + φ₄.τ₃)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - φ₃.τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂.τ₃ - φ₄.τ₃)

Tactic:
h'.comm₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂.τ₃ - φ₄.τ₃)
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: case mp
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ IsIso (F.map γ.φH) → IsIso γ.φH

pp: case mpr
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ IsIso γ.φH → IsIso (F.map γ.φH)

Tactic:
· intro
    exact isIso_of_reflects_iso _ F

Goal state after:
case mpr
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
⊢ IsIso γ.φH → IsIso (F.map γ.φH)
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
⊢ QuasiIso (F.mapShortComplex.map φ) ↔ QuasiIso φ

Tactic:
have γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData := default
  rw [γ.quasiIso_iff, (γ.map F).quasiIso_iff, LeftHomologyMapData.map_φH]
  constructor
  · intro
    exact isIso_of_reflects_iso _ F
  · intro
    infer_instance

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

Goal state before:
pp: case mp
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ IsIso (F.map γ.φH) → IsIso γ.φH

pp: case mpr
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ IsIso γ.φH → IsIso (F.map γ.φH)

Tactic:
· intro
    exact isIso_of_reflects_iso _ F

Goal state after:
case mpr
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
⊢ IsIso γ.φH → IsIso (F.map γ.φH)
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := S.X₃, f := h.left.i, g := S.g, zero := ⋯ }
S'' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }.Exact

Tactic:
ShortComplex.exact_iff_of_epi_of_isIso_of_mono b,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := S.X₃, f := h.left.i, g := S.g, zero := ⋯ }
S'' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S'.Exact
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesColimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesCoequalizer_of_preservesCokernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_iso_diagram F (diagramIsoParallelPair K).symm

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesColimit K F

Tactic:
by
    let := preservesCoequalizer_of_preservesCokernels F (K.map Limits.WalkingParallelPairHom.left)
        (K.map Limits.WalkingParallelPairHom.right)
    apply preservesColimit_of_iso_diagram F (diagramIsoParallelPair K).symm

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

Goal state before:
pp: S : ShortComplex Ab
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
by
  rw [S.ab_exact_iff]
  apply forall_congr'
  intro x₂
  constructor
  · intro h
    refine ⟨h, ?_⟩
    rintro ⟨x₁, rfl⟩
    simp only [ab_zero_apply]
  · tauto

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

Goal state before:
pp: case mp
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 : ShortComplex C
inst✝⁴ : S.HasHomology
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : F.Faithful
h : 𝟙 (F.obj S.leftHomologyData.H) = 0
⊢ 𝟙 (F.obj S.leftHomologyData.H) = F.map 0

Tactic:
F.map_zero,

Goal state after:
case mp
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 : ShortComplex C
inst✝⁴ : S.HasHomology
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : F.Faithful
h : 𝟙 (F.obj S.leftHomologyData.H) = 0
⊢ 𝟙 (F.obj S.leftHomologyData.H) = 0
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
hf : S.f = 0
a✝ : Mono S.g
⊢ S.Exact

Tactic:
rw [(HomologyData.ofIsLimitKernelFork S hf _
      (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
        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
hf : S.f = 0
a✝ : Mono S.g
⊢ IsZero
    (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι 0 ⋯)
          (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι 0 ⋯) ⋯ ⋯)).left.H
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.iCycles
this : Epi S.toCycles
⊢ Epi S.f

Tactic:
← S.toCycles_i

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
this✝¹ : S.HasHomology
h : IsZero S.homology
this✝ : IsIso S.iCycles
this : Epi S.toCycles
⊢ Epi (S.toCycles ≫ S.iCycles)
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
⊢ iD.map
      ((Trans.trans
            (Trans.trans
              (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X').homCongr (Iso.refl (iD.obj Y))))
                (adj.homEquiv (iC.obj X') (iD.obj Y)))
              ((Iso.refl (iC.obj X')).homCongr (comm2.app Y)))
            hiC.homEquiv.symm).symm
        (f ≫ g)) =
    iD.map
      (L.map f ≫
        (Trans.trans
              (Trans.trans
                (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                  (adj.homEquiv (iC.obj X) (iD.obj Y)))
                ((Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
              hiC.homEquiv.symm).symm
          g)

Tactic:
simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : QuasiIso φ
⊢ IsZero S₁.homology ↔ IsZero S₂.homology

Tactic:
exact Iso.isZero_iff (asIso (homologyMap φ))

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ Mono S.g

Tactic:
have : S.iCycles = 0 := by rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
⊢ Mono S.g
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X : C
⊢ ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [Mono f] [Mono g] (i : A ≅ B),
    i.hom ≫ g = f → Subobject.mk (cokernel.π f).op = Subobject.mk (cokernel.π g).op

Tactic:
by
        rintro A B f g hf hg i rfl
        refine Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)
        · exact (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
            (isCokernelEpiComp (colimit.isColimit _) i.hom rfl)).symm
        · simp only [Iso.comp_inv_eq, Iso.op_hom, Iso.symm_hom, unop_comp, Quiver.Hom.unop_op,
            colimit.comp_coconePointUniqueUpToIso_hom, Cofork.ofπ_ι_app,
            coequalizer.cofork_π]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
this : factorThruImage S.f ≫ imageToKernel' S.f S.g ⋯ = kernel.lift S.g S.f ⋯
a✝ : Epi (kernel.lift S.g S.f ⋯)
⊢ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
exact epi_of_epi_fac this

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

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
refine preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f) ?_
    apply (CokernelCofork.isColimitMapCoconeEquiv _ F).2
    let S := ShortComplex.mk _ _ (cokernel.condition f)
    let hS := hF S ⟨exact_cokernel f, inferInstance⟩
    have : Epi (S.map F).g := hS.2
    exact hS.1.gIsCokernel

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

Goal state before:
pp: case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (s✝.inf P).Factors f ↔ ∀ i ∈ s✝, (P i).Factors f
⊢ ((insert a✝¹ s✝).inf P).Factors f ↔ ∀ i ∈ insert a✝¹ s✝, (P i).Factors f

Tactic:
| insert _ _ _ ih =>

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

Goal state before:
pp: case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
⊢ ∀ i ∈ insert a✝¹ s✝, (P i).Factors ((insert a✝¹ s✝).inf P).arrow

Tactic:
| insert _ _ _ ih =>

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

Goal state before:
pp: case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
⊢ (∃ i ∈ insert a✝¹ s✝, (P i).Factors f) → ((insert a✝¹ s✝).sup P).Factors f

Tactic:
| insert _ _ _ ih =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.fst.op.unop = prod.fst

Tactic:
Quiver.Hom.unop_op

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.fst = prod.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.snd.op.unop = prod.snd

Tactic:
Quiver.Hom.unop_op

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.snd = prod.snd
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
· have : Infinite J := ⟨h⟩
      let _ := Encodable.ofCountable J
      let _ := Denumerable.ofEncodableOfInfinite J
      exact hasExactColimitsOfShape_of_final C (Discrete.equivalence (Denumerable.eqv J)).inverse

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : StructuredArrow S T
⊢ (∃ a, P a ∧ ∃ b, mk b = X) → P X.right

Tactic:
rintro ⟨_, h, _, rfl⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S ⟶ T.obj w✝¹
⊢ P (mk w✝).right
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
⊢ (∃ a, P a ∧ ∃ b, mk b = X) → P X.left

Tactic:
rintro ⟨_, h, _, rfl⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
w✝¹ : C
h : P w✝¹
w✝ : S.obj w✝¹ ⟶ T
⊢ P (mk w✝).left
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
by rintro ⟨(_ | _), _, (_ | _)⟩ <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Cotrident f
desc : (s : Cotrident f) → t.pt ⟶ s.pt
fac : ∀ (s : Cotrident f), t.π ≫ desc s = s.π
uniq : ∀ (s : Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : WalkingParallelFamily J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
s : Cocone (parallelFamily f)
j : WalkingParallelFamily J
⊢ t.ι.app zero ≫ desc s = s.ι.app zero

Tactic:
rw [← t.w_assoc (line (Classical.arbitrary J)), fac, s.w]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
⊢ (compULiftYonedaIsoULiftYonedaCompLan F).hom.app X ≫
      (compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ (StructuredArrow.hom Φ).app X =
    (StructuredArrow.hom Φ).app X

Tactic:
Iso.hom_inv_id_app_assoc

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
⊢ (StructuredArrow.hom Φ).app X = (StructuredArrow.hom Φ).app X
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x✝ : Mono f
⊢ Mono (free.map f)

Tactic:
by_cases! hX : IsEmpty X

Goal state after:
case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
⊢ Mono (free.map f)

case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Mono (free.map f)