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.δ = 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:
have hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd _ _ := by
    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]
-- 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₂'
hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ (π₂ ≫ π₁) ≫ x₃ = k₂ ≫ S.L₁'.f

Tactic:
simp only [assoc, L₁'_f, ← hk₂', hp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₁'_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₂'
hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ ∃ (A' : C) (π : A' ⟶ A₀) (_ : Epi π) (x₁ : A' ⟶ S.L₁'.X₁), π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
exact ⟨A₂, π₂ ≫ π₁, epi_comp _ _, k₂, by simp only [assoc, L₁'_f, ← hk₂', hp]⟩
-- 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 :
  Eq (α := Opposite.unop S.op.P' ⟶ Opposite.unop S.op.P)
    (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
      S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op))
    (CategoryStruct.comp (Y := S.L₁.X₂)
      (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
        Opposite.unop
            (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃)
              S.L₁.g.op S.v₀₁.τ₃.op) ⟶
          Opposite.unop (Opposite.op S.L₁.X₂))
      (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op)))
⊢ S.op.δ.unop = S.δ.op.unop

Tactic:
rw [Quiver.Hom.unop_op, ← cancel_mono (pushout.inr _ _ : _ ⟶ S.P'),
    ← cancel_epi (pullback.snd _ _ : S.P ⟶ _), S.snd_δ_inr,
    ← cancel_mono S.P'IsoUnopOpP.hom, ← cancel_epi S.PIsoUnopOpP'.inv,
    P'IsoUnopOpP, PIsoUnopOpP', assoc, assoc, assoc, assoc,
    pushoutIsoUnopPullback_inr_hom, pullbackIsoUnopPushout_inv_snd_assoc,
    pushoutIsoUnopPullback_inl_hom, pullbackIsoUnopPushout_inv_fst_assoc]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom, CategoryTheory.Limits.pullback.snd, CategoryTheory.ShortComplex.SnakeInput.PIsoUnopOpP', CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, CategoryTheory.cancel_mono, CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc, CategoryTheory.ShortComplex.SnakeInput.P'IsoUnopOpP, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc, CategoryTheory.Iso.inv, CategoryTheory.Limits.pushout.inr
-- 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 :
  Eq (α :=
    Opposite.op (Opposite.unop S.op.P) ⟶
      Opposite.op
        (Opposite.unop
          (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃) S.L₁.g.op
            S.v₀₁.τ₃.op)))
    (Quiver.Hom.op
      (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
        S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op)))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y := S.L₁.X₂)
        (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
          Opposite.unop
              (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃)
                S.L₁.g.op S.v₀₁.τ₃.op) ⟶
            Opposite.unop (Opposite.op S.L₁.X₂))
        (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op))))
⊢ Eq (α := Opposite.unop S.op.P' ⟶ Opposite.unop S.op.P)
    (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
      S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op))
    (CategoryStruct.comp (Y := S.L₁.X₂)
      (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
        Opposite.unop
            (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃)
              S.L₁.g.op S.v₀₁.τ₃.op) ⟶
          Opposite.unop (Opposite.op S.L₁.X₂))
      (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op)))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj
