awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this : Epi S.g
mp : IsIso S.f → IsZero.{v_1, u_1} S.X₃
mpr : IsZero.{v_1, u_1} S.X₃ → IsIso S.f
⊢ IsIso S.f ↔ IsZero.{v_1, u_1} S.X₃

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this : Epi S.g
hf : IsIso S.f
⊢ IsZero.{v_1, u_1} S.X₃

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_epi S.g, ← cancel_epi S.f,
      S.zero_assoc, zero_comp]

Premises used: CategoryTheory.ShortComplex.zero_assoc, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this : Epi S.g
hX₃ : IsZero.{v_1, u_1} S.X₃
⊢ Epi S.f

Tactic:
have : Epi S.f := (S.exact_iff_epi (hX₃.eq_of_tgt _ _)).1 hS.exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this_3 : Epi S.g
hX₃ : IsZero.{v_1, u_1} S.X₃
this : Epi S.f
⊢ IsIso S.f

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this : Epi S.g
mp : IsIso S.g → IsZero.{v_1, u_1} S.X₁
mpr : IsZero.{v_1, u_1} S.X₁ → IsIso S.g
⊢ IsIso S.g ↔ IsZero.{v_1, u_1} S.X₁

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this : Epi S.g
hf : IsIso S.g
⊢ IsZero.{v_1, u_1} S.X₁

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_mono S.f, ← cancel_mono S.g,
      S.zero, zero_comp, assoc, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.zero, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this : Epi S.g
hX₁ : IsZero.{v_1, u_1} S.X₁
⊢ Mono S.g

Tactic:
have : Mono S.g := (S.exact_iff_mono (hX₁.eq_of_src _ _)).1 hS.exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.ShortExact
inst_2 : Balanced.{v_1, u_1} C
this_1 : HasZeroObject.{v_1, u_1} C
this_2 : Mono S.f
this_3 : Epi S.g
hX₁ : IsZero.{v_1, u_1} S.X₁
this : Mono S.g
⊢ IsIso S.g

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
⊢ Mono S₁.f

Tactic:
have := h₁.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
this : Mono S₁.f
⊢ Mono S₂.f

Tactic:
have := h₂.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
this_1 : Mono S₁.f
this : Mono S₂.f
⊢ Epi S₁.g

Tactic:
have := h₁.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
this_1 : Mono S₁.f
this_2 : Mono S₂.f
this : Epi S₁.g
⊢ Epi S₂.g

Tactic:
have := h₂.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
this_1 : Mono S₁.f
this_2 : Mono S₂.f
this_3 : Epi S₁.g
this : Epi S₂.g
⊢ Mono φ.τ₂

Tactic:
have := mono_τ₂_of_exact_of_mono φ h₁.exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
this_1 : Mono S₁.f
this_2 : Mono S₂.f
this_3 : Epi S₁.g
this_4 : Epi S₂.g
this : Mono φ.τ₂
⊢ Epi φ.τ₂

Tactic:
have := epi_τ₂_of_exact_of_epi φ h₂.exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
inst_3 : IsIso φ.τ₁
inst_4 : IsIso φ.τ₃
this_1 : Mono S₁.f
this_2 : Mono S₂.f
this_3 : Epi S₁.g
this_4 : Epi S₂.g
this_5 : Mono φ.τ₂
this : Epi φ.τ₂
⊢ IsIso φ.τ₂

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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₁.ShortExact
h₂ : S₂.ShortExact
h : IsIso φ.τ₁
h_1 : IsIso φ.τ₃
⊢ IsIso φ.τ₂

Tactic:
isIso₂_of_shortExact_of_isIso₁₃ φ h₁ h₂

Premises used: CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Mono S.f
⊢ IsLimit (KernelFork.ofι S.f ⋯)

Tactic:
exact hS.exact.fIsKernel

Premises used: CategoryTheory.ShortComplex.Exact.fIsKernel, CategoryTheory.ShortComplex.ShortExact.exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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 : Balanced.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
this : Epi S.g
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)

Tactic:
exact hS.exact.gIsCokernel

Premises used: CategoryTheory.ShortComplex.Exact.gIsCokernel, CategoryTheory.ShortComplex.ShortExact.exact
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.Exact
h : S.HomologyData
⊢ Epi h.left.f'

Tactic:
have := hS.epi_f' h.left
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.Exact
h : S.HomologyData
this : Epi h.left.f'
⊢ Mono h.right.g'

