awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
⊢ (π₂ ≫ z) ≫ φ.τ₂ = y ≫ S₂.f

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
refine_2 :
  ∀ (A₃ : C) (π₃ : A₃ ⟶ A₂) (hπ₃ : Epi π₃) (x₁ : A₃ ⟶ S₁.X₁) (hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f),
    Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0

Tactic:
obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ :=
      h (π₂ ≫ z) (by rw [assoc, hz, comp_zero]) y (by simpa)

Premises used: CategoryTheory.ShortComplex.π₃, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
refine_2 : ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ z = x₁ ≫ S₁.f
⊢ Eq (α := A₁ ⟶ S₁.homology) (S₁.liftCycles z hz ≫ S₁.homologyπ) 0

Tactic:
rw [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ (π₃ ≫ π₂) ≫ z = x₁ ≫ S₁.f

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 →
      ∀ (y₁ : A ⟶ S₂.X₁),
        x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ x₂ = x₁ ≫ S₁.f
A : C
γ : A ⟶ S₁.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
z : A₁ ⟶ S₁.X₂
hz : z ≫ S₁.g = 0
fac : π₁ ≫ γ = S₁.liftCycles z hz ≫ S₁.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
y : A₂ ⟶ S₂.X₁
hy : π₂ ≫ z ≫ φ.τ₂ = y ≫ S₂.f
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₁.X₁
hx₁ : π₃ ≫ π₂ ≫ z = x₁ ≫ S₁.f
⊢ ∃ (A' : C) (π : A' ⟶ A₁) (_ : Epi π) (x₁ : A' ⟶ S₁.X₁), π ≫ z = x₁ ≫ S₁.f

Tactic:
exact ⟨A₃, π₃ ≫ π₂, epi_comp _ _, x₁, by simpa⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
rw :
  (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ Epi (X := S₁.homology) (Y := S₂.homology) (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
rw [epi_iff_surjective_up_to_refinements]

Premises used: CategoryTheory.epi_iff_surjective_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
mp :
  (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) →
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
mpr :
  (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology),
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
          π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
mp :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (γ : A₁ ⟶ S₁.homology)
    (hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (γ ≫ homologyMap φ)),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
      π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
obtain ⟨A₁, π₁, hπ₁, γ, hγ⟩ := h (S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ)

Premises used: CategoryTheory.ShortComplex.homologyπ, CategoryTheory.ShortComplex.π₁, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.liftCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (γ ≫ homologyMap φ)
mp :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂) (x₂ : A₂ ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0)
    (fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
      π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ

Premises used: CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements, CategoryTheory.ShortComplex.π₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
hγ : Eq (α := A₁ ⟶ S₂.homology) (π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (γ ≫ homologyMap φ)
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
⊢ Eq (α := A₂ ⟶ S₂.homology) (π₂ ≫ π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (π₂ ≫ γ ≫ homologyMap φ)

Tactic:
replace hγ := π₂ ≫= hγ
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
hγ : Eq (α := A₂ ⟶ S₂.homology) (π₂ ≫ π₁ ≫ S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ) (π₂ ≫ γ ≫ homologyMap φ)
⊢ ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ π₁ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f

Tactic:
simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements] at hγ

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements, CategoryTheory.ShortComplex.comp_liftCycles_assoc, CategoryTheory.ShortComplex.homologyπ_naturality
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
hγ : ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ π₁ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
mp :
  ∀ (A₃ : C) (π₃ : A₃ ⟶ A₂) (hπ₃ : Epi π₃) (x₁ : A₃ ⟶ S₂.X₁) (hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
      π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ := hγ

Premises used: CategoryTheory.ShortComplex.π₃
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₂.X₁
hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ (π₃ ≫ x₂) ≫ S₁.g = 0

Tactic:
simp only [assoc, hx₂, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₂.X₁
hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ (π₃ ≫ π₂ ≫ π₁) ≫ y₂ = (π₃ ≫ x₂) ≫ φ.τ₂ + x₁ ≫ S₂.f

Tactic:
simpa only [assoc] using hx₁

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₂.X₁
hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
    π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
exact ⟨A₃, π₃ ≫ π₂ ≫ π₁, inferInstance, π₃ ≫ x₂, by simp only [assoc, hx₂, comp_zero],
      x₁, by simpa only [assoc] using hx₁⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
mpr :
  ∀ (A₁ : C) (π₁ : A₁ ⟶ A) (hπ₁ : Epi π₁) (y₂ : A₁ ⟶ S₂.X₂) (hy₂ : y₂ ≫ S₂.g = 0)
    (fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ

Tactic:
obtain ⟨A₁, π₁, hπ₁, y₂, hy₂, fac⟩ := S₂.eq_liftCycles_homologyπ_up_to_refinements γ

Premises used: CategoryTheory.ShortComplex.π₁, CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
mpr :
  ∀ (A₂ : C) (π₂ : A₂ ⟶ A₁) (hπ₂ : Epi π₂) (x₂ : A₂ ⟶ S₁.X₂) (hx₂ : x₂ ≫ S₁.g = 0) (y₁ : A₂ ⟶ S₂.X₁)
    (hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f),
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ

Tactic:
obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, y₁, hy₁⟩ := h y₂ hy₂

Premises used: CategoryTheory.ShortComplex.π₂
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ

Tactic:
⟨A₂, π₂ ≫ π₁, inferInstance, S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ, ?_⟩

Premises used: CategoryTheory.ShortComplex.homologyπ, inferInstance, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.liftCycles
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
mpr : (π₂ ≫ π₁) ≫ γ = CategoryStruct.comp (Y := S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) (homologyMap φ)
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ S₁.homology), π ≫ γ = x ≫ homologyMap φ

Tactic:
refine ⟨A₂, π₂ ≫ π₁, inferInstance, S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ, ?_⟩
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
mpr : ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ (π₂ ≫ π₁) ≫ γ = CategoryStruct.comp (Y := S₁.homology) (S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ) (homologyMap φ)

Tactic:
simp only [assoc, fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements, CategoryTheory.ShortComplex.comp_liftCycles_assoc, CategoryTheory.ShortComplex.homologyπ_naturality
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ 𝟙 A₂ ≫ π₂ ≫ y₂ = 𝟙 A₂ ≫ x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
simpa only [id_comp] using hy₁

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Refinements
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
    y₂ ≫ S₂.g = 0 →
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ S₁.X₂) (_ : x₂ ≫ S₁.g = 0) (y₁ : A' ⟶ S₂.X₁),
        π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
A : C
γ : A ⟶ S₂.homology
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
y₂ : A₁ ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
fac : π₁ ≫ γ = S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A₂ ⟶ S₂.X₁
hy₁ : π₂ ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
⊢ ∃ (A' : C) (π : A' ⟶ A₂) (_ : Epi π) (x₁ : A' ⟶ S₂.X₁), π ≫ π₂ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f

Tactic:
exact ⟨A₂, 𝟙 _, inferInstance, y₁, by simpa only [id_comp] using hy₁⟩
-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
rw :
  Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj F.rightDerivedToHomotopyCategory X) (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Functor.map F.rightDerivedToHomotopyCategory f)
    (Iso.hom (I.isoRightDerivedToHomotopyCategoryObj F) ≫
      Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)) φ ≫
        Iso.inv (J.isoRightDerivedToHomotopyCategoryObj F))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.up ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ))
        I.cocomplex)
      (Functor.obj F.rightDerivedToHomotopyCategory Y))
    (Iso.inv (I.isoRightDerivedToHomotopyCategoryObj F) ≫ Functor.map F.rightDerivedToHomotopyCategory f)
    (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)) φ ≫
      Iso.inv (J.isoRightDerivedToHomotopyCategoryObj F))

Tactic:
rw [← cancel_epi (I.isoRightDerivedToHomotopyCategoryObj F).hom, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom