awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n : ℕ
S : ComposableArrows.{v_1, u_1} C (n + 2)
h₁ : S.δlast.Exact
h₂ :
  (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact
⊢ (mk₂ (X₀ := S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1))) (X₁ := S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' n (n + 1) ⋯ ⋯ : S.obj (⟨n, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)))
      (S.map' (n + 1) (n + 2) ⋯ ⋯ : S.obj (⟨n + 1, ⋯⟩ : Fin (n + 2 + 1)) ⟶ S.obj (⟨n + 2, ⋯⟩ : Fin (n + 2 + 1)))).Exact

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
n k l : ℕ
h : k + l ≤ n
R : ComposableArrows.{v_1, u_1} C n
hR : R.Exact
⊢ (Functor.obj (natAddLEFunctor h) R).Exact

Tactic:
⟨⟨fun i _ => hR.1.1 (k + i)⟩, fun i _ => hR.exact (k + i)⟩

Premises used: CategoryTheory.ComposableArrows.IsComplex.mk, CategoryTheory.ComposableArrows.Exact.toIsComplex, CategoryTheory.ComposableArrows.Exact.mk, HAdd.hAdd, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.ComposableArrows.Exact.exact
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : Preadditive.{v_2, u_2} C
inst_2 : Balanced.{v_2, u_2} C
n : ℕ
S : ComposableArrows.{v_2, u_2} C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ :
  Eq (α := S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (0 : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
⊢ Mono (S.sc ⋯ k ⋯).g

Tactic:
have := (hS.exact k).mono_g h₀
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : Preadditive.{v_2, u_2} C
inst_2 : Balanced.{v_2, u_2} C
n : ℕ
S : ComposableArrows.{v_2, u_2} C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ :
  Eq (α := S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (0 : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
this : Mono (S.sc ⋯ k ⋯).g
⊢ Epi (S.sc ⋯ (k + 1) hk).f

Tactic:
have := (hS.exact (k + 1)).epi_f h₁
-- Module: Mathlib.Algebra.Homology.ExactSequence
Goal:
C : Type u_2
inst : Category.{v_2, u_2} C
inst_1 : Preadditive.{v_2, u_2} C
inst_2 : Balanced.{v_2, u_2} C
n : ℕ
S : ComposableArrows.{v_2, u_2} C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ :
  Eq (α := S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (S.map' k (k + 1) ⋯ ⋯ : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
    (0 : S.obj (⟨k, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 1, ⋯⟩)
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
this_1 : Mono (S.sc ⋯ k ⋯).g
this : Epi (S.sc ⋯ (k + 1) hk).f
⊢ IsIso (X := S.obj ⟨k + 1, ⋯⟩) (Y := S.obj ⟨k + 2, ⋯⟩)
    (S.map' (k + 1) (k + 2) ⋯ ⋯ : S.obj (⟨k + 1, ⋯⟩ : Fin (n + 1)) ⟶ S.obj ⟨k + 2, ⋯⟩)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
rw :
  (K.sc' i j k).Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j
⊢ K.ExactAt j ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
rw [K.exactAt_iff' i j k hi hk]

Premises used: HomologicalComplex.exactAt_iff'
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ (K.sc' i j k).Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
(K.sc' i j k).exact_iff_exact_up_to_refinements

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements, HomologicalComplex.sc'
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ (K.sc' i j k).Exact ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
exact (K.sc' i j k).exact_iff_exact_up_to_refinements

Premises used: CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements, HomologicalComplex.sc'
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
γ : A ⟶ K.homology i
j : ι
hj : c.next i = j
subst :
  ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : Eq (α := A' ⟶ K.X (c.next i)) (z ≫ K.d i (c.next i)) 0),
    π ≫ γ = K.liftCycles z (c.next i) ⋯ hz ≫ K.homologyπ i
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : z ≫ K.d i j = 0),
    π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
γ : A ⟶ K.homology i
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : Eq (α := A' ⟶ K.X (c.next i)) (z ≫ K.d i (c.next i)) 0),
    π ≫ γ = K.liftCycles z (c.next i) ⋯ hz ≫ K.homologyπ i

Tactic:
(K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements, HomologicalComplex.liftCycles, HomologicalComplex.homology, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
γ : A ⟶ K.homology i
⊢ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : Eq (α := A' ⟶ K.X (c.next i)) (z ≫ K.d i (c.next i)) 0),
    π ≫ γ = K.liftCycles z (c.next i) ⋯ hz ≫ K.homologyπ i

Tactic:
exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ

Premises used: CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
subst :
  ∀ (hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0),
    Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) ⋯ hx₂ ≫ K.homologyπ j) 0 ↔
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
subst hi hk
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
x₂ : A ⟶ K.X j
hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) ⋯ hx₂ ≫ K.homologyπ j) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j

Tactic:
(K.sc j).liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements x₂ hx₂

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, HomologicalComplex.liftCycles, HomologicalComplex.homology, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
x₂ : A ⟶ K.X j
hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) ⋯ hx₂ ≫ K.homologyπ j) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j

Tactic:
exact (K.sc j).liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements x₂ hx₂

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
hx₂' : x₂' ≫ K.d j k = 0
subst :
  ∀ (hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0)
    (hx₂' : Eq (α := A ⟶ K.X (c.next j)) (x₂' ≫ K.d j (c.next j)) 0),
    Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) ⋯ hx₂ ≫ K.homologyπ j)
        (K.liftCycles x₂' (c.next j) ⋯ hx₂' ≫ K.homologyπ j) ↔
      ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d (c.prev j) j
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j) (K.liftCycles x₂' k hk hx₂' ≫ K.homologyπ j) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d i j

Tactic:
subst hi hk
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0
hx₂' : Eq (α := A ⟶ K.X (c.next j)) (x₂' ≫ K.d j (c.next j)) 0
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) ⋯ hx₂ ≫ K.homologyπ j)
      (K.liftCycles x₂' (c.next j) ⋯ hx₂' ≫ K.homologyπ j) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d (c.prev j) j

Tactic:
(K.sc j).liftCycles_comp_homologyπ_eq_iff_up_to_refinements x₂ x₂' hx₂ hx₂'

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements, HomologicalComplex.liftCycles, HomologicalComplex.homology, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0
hx₂' : Eq (α := A ⟶ K.X (c.next j)) (x₂' ≫ K.d j (c.next j)) 0
⊢ Eq (α := A ⟶ K.homology j) (K.liftCycles x₂ (c.next j) ⋯ hx₂ ≫ K.homologyπ j)
      (K.liftCycles x₂' (c.next j) ⋯ hx₂' ≫ K.homologyπ j) ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d (c.prev j) j

Tactic:
exact (K.sc j).liftCycles_comp_homologyπ_eq_iff_up_to_refinements x₂ x₂' hx₂ hx₂'

Premises used: CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
A : C
z₂ : A ⟶ K.cycles j
subst :
  z₂ ≫ K.homologyπ j = 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = x₁ ≫ K.toCycles (c.prev j) j
⊢ z₂ ≫ K.homologyπ j = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ z₂ = x₁ ≫ K.toCycles i j

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
z₂ : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = x₁ ≫ K.toCycles (c.prev j) j

Tactic:
(K.sc j).comp_homologyπ_eq_zero_iff_up_to_refinements z₂

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements, CategoryTheory.ShortComplex.liftCycles, HomologicalComplex.liftCycles, HomologicalComplex.homology, HomologicalComplex.cycles, HomologicalComplex.toCycles
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
z₂ : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = x₁ ≫ K.toCycles (c.prev j) j

Tactic:
exact (K.sc j).comp_homologyπ_eq_zero_iff_up_to_refinements z₂

Premises used: CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
A : C
z₂ z₂' : A ⟶ K.cycles j
subst :
  z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles (c.prev j) j
⊢ z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles i j

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
z₂ z₂' : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles (c.prev j) j

Tactic:
(K.sc j).comp_homologyπ_eq_iff_up_to_refinements z₂ z₂'

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.comp_homologyπ_eq_iff_up_to_refinements, CategoryTheory.ShortComplex.liftCycles, HomologicalComplex.liftCycles, HomologicalComplex.homology, HomologicalComplex.cycles, HomologicalComplex.toCycles
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
A : C
z₂ z₂' : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles (c.prev j) j

Tactic:
exact (K.sc j).comp_homologyπ_eq_iff_up_to_refinements z₂ z₂'

Premises used: CategoryTheory.ShortComplex.comp_homologyπ_eq_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
z : A ⟶ K.X i
j : ι
hj : c.prev i = j
subst :
  Eq (α := A ⟶ K.opcycles i) (z ≫ K.pOpcycles i) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ K.X (c.prev i)), π ≫ z = x ≫ K.d (c.prev i) i
⊢ Eq (α := A ⟶ K.opcycles i) (z ≫ K.pOpcycles i) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ K.X j), π ≫ z = x ≫ K.d j i

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
A : C
i : ι
z : A ⟶ K.X i
⊢ Eq (α := A ⟶ K.opcycles i) (z ≫ K.pOpcycles i) 0 ↔
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x : A' ⟶ K.X (c.prev i)), π ≫ z = x ≫ K.d (c.prev i) i

Tactic:
apply (K.sc i).comp_pOpcycles_eq_zero_iff_up_to_refinements

Premises used: CategoryTheory.ShortComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
subst :
  Mono (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0 →
        ∀ (y₁ : A ⟶ L.X (c.prev j)),
          x₂ ≫ φ.f j = y₁ ≫ L.d (c.prev j) j →
            ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j
⊢ Mono (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 →
        ∀ (y₁ : A ⟶ L.X i),
          x₂ ≫ φ.f j = y₁ ≫ L.d i j → ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X i), π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
subst hi hk
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
j : ι
⊢ Mono (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      Eq (α := A ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0 →
        ∀ (y₁ : A ⟶ L.X (c.prev j)),
          x₂ ≫ φ.f j = y₁ ≫ L.d (c.prev j) j →
            ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ K.X (c.prev j)), π ≫ x₂ = x₁ ≫ K.d (c.prev j) j

Tactic:
apply ShortComplex.mono_homologyMap_iff_up_to_refinements

Premises used: CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
subst :
  Epi (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
      Eq (α := A ⟶ L.X (c.next j)) (y₂ ≫ L.d j (c.next j)) 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ K.X j) (_ :
          Eq (α := A' ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0) (y₁ : A' ⟶ L.X (c.prev j)),
          π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d (c.prev j) j
⊢ Epi (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
      y₂ ≫ L.d j k = 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ K.X j) (_ : x₂ ≫ K.d j k = 0) (y₁ : A' ⟶ L.X i),
          π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d i j

Tactic:
subst hi hk
-- Module: Mathlib.Algebra.Homology.Refinements
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
j : ι
⊢ Epi (X := K.homology j) (Y := L.homology j) (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
      Eq (α := A ⟶ L.X (c.next j)) (y₂ ≫ L.d j (c.next j)) 0 →
        ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₂ : A' ⟶ K.X j) (_ :
          Eq (α := A' ⟶ K.X (c.next j)) (x₂ ≫ K.d j (c.next j)) 0) (y₁ : A' ⟶ L.X (c.prev j)),
          π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d (c.prev j) j

Tactic:
apply ShortComplex.epi_homologyMap_iff_up_to_refinements

Premises used: CategoryTheory.ShortComplex.epi_homologyMap_iff_up_to_refinements
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
⊢ Eq (α := Abelian.image S.f ⟶ S.X₃) (Abelian.image.ι S.f ≫ S.g) 0

Tactic:
simp only [← cancel_epi (Abelian.factorThruImage S.f),
      kernel.lift_ι_assoc, zero, comp_zero]

Premises used: CategoryTheory.Abelian.factorThruImage, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernel.lift_ι_assoc, CategoryTheory.ShortComplex.zero, CategoryTheory.ShortComplex.f, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
⊢ S.abelianImageToKernel ≫ kernel.ι S.g = Abelian.image.ι S.f

Tactic:
kernel.lift_ι _ _ _

Premises used: CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.ShortComplex.abelianImageToKernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
⊢ Mono S.abelianImageToKernel

Tactic:
mono_of_mono_fac S.abelianImageToKernel_comp_kernel_ι

Premises used: CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
⊢ Eq (α := Abelian.image S.f ⟶ cokernel S.f) (S.abelianImageToKernel ≫ kernel.ι S.g ≫ cokernel.π S.f) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
W' : C
k : W' ⟶ kernel S.g
hk rw : Eq (α := W' ⟶ cokernel S.f) (k ≫ kernel.ι S.g ≫ cokernel.π S.f) 0
rw₁ rw₂ : Eq.{v + 1} (α := W' ⟶ cokernel S.f) 0 0
⊢ Eq (α := W' ⟶ cokernel S.f) ((k ≫ kernel.ι S.g) ≫ cokernel.π S.f) 0

Tactic:
rw [assoc, hk]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
W' : C
k : W' ⟶ kernel S.g
hk : Eq (α := W' ⟶ cokernel S.f) (k ≫ kernel.ι S.g ≫ cokernel.π S.f) 0
⊢ (fun {W' : C} (k : W' ⟶ kernel S.g) (hk : Eq (α := W' ⟶ cokernel S.f) (k ≫ kernel.ι S.g ≫ cokernel.π S.f) 0) ↦
          (kernel.lift (cokernel.π S.f) (k ≫ kernel.ι S.g) ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
        k hk ≫
      S.abelianImageToKernel =
    k

Tactic:
simp only [← cancel_mono (kernel.ι S.g), assoc,
      abelianImageToKernel_comp_kernel_ι, kernel.lift_ι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.ShortComplex.g, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
W' : C
k : W' ⟶ kernel S.g
hk : Eq (α := W' ⟶ cokernel S.f) (k ≫ kernel.ι S.g ≫ cokernel.π S.f) 0
b : W' ⟶ Abelian.image S.f
hb : b ≫ S.abelianImageToKernel = k
⊢ b =
    (fun {W' : C} (k : W' ⟶ kernel S.g) (hk : Eq (α := W' ⟶ cokernel S.f) (k ≫ kernel.ι S.g ≫ cokernel.π S.f) 0) ↦
        (kernel.lift (cokernel.π S.f) (k ≫ kernel.ι S.g) ⋯ : W' ⟶ kernel (Y := cokernel S.f) (cokernel.π S.f)))
      k hk

Tactic:
simp only [← cancel_mono S.abelianImageToKernel,
      ← cancel_mono (kernel.ι S.g), hb, assoc, abelianImageToKernel_comp_kernel_ι, kernel.lift_ι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.ShortComplex.g, CategoryTheory.Limits.kernel.ι, CategoryTheory.ShortComplex.abelianImageToKernel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ f' ≫ γ = 0

Tactic:
simp [γ, f']