Tactic:
have := hS.mono_g' h.right
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.Exact
h : S.HomologyData
this_1 : Epi h.left.f'
this : Mono h.right.g'
⊢ h.left.i ≫ S.g = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
hS : S.Exact
h : S.HomologyData
this_1 : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex.{v_1, u_1} C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := S.X₃, f := h.left.i, g := S.g, zero := ⋯ }
S'' : ShortComplex.{v_1, u_1} 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₂₃ := ⋯ }
rwa : S'.Exact
rwa₁ rwa₂ rwa₃ rwa₄ : S.Exact
⊢ { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
rwa [ShortComplex.exact_iff_of_epi_of_isIso_of_mono b,
      ← ShortComplex.exact_iff_of_epi_of_isIso_of_mono a]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
inst_3 : Injective.{v_1, u_1} S.X₁
inst_4 : Balanced.{v_1, u_1} C
this : Mono S.f
⊢ S.f ≫ Injective.factorThru (𝟙 S.X₁) S.f = 𝟙 S.X₁

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact
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
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
inst_3 : Projective.{v_1, u_1} S.X₃
inst_4 : Balanced.{v_1, u_1} C
this : Epi S.g
⊢ Projective.factorThru (𝟙 S.X₃) S.g ≫ S.g = 𝟙 S.X₃

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Epi.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S.L₂.X₂) (Y := Opposite.op S.L₂.X₁) S.L₂.f.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Mono.{v_1, u_1} (C := Cᵒᵖ) (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) S.L₁.g.op

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.v₀₁ ≫ S.v₁₂).τ₁ = 0
rw₁ : Eq.{v_1 + 1} (α := S.L₀.X₁ ⟶ S.L₂.X₁) (Hom.τ₁ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.L₀.X₁ ⟶ S.L₂.X₁) 0 0
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₀₂, zero_τ₁]

Premises used: CategoryTheory.ShortComplex.comp_τ₁, CategoryTheory.ShortComplex.SnakeInput.w₀₂, CategoryTheory.ShortComplex.zero_τ₁
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.v₀₁ ≫ S.v₁₂).τ₂ = 0
rw₁ : Eq.{v_1 + 1} (α := S.L₀.X₂ ⟶ S.L₂.X₂) (Hom.τ₂ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.L₀.X₂ ⟶ S.L₂.X₂) 0 0
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₀₂, zero_τ₂]

Premises used: CategoryTheory.ShortComplex.comp_τ₂, CategoryTheory.ShortComplex.SnakeInput.w₀₂, CategoryTheory.ShortComplex.zero_τ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.v₀₁ ≫ S.v₁₂).τ₃ = 0
rw₁ : Eq.{v_1 + 1} (α := S.L₀.X₃ ⟶ S.L₂.X₃) (Hom.τ₃ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.L₀.X₃ ⟶ S.L₂.X₃) 0 0
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₀₂, zero_τ₃]

Premises used: CategoryTheory.ShortComplex.zero_τ₃, CategoryTheory.ShortComplex.SnakeInput.w₀₂, CategoryTheory.ShortComplex.comp_τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.v₁₂ ≫ S.v₂₃).τ₁ = 0
rw₁ : Eq.{v_1 + 1} (α := S.L₁.X₁ ⟶ S.L₃.X₁) (Hom.τ₁ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.L₁.X₁ ⟶ S.L₃.X₁) 0 0
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₁₃, zero_τ₁]

Premises used: CategoryTheory.ShortComplex.comp_τ₁, CategoryTheory.ShortComplex.zero_τ₁, CategoryTheory.ShortComplex.SnakeInput.w₁₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.v₁₂ ≫ S.v₂₃).τ₂ = 0
rw₁ : Eq.{v_1 + 1} (α := S.L₁.X₂ ⟶ S.L₃.X₂) (Hom.τ₂ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.L₁.X₂ ⟶ S.L₃.X₂) 0 0
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₁₃, zero_τ₂]

Premises used: CategoryTheory.ShortComplex.comp_τ₂, CategoryTheory.ShortComplex.SnakeInput.w₁₃, CategoryTheory.ShortComplex.zero_τ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw : (S.v₁₂ ≫ S.v₂₃).τ₃ = 0
rw₁ : Eq.{v_1 + 1} (α := S.L₁.X₃ ⟶ S.L₃.X₃) (Hom.τ₃ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.L₁.X₃ ⟶ S.L₃.X₃) 0 0
⊢ S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₁₃, zero_τ₃]

Premises used: CategoryTheory.ShortComplex.zero_τ₃, CategoryTheory.ShortComplex.comp_τ₃, CategoryTheory.ShortComplex.SnakeInput.w₁₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Mono S.v₀₁.τ₁

Tactic:
mono_of_isLimit_fork S.h₀τ₁

Premises used: CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.ShortComplex.SnakeInput.h₀τ₁, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Mono S.v₀₁.τ₂

Tactic:
mono_of_isLimit_fork S.h₀τ₂

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₀τ₂, CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Mono S.v₀₁.τ₃

Tactic:
mono_of_isLimit_fork S.h₀τ₃

