awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Epi S₂.g
have suffices : Epi (e.hom.τ₂ ≫ S₂.g)
Tactic: suffices Epi (e.hom.τ₂ ≫ S₂.g) by
      exact epi_of_epi e.hom.τ₂ _
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.ShortExact
⊢ Epi (e.hom.τ₂ ≫ S₂.g)
have this : Epi S₁.g
Tactic: have := h.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Epi S₁.g
⊢ Epi (e.hom.τ₂ ≫ S₂.g)
have rw : Epi (S₁.g ≫ e.hom.τ₃)
Tactic: rw [e.hom.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
⊢ S₁.ShortExact ↔ S₂.ShortExact
have mp : S₁.ShortExact → S₂.ShortExact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
e : S₁ ≅ S₂
mp : S₁.ShortExact → S₂.ShortExact
⊢ S₁.ShortExact ↔ S₂.ShortExact
have mpr : S₂.ShortExact → S₁.ShortExact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.ShortExact
⊢ Mono S.op.f
have this : Epi S.g
Tactic: have := h.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.ShortExact
⊢ Epi S.op.g
have this : Mono S.f
Tactic: have := h.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : S.ShortExact
⊢ Mono S.unop.f
have this : Epi S.g
Tactic: have := h.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : S.ShortExact
this : Epi S.g
⊢ Mono S.unop.f
have dsimp : Mono S.g.unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : S.ShortExact
⊢ Epi S.unop.g
have this : Mono S.f
Tactic: have := h.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : S.ShortExact
this : Mono S.f
⊢ Epi S.unop.g
have dsimp : Epi S.f.unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
⊢ ShortExact (S.map F)
have this : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.ShortExact
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits F
inst_6 : PreservesFiniteColimits F
this : Mono S.f
⊢ ShortExact (S.map F)
have this₁ : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsIso S.f ↔ IsZero.{v_1, u_1} S.X₃
have this : HasZeroObject.{v_1, u_1} C
Tactic: have := hS.exact.hasZeroObject
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 : HasZeroObject.{v_1, u_1} C
⊢ IsIso S.f ↔ IsZero.{v_1, u_1} S.X₃
have this₁ : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 : Mono S.f
⊢ IsIso S.f ↔ IsZero.{v_1, u_1} S.X₃
have this₁ : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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
⊢ IsIso S.f ↔ IsZero.{v_1, u_1} S.X₃
have mp : IsIso S.f → IsZero.{v_1, u_1} S.X₃
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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₃
⊢ IsIso S.f ↔ IsZero.{v_1, u_1} S.X₃
have mpr : IsZero.{v_1, u_1} S.X₃ → IsIso S.f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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₃
⊢ IsIso S.f
have this₁ : Epi S.f
Tactic: have : Epi S.f := (S.exact_iff_epi (hX₃.eq_of_tgt _ _)).1 hS.exact
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsIso S.g ↔ IsZero.{v_1, u_1} S.X₁
have this : HasZeroObject.{v_1, u_1} C
Tactic: have := hS.exact.hasZeroObject
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 : HasZeroObject.{v_1, u_1} C
⊢ IsIso S.g ↔ IsZero.{v_1, u_1} S.X₁
have this₁ : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 : Mono S.f
⊢ IsIso S.g ↔ IsZero.{v_1, u_1} S.X₁
have this₁ : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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
⊢ IsIso S.g ↔ IsZero.{v_1, u_1} S.X₁
have mp : IsIso S.g → IsZero.{v_1, u_1} S.X₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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₁
⊢ IsIso S.g ↔ IsZero.{v_1, u_1} S.X₁
have mpr : IsZero.{v_1, u_1} S.X₁ → IsIso S.g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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₁
⊢ IsIso S.g
have this₁ : Mono S.g
Tactic: have : Mono S.g := (S.exact_iff_mono (hX₁.eq_of_src _ _)).1 hS.exact
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 φ.τ₃
⊢ IsIso φ.τ₂
have this : Mono S₁.f
Tactic: have := h₁.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsIso φ.τ₂
have this₁ : Mono S₂.f
Tactic: have := h₂.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsIso φ.τ₂
have this₁ : Epi S₁.g
Tactic: have := h₁.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsIso φ.τ₂
have this₁ : Epi S₂.g
Tactic: have := h₂.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsIso φ.τ₂
have this₁ : Mono φ.τ₂
Tactic: have := mono_τ₂_of_exact_of_mono φ h₁.exact
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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 φ.τ₂
⊢ IsIso φ.τ₂
have this₁ : Epi φ.τ₂
Tactic: have := epi_τ₂_of_exact_of_epi φ h₂.exact
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsLimit (KernelFork.ofι S.f ⋯)
have this : Mono S.f
Tactic: have := hS.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)
have this : Epi S.g
Tactic: have := hS.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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
⊢ { 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
have this : Epi h.left.f'
Tactic: have := hS.epi_f' h.left
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (hypothesis)
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'
⊢ { 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
have this₁ : Mono h.right.g'
Tactic: have := hS.mono_g' h.right
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.ShortExact (goal)
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₂₃ := ⋯ }
⊢ { 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
have rwa : S'.Exact
Tactic: rwa [ShortComplex.exact_iff_of_epi_of_isIso_of_mono b,
      ← ShortComplex.exact_iff_of_epi_of_isIso_of_mono a]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0
have rw : (S.v₀₁ ≫ S.v₁₂).τ₁ = 0
Tactic: rw [← comp_τ₁, S.w₀₂, zero_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.L₀.X₁ ⟶ S.L₂.X₁) (Hom.τ₁ 0) 0
Tactic: rw [← comp_τ₁, S.w₀₂, zero_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0
have rw₂ : Eq.{v_1 + 1} (α := S.L₀.X₁ ⟶ S.L₂.X₁) 0 0
Tactic: rw [← comp_τ₁, S.w₀₂, zero_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0
have rw : (S.v₀₁ ≫ S.v₁₂).τ₂ = 0
Tactic: rw [← comp_τ₂, S.w₀₂, zero_τ₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.L₀.X₂ ⟶ S.L₂.X₂) (Hom.τ₂ 0) 0
Tactic: rw [← comp_τ₂, S.w₀₂, zero_τ₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := S.L₀.X₂ ⟶ S.L₂.X₂) 0 0
Tactic: rw [← comp_τ₂, S.w₀₂, zero_τ₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0
have rw : (S.v₀₁ ≫ S.v₁₂).τ₃ = 0
Tactic: rw [← comp_τ₃, S.w₀₂, zero_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.L₀.X₃ ⟶ S.L₂.X₃) (Hom.τ₃ 0) 0
Tactic: rw [← comp_τ₃, S.w₀₂, zero_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0
have rw₂ : Eq.{v_1 + 1} (α := S.L₀.X₃ ⟶ S.L₂.X₃) 0 0
Tactic: rw [← comp_τ₃, S.w₀₂, zero_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0
have rw : (S.v₁₂ ≫ S.v₂₃).τ₁ = 0
Tactic: rw [← comp_τ₁, S.w₁₃, zero_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.L₁.X₁ ⟶ S.L₃.X₁) (Hom.τ₁ 0) 0
Tactic: rw [← comp_τ₁, S.w₁₃, zero_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0
have rw₂ : Eq.{v_1 + 1} (α := S.L₁.X₁ ⟶ S.L₃.X₁) 0 0
Tactic: rw [← comp_τ₁, S.w₁₃, zero_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0
have rw : (S.v₁₂ ≫ S.v₂₃).τ₂ = 0
Tactic: rw [← comp_τ₂, S.w₁₃, zero_τ₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.L₁.X₂ ⟶ S.L₃.X₂) (Hom.τ₂ 0) 0
Tactic: rw [← comp_τ₂, S.w₁₃, zero_τ₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := S.L₁.X₂ ⟶ S.L₃.X₂) 0 0
Tactic: rw [← comp_τ₂, S.w₁₃, zero_τ₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0
have rw : (S.v₁₂ ≫ S.v₂₃).τ₃ = 0
Tactic: rw [← comp_τ₃, S.w₁₃, zero_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0
have rw₁ : Eq.{v_1 + 1} (α := S.L₁.X₃ ⟶ S.L₃.X₃) (Hom.τ₃ 0) 0
Tactic: rw [← comp_τ₃, S.w₁₃, zero_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0
have rw₂ : Eq.{v_1 + 1} (α := S.L₁.X₃ ⟶ S.L₃.X₃) 0 0
Tactic: rw [← comp_τ₃, S.w₁₃, zero_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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₀₁.τ₂)
have rw : Mono (S.v₀₁.τ₁ ≫ S.L₁.f)
Tactic: rw [← S.v₀₁.comm₁₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
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
have this : Mono (S.L₀.f ≫ S.v₀₁.τ₂)
Tactic: have : Mono (S.L₀.f ≫ S.v₀₁.τ₂) := by
    rw [← S.v₀₁.comm₁₂]
    apply mono_comp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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)
have rw : Epi (S.L₂.g ≫ S.v₂₃.τ₃)
Tactic: rw [S.v₂₃.comm₂₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (hypothesis)
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
have this : Epi (S.v₂₃.τ₂ ≫ S.L₃.g)
Tactic: have : Epi (S.v₂₃.τ₂ ≫ S.L₃.g) := by
    rw [S.v₂₃.comm₂₃]
    apply epi_comp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ S.L₀.Exact
have 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
Tactic: rw [ShortComplex.exact_iff_exact_up_to_refinements]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0
have rw : x₂ ≫ S.v₀₁.τ₂ ≫ S.L₁.g = 0
Tactic: rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0
have rw₁ : x₂ ≫ S.L₀.g ≫ S.v₀₁.τ₃ = 0
Tactic: rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0
have rw₂ : Eq (α := A ⟶ S.L₁.X₃) (0 ≫ S.v₀₁.τ₃) 0
Tactic: rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.SnakeLemma (goal)
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
⊢ (x₂ ≫ S.v₀₁.τ₂) ≫ S.L₁.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.L₁.X₃) 0 0
Tactic: rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp]