awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (y₁ : A₁ ⟶ S.L₁.X₁) (hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
obtain ⟨A₁, π₁, hπ₁, y₁, hy₁⟩ := S.L₁_exact.exact_up_to_refinements (x₂ ≫ S.v₀₁.τ₂)
    (by rw [assoc, S.v₀₁.comm₂₃, reassoc_of% hx₂, zero_comp])

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₁_exact, CategoryTheory.ShortComplex.π₁, CategoryTheory.ShortComplex.SnakeInput.v₀₁, CategoryTheory.ShortComplex.Hom.τ₂, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.CategoryStruct.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
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
⊢ y₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, zero_comp, S.v₁₂.comm₁₂,
      ← reassoc_of% hy₁, w₀₂_τ₂, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₂, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp, 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
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
⊢ y₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
have hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0 := by
    simp only [← cancel_mono S.L₂.f, assoc, zero_comp, S.v₁₂.comm₁₂,
      ← reassoc_of% hy₁, w₀₂_τ₂, comp_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
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
⊢ ∃ (x₁ : A₁ ⟶ S.L₀.X₁), x₁ ≫ S.v₀₁.τ₁ = y₁

Tactic:
⟨_, S.exact_C₁_up.lift_f y₁ hy₁'⟩

Premises used: CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up, Exists.intro, CategoryTheory.ShortComplex.Exact.lift_f
-- 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
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
obtain :
  ∀ (x₁ : A₁ ⟶ S.L₀.X₁) (hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S.v₀₁.τ₁ = y₁ := ⟨_, S.exact_C₁_up.lift_f y₁ hy₁'⟩

Premises used: 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
A : C
x₂ : A ⟶ S.L₀.X₂
hx₂ : x₂ ≫ S.L₀.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
x₁ : A₁ ⟶ S.L₀.X₁
hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
⟨A₁, π₁, hπ₁, x₁, ?_⟩

Premises used: Exists.intro
-- 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
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
x₁ : A₁ ⟶ S.L₀.X₁
hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁
refine : π₁ ≫ x₂ = x₁ ≫ S.L₀.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀.X₁), π ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
refine ⟨A₁, π₁, hπ₁, x₁, ?_⟩
-- 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
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₁ : A₁ ⟶ S.L₁.X₁
hy₁ : π₁ ≫ x₂ ≫ S.v₀₁.τ₂ = y₁ ≫ S.L₁.f
hy₁' : y₁ ≫ S.v₁₂.τ₁ = 0
x₁ : A₁ ⟶ S.L₀.X₁
hx₁ : x₁ ≫ S.v₀₁.τ₁ = y₁
⊢ π₁ ≫ x₂ = x₁ ≫ S.L₀.f

Tactic:
simp only [← cancel_mono S.v₀₁.τ₂, assoc, ← S.v₀₁.comm₁₂, reassoc_of% hx₁, hy₁]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.SnakeInput.v₀₁, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Hom.τ₂
-- 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
⊢ S.L₃.Exact

Tactic:
S.op.L₀_exact.unop

Premises used: Quiver.Hom.unop, CategoryTheory.ShortComplex.SnakeInput.L₀_exact, CategoryTheory.ShortComplex.Exact.unop, CategoryTheory.ShortComplex.SnakeInput.op, CategoryTheory.ShortComplex.unop
-- 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
a : A ⟶ S.L₁.X₂
b : A ⟶ S.L₀.X₃
h : a ≫ S.L₁.g = b ≫ S.v₀₁.τ₃
⊢ pullback.lift a b h ≫ S.φ₂ = a ≫ S.v₁₂.τ₂

Tactic:
simp [φ₂]

Premises used: CategoryTheory.ShortComplex.SnakeInput.φ₂
-- 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
⊢ S.φ₂ ≫ S.L₂.g = 0

Tactic:
simp only [φ₂, assoc, S.v₁₂.comm₂₃, pullback.condition_assoc, w₀₂_τ₃, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.SnakeInput.φ₂, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.SnakeInput.v₁₂, 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
⊢ S.φ₁ ≫ S.L₂.f = S.φ₂

Tactic:
S.L₂_exact.lift_f _ _

Premises used: CategoryTheory.ShortComplex.SnakeInput.φ₁, CategoryTheory.ShortComplex.SnakeInput.L₂_exact, CategoryTheory.ShortComplex.Exact.lift_f
-- 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
⊢ S.L₁.f ≫ S.L₁.g = 0 ≫ S.v₀₁.τ₃

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
⊢ CategoryStruct.comp (Y := S.P) (pullback.lift S.L₁.f 0 ⋯) (pullback.snd S.L₁.g S.v₀₁.τ₃) = 0

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
dsimp : pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁
⊢ S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
dsimp only [L₀']

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₀'
-- 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
⊢ pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, φ₂, pullback.lift_fst_assoc,
    S.v₁₂.comm₁₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₂, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.ShortComplex.SnakeInput.φ₂, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, CategoryTheory.ShortComplex.f, 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
dsimp : Epi (X := S.P) (pullback.snd S.L₁.g S.v₀₁.τ₃)
⊢ Epi S.L₀'.g

Tactic:
dsimp only [L₀']

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₀'
-- 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 (X := S.P) (pullback.snd S.L₁.g S.v₀₁.τ₃)

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
inst_2 : Mono S.L₁.f
⊢ S.L₀'.f ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = S.L₁.f

Tactic:
simp [L₀']

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₀'
-- 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.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
rw : x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.L₁.g = 0
rw₁ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ 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₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃) ≫ S.L₁.g = 0

Tactic:
rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.pullback.condition
-- 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.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
obtain :
  ∀ (A' : C) (π : A' ⟶ A) (hπ : Epi π) (x₁ : A' ⟶ S.L₁.X₁) (fac : π ≫ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = x₁ ≫ S.L₁.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀'.X₁), π ≫ x₂ = x₁ ≫ S.L₀'.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀'.X₁), π ≫ x₂ = x₁ ≫ S.L₀'.f

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := S.L₁_exact.exact_up_to_refinements (x₂ ≫ pullback.fst _ _)
    (by rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp])

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₁_exact, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.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
A : C
x₂ : A ⟶ S.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.L₁.X₁
fac : π ≫ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = x₁ ≫ S.L₁.f
⊢ (π ≫ x₂) ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = (x₁ ≫ S.L₀'.f) ≫ pullback.fst S.L₁.g S.v₀₁.τ₃

Tactic:
simpa [L₀'] using fac

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₀'
-- 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.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.L₁.X₁
fac : π ≫ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = x₁ ≫ S.L₁.f
⊢ (π ≫ x₂) ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = (x₁ ≫ S.L₀'.f) ≫ pullback.snd S.L₁.g S.v₀₁.τ₃

Tactic:
simp [L₀', hx₂]

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₀'
-- 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.P
hx₂ : x₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = 0
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ S.L₁.X₁
fac : π ≫ x₂ ≫ pullback.fst S.L₁.g S.v₀₁.τ₃ = x₁ ≫ S.L₁.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.L₀'.X₁), π ≫ x₂ = x₁ ≫ S.L₀'.f

Tactic:
exact ⟨A', π, hπ, x₁, pullback.hom_ext (by simpa [L₀'] using fac) (by simp [L₀', hx₂])⟩
-- 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
⊢ S.L₀'.f ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0

Tactic:
simp only [L₁_f_φ₁_assoc, w₁₃_τ₁]

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc, 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
⊢ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = S.φ₁ ≫ S.v₂₃.τ₁

Tactic:
S.L₀'_exact.g_desc _ _

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₀'_exact, CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.ShortComplex.SnakeInput.P, CategoryTheory.ShortComplex.Exact.g_desc, CategoryTheory.ShortComplex.SnakeInput.δ
-- 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
⊢ Eq (α := pullback S.L₁.g S.v₀₁.τ₃ ⟶ pushout S.L₂.f S.v₂₃.τ₁)
    (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ ≫ pushout.inr S.L₂.f S.v₂₃.τ₁)
    (pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁)

Tactic:
simp only [snd_δ_assoc, ← pushout.condition, φ₂, φ₁_L₂_f_assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.condition, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc, CategoryTheory.ShortComplex.SnakeInput.φ₂, CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc
-- 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
⊢ S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ = S.L₀.g

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
⊢ S.L₀X₂ToP ≫ S.φ₁ = 0

Tactic:
simp only [← cancel_mono S.L₂.f, L₀X₂ToP, assoc, φ₂, φ₁_L₂_f,
    pullback.lift_fst_assoc, w₀₂_τ₂, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₂, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.ShortComplex.SnakeInput.φ₂, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_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.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃) ≫ S.δ = 0
rw₁ : S.L₀X₂ToP ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
rw₂ : S.L₀X₂ToP ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
rw₃ : Eq (α := S.L₀.X₂ ⟶ S.L₃.X₁) (0 ≫ S.v₂₃.τ₁) 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := S.L₀.X₂ ⟶ S.L₃.X₁) 0 0
⊢ S.L₀.g ≫ S.δ = 0

Tactic:
rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd, CategoryTheory.ShortComplex.SnakeInput.snd_δ, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁_assoc, CategoryTheory.Limits.zero_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
⊢ S.δ ≫ S.L₃.f = 0

Tactic:
simp [← cancel_epi S.L₀'.g, δ, S.v₂₃.comm₁₂, φ₂]

Premises used: CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.SnakeInput.φ₂, CategoryTheory.ShortComplex.SnakeInput.L₀', CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.SnakeInput.v₂₃, CategoryTheory.ShortComplex.g, CategoryTheory.ShortComplex.SnakeInput.δ
-- 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.δ = 0
obtain :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A₀) (hπ₁ : Epi π₁) (p : A₁ ⟶ S.L₀'.X₂) (hp : π₁ ≫ x₃ = p ≫ S.L₀'.g),
    ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
obtain ⟨A₁, π₁, hπ₁, p, hp⟩ := surjective_up_to_refinements_of_epi S.L₀'.g x₃

Premises used: CategoryTheory.ShortComplex.π₁, CategoryTheory.surjective_up_to_refinements_of_epi, CategoryTheory.ShortComplex.SnakeInput.L₀', CategoryTheory.ShortComplex.g
-- 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.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
rw : p ≫ S.φ₁ ≫ S.v₂₃.τ₁ = 0
rw₁ : p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = 0
rw₂ : π₁ ≫ x₃ ≫ S.δ = 0
rw₃ : Eq (α := A₁ ⟶ S.L₃.X₁) (π₁ ≫ 0) 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := A₁ ⟶ S.L₃.X₁) 0 0
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0

Tactic:
rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.SnakeInput.snd_δ
-- 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.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0

Tactic:
have hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0 := by
    rw [assoc, ← S.snd_δ, ← reassoc_of% hp, hx₃, comp_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
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
obtain :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂)
    (x₁ :
      A₂ ⟶
        { 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 }.X₁)
    (hx₁ :
      π₂ ≫ p ≫ S.φ₁ = x₁ ≫ { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := ⋯ }.f),
    ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
obtain ⟨A₂, π₂, hπ₂, x₁, hx₁⟩ := S.exact_C₁_down.exact_up_to_refinements (p ≫ S.φ₁) hp'

Premises used: CategoryTheory.ShortComplex.SnakeInput.φ₁, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.π₂, CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down
-- 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.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
⊢ (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0

Tactic:
simp only [x₂, x₂', sub_comp, assoc, ← S.v₁₂.comm₁₂, ← reassoc_of% hx₁, φ₂, φ₁_L₂_f, sub_self]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, sub_self, CategoryTheory.ShortComplex.SnakeInput.φ₂, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, CategoryTheory.ShortComplex.SnakeInput.v₁₂, CategoryTheory.Preadditive.sub_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
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
⊢ (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0

Tactic:
have hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0 := by
    simp only [x₂, x₂', sub_comp, assoc, ← S.v₁₂.comm₁₂, ← reassoc_of% hx₁, φ₂, φ₁_L₂_f, sub_self]
-- 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.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0
k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'
⊢ k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'

Tactic:
have hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂' := S.exact_C₂_up.lift_f _ _
-- 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.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0
k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'
hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'
⊢ k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃

Tactic:
simp only [x₂, x₂', ← cancel_mono S.v₀₁.τ₃, assoc, ← S.v₀₁.comm₂₃, reassoc_of% hk₂,
      sub_comp, S.L₁.zero, comp_zero, sub_zero, pullback.condition]

Premises used: CategoryTheory.Category.assoc, sub_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.SnakeInput.v₀₁, CategoryTheory.ShortComplex.SnakeInput.L₁, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.zero, CategoryTheory.Limits.pullback.condition, CategoryTheory.Preadditive.sub_comp, CategoryTheory.ShortComplex.Hom.τ₃