Premises used: CategoryTheory.Limits.mono_of_isLimit_fork, CategoryTheory.Limits.Fork.ι, CategoryTheory.ShortComplex.SnakeInput.h₀τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ { X₁ := S.L₀.X₁, X₂ := S.L₁.X₁, X₃ := S.L₂.X₁, f := S.v₀₁.τ₁, g := S.v₁₂.τ₁, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
exact_of_f_is_kernel _ S.h₀τ₁

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₀τ₁, CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ { X₁ := S.L₀.X₂, X₂ := S.L₁.X₂, X₃ := S.L₂.X₂, f := S.v₀₁.τ₂, g := S.v₁₂.τ₂, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
exact_of_f_is_kernel _ S.h₀τ₂

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₀τ₂, CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ { X₁ := S.L₀.X₃, X₂ := S.L₁.X₃, X₃ := S.L₂.X₃, f := S.v₀₁.τ₃, g := S.v₁₂.τ₃, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
exact_of_f_is_kernel _ S.h₀τ₃

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel, CategoryTheory.ShortComplex.SnakeInput.h₀τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Mono S.L₁.f
rw : Mono (S.v₀₁.τ₁ ≫ S.L₁.f)
⊢ Mono (S.L₀.f ≫ S.v₀₁.τ₂)

Tactic:
rw [← S.v₀₁.comm₁₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.SnakeInput.v₀₁
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Mono S.L₁.f
⊢ Mono (S.v₀₁.τ₁ ≫ S.L₁.f)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Mono S.L₁.f
⊢ Mono (S.L₀.f ≫ S.v₀₁.τ₂)

Tactic:
have : Mono (S.L₀.f ≫ S.v₀₁.τ₂) := by
    rw [← S.v₀₁.comm₁₂]
    apply mono_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Mono S.L₁.f
this : Mono (S.L₀.f ≫ S.v₀₁.τ₂)
⊢ Mono S.L₀.f

Tactic:
mono_of_mono _ S.v₀₁.τ₂

Premises used: CategoryTheory.ShortComplex.SnakeInput.v₀₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.mono_of_mono
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Mono S.L₁.f
this : Mono (S.L₀.f ≫ S.v₀₁.τ₂)
⊢ Mono S.L₀.f

Tactic:
exact mono_of_mono _ S.v₀₁.τ₂

Premises used: CategoryTheory.ShortComplex.SnakeInput.v₀₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.mono_of_mono
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Epi S.v₂₃.τ₁

Tactic:
epi_of_isColimit_cofork S.h₃τ₁

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₃τ₁, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Epi S.v₂₃.τ₂

Tactic:
epi_of_isColimit_cofork S.h₃τ₂

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₃τ₂, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ Epi S.v₂₃.τ₃

Tactic:
epi_of_isColimit_cofork S.h₃τ₃

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₃τ₃, CategoryTheory.Limits.Cofork.π, CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
exact_of_g_is_cokernel _ S.h₃τ₁

Premises used: CategoryTheory.ShortComplex.SnakeInput.h₃τ₁, CategoryTheory.ShortComplex.exact_of_g_is_cokernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ { X₁ := S.L₁.X₂, X₂ := S.L₂.X₂, X₃ := S.L₃.X₂, f := S.v₁₂.τ₂, g := S.v₂₃.τ₂, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
exact_of_g_is_cokernel _ S.h₃τ₂

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.ShortComplex.SnakeInput.h₃τ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
⊢ { X₁ := S.L₁.X₃, X₂ := S.L₂.X₃, X₃ := S.L₃.X₃, f := S.v₁₂.τ₃, g := S.v₂₃.τ₃, zero := ⋯ :
      ShortComplex.{v_1, u_1} C }.Exact

Tactic:
exact_of_g_is_cokernel _ S.h₃τ₃

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.ShortComplex.SnakeInput.h₃τ₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Epi S.L₂.g
rw : Epi (S.L₂.g ≫ S.v₂₃.τ₃)
⊢ Epi (S.v₂₃.τ₂ ≫ S.L₃.g)

Tactic:
rw [S.v₂₃.comm₂₃]

Premises used: CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.SnakeInput.v₂₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Epi S.L₂.g
⊢ Epi (S.L₂.g ≫ S.v₂₃.τ₃)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Epi S.L₂.g
⊢ Epi (S.v₂₃.τ₂ ≫ S.L₃.g)

Tactic:
have : Epi (S.v₂₃.τ₂ ≫ S.L₃.g) := by
    rw [S.v₂₃.comm₂₃]
    apply epi_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Epi S.L₂.g
this : Epi (S.v₂₃.τ₂ ≫ S.L₃.g)
⊢ Epi S.L₃.g

Tactic:
epi_of_epi S.v₂₃.τ₂ _

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.SnakeInput.v₂₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
inst_2 : Epi S.L₂.g
this : Epi (S.v₂₃.τ₂ ≫ S.L₃.g)
⊢ Epi S.L₃.g

Tactic:
exact epi_of_epi S.v₂₃.τ₂ _

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.SnakeInput.v₂₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
rw :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₀.X₂),
    x₂ ≫ S.L₀.g = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
⊢ S.L₀.Exact

Tactic:
rw [ShortComplex.exact_iff_exact_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements
-- Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : SnakeInput.{v_1, u_1} C
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
rw : x₂ ≫ S.v₀₁.τ₂ ≫ S.L₁.g = 0
rw₁ : x₂ ≫ S.L₀.g ≫ S.v₀₁.τ₃ = 0
rw₂ : Eq (α := A ⟶ S.L₁.X₃) (0 ≫ S.v₀₁.τ₃) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ S.L₁.X₃) 0 0
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0

Tactic:
rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.v₀₁, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.Limits.zero_comp