awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
inst_3 : Mono S.f
this : Epi h.f'
⊢ Mono h.f'

Tactic:
have := mono_of_mono_fac h.f'_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
inst_3 : Mono S.f
this_1 : Epi h.f'
this : Mono h.f'
⊢ IsIso h.f'

Tactic:
isIso_of_mono_of_epi h.f'

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
inst_3 : Mono S.f
this_1 : Epi h.f'
this : Mono h.f'
⊢ IsIso h.f'

Tactic:
exact isIso_of_mono_of_epi h.f'

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.f', CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_3 : Mono S.f
inst_4 : S.HasLeftHomology
⊢ IsIso (Y := S.cycles) S.toCycles

Tactic:
hS.isIso_f' _

Premises used: CategoryTheory.ShortComplex.Exact.isIso_f', CategoryTheory.ShortComplex.cycles, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
inst_3 : Epi S.g
⊢ Mono h.g'

Tactic:
have := hS.mono_g' h
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
inst_3 : Epi S.g
this : Mono h.g'
⊢ Epi h.g'

Tactic:
have := epi_of_epi_fac h.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
inst_3 : Epi S.g
this_1 : Mono h.g'
this : Epi h.g'
⊢ IsIso h.g'

Tactic:
isIso_of_mono_of_epi h.g'

Premises used: CategoryTheory.isIso_of_mono_of_epi, CategoryTheory.ShortComplex.RightHomologyData.g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
inst_3 : Epi S.g
this_1 : Mono h.g'
this : Epi h.g'
⊢ IsIso h.g'

Tactic:
exact isIso_of_mono_of_epi h.g'

Premises used: CategoryTheory.isIso_of_mono_of_epi, CategoryTheory.ShortComplex.RightHomologyData.g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_3 : Epi S.g
inst_4 : S.HasRightHomology
⊢ IsIso (X := S.opcycles) S.fromOpcycles

Tactic:
hS.isIso_g' _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.Exact.isIso_g', CategoryTheory.ShortComplex.fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Mono S.f
⊢ S.HasHomology

Tactic:
have := hS.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Mono S.f
this : S.HasHomology
⊢ IsIso (Y := S.cycles) S.toCycles

Tactic:
have := hS.isIso_toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Mono S.f
this_1 : S.HasHomology
this : IsIso (Y := S.cycles) S.toCycles
⊢ Iso.hom (Iso.symm (asIso S.toCycles)) ≫ Fork.ι (KernelFork.ofι S.f ⋯) =
    Fork.ι (KernelFork.ofι (Z := S.cycles) S.iCycles ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Mono S.f
this_1 : S.HasHomology
this : IsIso (Y := S.cycles) S.toCycles
⊢ IsLimit (KernelFork.ofι S.f ⋯)

Tactic:
exact IsLimit.ofIsoLimit S.cyclesIsKernel
    (Fork.ext (asIso S.toCycles).symm (by simp))
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : HasHomology (S.map F)
h : Mono S.f
h_1 : PreservesLimit (parallelPair S.g 0) F
⊢ Exact (S.map F)

Tactic:
exact_of_f_is_kernel _ (KernelFork.mapIsLimit _ hS.fIsKernel F)

Premises used: CategoryTheory.ShortComplex.Exact.fIsKernel, CategoryTheory.Limits.KernelFork.mapIsLimit, CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Epi S.g
⊢ S.HasHomology

Tactic:
have := hS.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Epi S.g
this : S.HasHomology
⊢ IsIso (X := S.opcycles) S.fromOpcycles

Tactic:
have := hS.isIso_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Epi S.g
this_1 : S.HasHomology
this : IsIso (X := S.opcycles) S.fromOpcycles
⊢ Cofork.π (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles ⋯) ≫ Iso.hom (asIso S.fromOpcycles) =
    Cofork.π (CokernelCofork.ofπ S.g ⋯)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Epi S.g
this_1 : S.HasHomology
this : IsIso (X := S.opcycles) S.fromOpcycles
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)

Tactic:
exact IsColimit.ofIsoColimit S.opcyclesIsCokernel
    (Cofork.ext (asIso S.fromOpcycles) (by simp))
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : Balanced.{v_1, u_1} C
hS : S.Exact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_5 : F.PreservesZeroMorphisms
inst_6 : HasHomology (S.map F)
h : Epi S.g
h_1 : PreservesColimit (parallelPair S.f 0) F
⊢ Exact (S.map F)

Tactic:
exact_of_g_is_cokernel _ (CokernelCofork.mapIsColimit _ hS.gIsCokernel F)

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.Limits.CokernelCofork.mapIsColimit
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_3 : Mono S.f
⊢ hS.lift k hk ≫ S.f = k

Tactic:
Fork.IsLimit.lift_ι _

Premises used: CategoryTheory.ShortComplex.Exact.lift, CategoryTheory.Limits.Fork.IsLimit.lift_ι, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_3 : Mono S.f
⊢ hS.lift k hk ≫ S.f = k

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_3 : Epi S.g
⊢ S.g ≫ hS.desc k hk = k

Tactic:
Cofork.IsColimit.π_desc (hS.gIsCokernel)

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, CategoryTheory.ShortComplex.Exact.desc, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst_3 : Epi S.g
⊢ S.g ≫ hS.desc k hk = k

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
rw : ∀ (P : C) (g : P ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0
⊢ Mono φ.τ₂

Tactic:
rw [mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
⊢ x₂ ≫ S₁.g = 0

Tactic:
simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.Hom.τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
obtain : ∀ (x₁ : A ⟶ S₁.X₁) (hx₁ : x₁ ≫ S₁.f = x₂), x₂ = 0
⊢ x₂ = 0

Tactic:
obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S₁.f = x₂ := ⟨_, h₁.lift_f x₂
    (by simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂])⟩

Premises used: CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
rw : x₁ ≫ S₁.f = 0
rw₁ : Eq (α := A ⟶ S₁.X₂) (0 ≫ S₁.f) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := A ⟶ S₁.X₂) 0 0
⊢ x₂ = 0

Tactic:
rw [← hx₁, this, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
suffices : x₁ = 0
⊢ x₂ = 0

Tactic:
suffices x₁ = 0 by rw [← hx₁, this, zero_comp]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
⊢ x₁ = 0

Tactic:
simp only [← cancel_mono φ.τ₁, ← cancel_mono S₂.f, assoc, φ.comm₁₂, zero_comp,
    reassoc_of% hx₁, hx₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.Hom.τ₁, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₁.X₃) (Y := Opposite.op S₁.X₂) S₁.g.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
⊢ Mono S₁.op.f

Tactic:
have : Mono S₁.op.f := by dsimp; infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₃) (Y := Opposite.op S₂.X₂) S₂.g.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono S₂.op.f

Tactic:
have : Mono S₂.op.f := by dsimp; infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₃) (Y := Opposite.op S₁.X₃) φ.τ₃.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono (opMap φ).τ₁

Tactic:
have : Mono (opMap φ).τ₁ := by dsimp; infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S₂.X₁) (Y := Opposite.op S₁.X₁) φ.τ₁.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono (opMap φ).τ₃

Tactic:
have : Mono (opMap φ).τ₃ := by dsimp; infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this_3 : Mono (opMap φ).τ₁
this : Mono (opMap φ).τ₃
⊢ Mono (opMap φ).τ₂

Tactic:
have := mono_τ₂_of_exact_of_mono (opMap φ) h₂.op
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this_3 : Mono (opMap φ).τ₁
this_4 : Mono (opMap φ).τ₃
this : Mono (opMap φ).τ₂
⊢ Epi φ.τ₂

Tactic:
unop_epi_of_mono (opMap φ).τ₂

Premises used: CategoryTheory.unop_epi_of_mono, Quiver.Hom.unop, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.opMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this_3 : Mono (opMap φ).τ₁
this_4 : Mono (opMap φ).τ₃
this : Mono (opMap φ).τ₂
⊢ Epi φ.τ₂

Tactic:
exact unop_epi_of_mono (opMap φ).τ₂

Premises used: CategoryTheory.unop_epi_of_mono, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.opMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
mp : S.Exact ∧ Mono S.f → Nonempty (IsLimit (KernelFork.ofι S.f ⋯))
mpr : Nonempty (IsLimit (KernelFork.ofι S.f ⋯)) → S.Exact ∧ Mono S.f
⊢ S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : S.Exact
right : Mono S.f
⊢ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
⟨hS.fIsKernel⟩

Premises used: CategoryTheory.ShortComplex.Exact.fIsKernel, Nonempty.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : S.Exact
right : Mono S.f
⊢ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
exact ⟨hS.fIsKernel⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : IsLimit (KernelFork.ofι S.f ⋯)
⊢ S.Exact ∧ Mono S.f

Tactic:
⟨S.exact_of_f_is_kernel hS, mono_of_isLimit_fork hS⟩

Premises used: CategoryTheory.Limits.mono_of_isLimit_fork, And.intro, CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : IsLimit (KernelFork.ofι S.f ⋯)
⊢ S.Exact ∧ Mono S.f

Tactic:
exact ⟨S.exact_of_f_is_kernel hS, mono_of_isLimit_fork hS⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
mp : S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))
mpr : Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g
⊢ S.Exact ∧ Epi S.g ↔ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : S.Exact
right : Epi S.g
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
⟨hS.gIsCokernel⟩

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, Nonempty.intro
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : S.Exact
right : Epi S.g
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))

Tactic:
exact ⟨hS.gIsCokernel⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
⊢ S.Exact ∧ Epi S.g

Tactic:
⟨S.exact_of_g_is_cokernel hS, epi_of_isColimit_cofork hS⟩

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, And.intro, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
⊢ S.Exact ∧ Epi S.g

Tactic:
exact ⟨S.exact_of_g_is_cokernel hS, epi_of_isColimit_cofork hS⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
dsimp : Mono (X := kernel f) (kernel.ι f)
⊢ Mono (X := X₁ (kernelSequence f)) (ShortComplex.f (kernelSequence f))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono (X := kernel f) (kernel.ι f)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
dsimp : Epi (Y := cokernel f) (cokernel.π f)
⊢ Epi (X := X₂ (cokernelSequence f)) (g (cokernelSequence f))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi (Y := cokernel f) (cokernel.π f)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Exact (kernelSequence f)

Tactic:
exact_of_f_is_kernel _ (kernelIsKernel f)

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.Limits.kernelIsKernel