-- 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 (α :=
    Opposite.op (Opposite.unop S.op.P) ⟶
      Opposite.op
        (Opposite.unop
          (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃) S.L₁.g.op
            S.v₀₁.τ₃.op)))
    (Quiver.Hom.op
      (Quiver.Hom.unop (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op) ≫
        S.op.δ.unop ≫ Quiver.Hom.unop (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op)))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y := S.L₁.X₂)
        (Quiver.Hom.unop (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op) :
          Opposite.unop
              (pushout.{v_1, u_1} (X := Opposite.op S.L₁.X₃) (Y := Opposite.op S.L₁.X₂) (Z := Opposite.op S.L₀.X₃)
                S.L₁.g.op S.v₀₁.τ₃.op) ⟶
            Opposite.unop (Opposite.op S.L₁.X₂))
        (S.v₁₂.τ₂ ≫ Quiver.Hom.unop (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op))))

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop, assoc] using S.op.snd_δ_inr

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Quiver.Hom.op_unop, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, CategoryTheory.ShortComplex.SnakeInput.op
-- 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
⊢ Iso.hom (Iso.refl S.L₂'.op.X₁) ≫ S.op.L₁'.f = S.L₂'.op.f ≫ Iso.hom (Iso.refl S.L₂'.op.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
dsimp : 𝟙 (Opposite.op S.L₃.X₁) ≫ S.op.δ = S.δ.op ≫ 𝟙 (Opposite.op S.L₀.X₃)
⊢ Iso.hom (Iso.refl S.L₂'.op.X₂) ≫ S.op.L₁'.g = S.L₂'.op.g ≫ Iso.hom (Iso.refl S.L₂'.op.X₃)

Tactic:
dsimp
-- 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
⊢ 𝟙 (Opposite.op S.L₃.X₁) ≫ S.op.δ = S.δ.op ≫ 𝟙 (Opposite.op S.L₀.X₃)

Tactic:
simp only [id_comp, comp_id, S.op_δ]

Premises used: CategoryTheory.ShortComplex.SnakeInput.op_δ, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_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.op.L₁'.Exact
⊢ S.L₂'.Exact

Tactic:
rw [← exact_op_iff, exact_iff_of_iso S.L₂'OpIso]

Premises used: CategoryTheory.ShortComplex.exact_op_iff, CategoryTheory.ShortComplex.exact_iff_of_iso, CategoryTheory.ShortComplex.SnakeInput.L₂'OpIso
-- 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.op.L₁'.Exact

Tactic:
S.op.L₁'_exact

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.ShortComplex.SnakeInput.op
-- 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.op.L₁'.Exact

Tactic:
exact S.op.L₁'_exact

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.ShortComplex.SnakeInput.op
-- 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.composableArrows.Exact

Tactic:
exact_of_δ₀ S.L₀_exact.exact_toComposableArrows
    (exact_of_δ₀ S.L₁'_exact.exact_toComposableArrows
    (exact_of_δ₀ S.L₂'_exact.exact_toComposableArrows
    S.L₃_exact.exact_toComposableArrows))

Premises used: CategoryTheory.ShortComplex.SnakeInput.L₃_exact, CategoryTheory.ShortComplex.SnakeInput.L₀_exact, CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.ShortComplex.SnakeInput.L₂'_exact, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ComposableArrows.exact_of_δ₀
-- 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₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
⊢ CategoryStruct.comp (Y := pullback S.L₁.g S.v₀₁.τ₃) (pullback.lift x₂ x₃ h₂) (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ) =
    pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁

Tactic:
have H := (pullback.lift x₂ x₃ h₂) ≫= S.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₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H :
  CategoryStruct.comp (Y := pullback S.L₁.g S.v₀₁.τ₃) (pullback.lift x₂ x₃ h₂) (pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ) =
    pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁

Tactic:
rw [pullback.lift_snd_assoc] at H

Premises used: CategoryTheory.Limits.pullback.lift_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
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
rw : (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁
⊢ x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁

Tactic:
rw [H, ← assoc]

Premises used: CategoryTheory.Category.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
A : C
x₃ : A ⟶ S.L₀.X₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
e_a : pullback.lift x₂ x₃ h₂ ≫ S.φ₁ = x₁
⊢ (pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁

Tactic:
congr 1
-- 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₃
x₂ : A ⟶ S.L₁.X₂
x₁ : A ⟶ S.L₂.X₁
h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃
h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂
H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁
⊢ pullback.lift x₂ x₃ h₂ ≫ S.φ₁ = x₁

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, lift_φ₂, h₁]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₂, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, CategoryTheory.ShortComplex.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
h₀ : IsZero.{v_1, u_1} S.L₀.X₂
⊢ Mono S.δ

Tactic:
(S.L₁'.exact_iff_mono (IsZero.eq_zero_of_src h₀ S.L₁'.f)).1 S.L₁'_exact

Premises used: CategoryTheory.ShortComplex.Exact.desc, CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.ShortComplex.exact_iff_mono, CategoryTheory.ShortComplex.SnakeInput.L₁', Iff.mp, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.IsZero.eq_zero_of_src, 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
h₃ : IsZero.{v_1, u_1} S.L₃.X₂
⊢ Epi S.δ

Tactic:
(S.L₂'.exact_iff_epi (IsZero.eq_zero_of_tgt h₃ S.L₂'.g)).1 S.L₂'_exact

Premises used: CategoryTheory.ShortComplex.Exact.desc, CategoryTheory.ShortComplex.SnakeInput.L₂', CategoryTheory.Limits.IsZero.eq_zero_of_tgt, CategoryTheory.ShortComplex.SnakeInput.L₂'_exact, Iff.mp, CategoryTheory.ShortComplex.exact_iff_epi, 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
h₀ : IsZero.{v_1, u_1} S.L₀.X₂
h₃ : IsZero.{v_1, u_1} S.L₃.X₂
⊢ IsIso S.δ

Tactic:
@Balanced.isIso_of_mono_of_epi _ _ _ _ _ S.δ (S.mono_δ h₀) (S.epi_δ h₃)

Premises used: CategoryTheory.Balanced.isIso_of_mono_of_epi, 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 S₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁.Hom S₂
g : S₂.Hom S₃
⊢ (f.f₀ ≫ g.f₀) ≫ S₃.v₀₁ = S₁.v₀₁ ≫ f.f₁ ≫ g.f₁

Tactic:
simp only [assoc, comm₀₁, comm₀₁_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁_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 S₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁.Hom S₂
g : S₂.Hom S₃
⊢ (f.f₁ ≫ g.f₁) ≫ S₃.v₁₂ = S₁.v₁₂ ≫ f.f₂ ≫ g.f₂

Tactic:
simp only [assoc, comm₁₂, comm₁₂_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂_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 S₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁.Hom S₂
g : S₂.Hom S₃
⊢ (f.f₂ ≫ g.f₂) ≫ S₃.v₂₃ = S₁.v₂₃ ≫ f.f₃ ≫ g.f₃

Tactic:
simp only [assoc, comm₂₃, comm₂₃_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃_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
⊢ Hom.f₀ (𝟙 S) = 𝟙 S.L₀

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Hom.f₁ (𝟙 S) = 𝟙 S.L₁

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Hom.f₂ (𝟙 S) = 𝟙 S.L₂

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Hom.f₃ (𝟙 S) = 𝟙 S.L₃

Tactic:
rfl

Premises used: rfl
-- 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₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
g : S₂ ⟶ S₃
⊢ (f ≫ g).f₀ = f.f₀ ≫ g.f₀

Tactic:
rfl

Premises used: rfl
-- 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₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
g : S₂ ⟶ S₃
⊢ (f ≫ g).f₁ = f.f₁ ≫ g.f₁

Tactic:
rfl

Premises used: rfl
-- 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₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
g : S₂ ⟶ S₃
⊢ (f ≫ g).f₂ = f.f₂ ≫ g.f₂

Tactic:
rfl

Premises used: rfl
-- 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₁ S₂ S₃ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
g : S₂ ⟶ S₃
⊢ (f ≫ g).f₃ = f.f₃ ≫ g.f₃

Tactic:
rfl

Premises used: rfl
-- 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 S₁ S₂ S₃ x : SnakeInput.{v_1, u_1} C
dsimp :
  pullback.map x.L₁.g x.v₀₁.τ₃ x.L₁.g x.v₀₁.τ₃ (𝟙 x.L₁.X₂) (𝟙 x.L₀.X₃) (𝟙 x.L₁.X₃) ⋯ ⋯ = 𝟙 (pullback x.L₁.g x.v₀₁.τ₃)
⊢ pullback.map x.L₁.g x.v₀₁.τ₃ x.L₁.g x.v₀₁.τ₃ (Hom.f₁ (𝟙 x)).τ₂ (Hom.f₀ (𝟙 x)).τ₃ (Hom.f₁ (𝟙 x)).τ₃ ⋯ ⋯ = 𝟙 x.P

Tactic:
dsimp [P]

Premises used: CategoryTheory.ShortComplex.SnakeInput.P
-- 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 S₁ S₂ S₃ x : SnakeInput.{v_1, u_1} C
⊢ pullback.map x.L₁.g x.v₀₁.τ₃ x.L₁.g x.v₀₁.τ₃ (𝟙 x.L₁.X₂) (𝟙 x.L₀.X₃) (𝟙 x.L₁.X₃) ⋯ ⋯ = 𝟙 (pullback x.L₁.g x.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 S₁ S₂ S₃ X Y Z : SnakeInput.{v_1, u_1} C
x : X ⟶ Y
x_1 : Y ⟶ Z
dsimp :
  Eq (α := pullback X.L₁.g X.v₀₁.τ₃ ⟶ pullback Z.L₁.g Z.v₀₁.τ₃)
    (pullback.map X.L₁.g X.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ (x.f₁.τ₂ ≫ x_1.f₁.τ₂) (x.f₀.τ₃ ≫ x_1.f₀.τ₃) (x.f₁.τ₃ ≫ x_1.f₁.τ₃) ⋯ ⋯)
    (CategoryStruct.comp (Y := pullback Y.L₁.g Y.v₀₁.τ₃)
      (pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ x.f₁.τ₂ x.f₀.τ₃ x.f₁.τ₃ ⋯ ⋯)
      (pullback.map Y.L₁.g Y.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ x_1.f₁.τ₂ x_1.f₀.τ₃ x_1.f₁.τ₃ ⋯ ⋯))
⊢ Eq (α := X.P ⟶ Z.P) (pullback.map X.L₁.g X.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ (x ≫ x_1).f₁.τ₂ (x ≫ x_1).f₀.τ₃ (x ≫ x_1).f₁.τ₃ ⋯ ⋯)
    (CategoryStruct.comp (Y := Y.P) (pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ x.f₁.τ₂ x.f₀.τ₃ x.f₁.τ₃ ⋯ ⋯)
      (pullback.map Y.L₁.g Y.v₀₁.τ₃ Z.L₁.g Z.v₀₁.τ₃ x_1.f₁.τ₂ x_1.f₀.τ₃ x_1.f₁.τ₃ ⋯ ⋯))

Tactic:
dsimp [P]

Premises used: CategoryTheory.ShortComplex.SnakeInput.P
-- 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₁ S₂ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
dsimp :
  Eq (α := S₁.P ⟶ S₂.L₂.X₂) ((pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂)
    (CategoryStruct.comp (Y := S₂.P) (pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯)
      (pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂))
⊢ S₁.φ₂ ≫ f.f₂.τ₂ = Functor.map functorP f ≫ S₂.φ₂

Tactic:
dsimp [φ₂]

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₁ S₂ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
⊢ Eq (α := S₁.P ⟶ S₂.L₂.X₂) ((pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂)
    (CategoryStruct.comp (Y := S₂.P) (pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯)
      (pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂))

Tactic:
simp only [assoc, pullback.lift_fst_assoc, ← comp_τ₂, f.comm₁₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.ShortComplex.comp_τ₂, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂
-- 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₁ S₂ : SnakeInput.{v_1, u_1} C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ f.f₂.τ₁ = Functor.map functorP f ≫ S₂.φ₁

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.SnakeInput.L₂, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, CategoryTheory.ShortComplex.SnakeInput.Hom.f₂, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂, CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
dsimp : (if i = j then X else 0) = X
⊢ HomologicalComplex.X.{v, u, u_1}
      { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v, u, u_1} V c }
      i =
    X

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
rw rw₁ : X = X
⊢ (if i = j then X else 0) = X

Tactic:
rw [if_pos h]

Premises used: if_pos
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
dsimp : Y = if i = j then Y else 0
⊢ Y =
    HomologicalComplex.X.{v, u, u_1}
      { X := fun (i : ι) ↦ if i = j then Y else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ } i

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Single
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
rw rw₁ : Y = Y
⊢ Y = if i = j then Y else 0

Tactic:
rw [if_pos h]

Premises used: if_pos