awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
rw : Mono (X := S.opcycles) S.fromOpcycles
⊢ S.Exact

Tactic:
rw [exact_iff_mono_fromOpcycles]

Premises used: CategoryTheory.ShortComplex.exact_iff_mono_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
rw :
  Eq (α := S.X₂ ⟶ S.opcycles) (S.g ≫ hS.desc (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles ⋯) : S.X₂ ⟶ S.opcycles)
    (S.pOpcycles : S.X₂ ⟶ S.opcycles)
⊢ Eq (α := S.opcycles ⟶ S.opcycles)
    (S.fromOpcycles ≫ hS.desc (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles ⋯) : S.opcycles ⟶ S.opcycles)
    (𝟙 S.opcycles : S.opcycles ⟶ S.opcycles)

Tactic:
rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Category.comp_id, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.p_fromOpcycles_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
⊢ Eq (α := S.X₂ ⟶ S.opcycles) (S.g ≫ hS.desc (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles ⋯) : S.X₂ ⟶ S.opcycles)
    (S.pOpcycles : S.X₂ ⟶ S.opcycles)

Tactic:
Cofork.IsColimit.π_desc hS

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
⊢ Eq (α := S.X₂ ⟶ S.opcycles) (S.g ≫ hS.desc (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles ⋯) : S.X₂ ⟶ S.opcycles)
    (S.pOpcycles : S.X₂ ⟶ S.opcycles)

Tactic:
exact Cofork.IsColimit.π_desc hS

Premises used: CategoryTheory.Limits.Cofork.IsColimit.π_desc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
⊢ IsSplitMono (X := S.opcycles) S.fromOpcycles

Tactic:
have : IsSplitMono S.fromOpcycles :=
    ⟨⟨{ retraction := hS.desc (CokernelCofork.ofπ S.pOpcycles S.f_pOpcycles)
        id := by
          rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
          exact Cofork.IsColimit.π_desc hS }⟩⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
this : IsSplitMono (X := S.opcycles) S.fromOpcycles
⊢ Mono (X := S.opcycles) S.fromOpcycles

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
⊢ S.HasHomology

Tactic:
have := hS.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this : S.HasHomology
⊢ Epi (Y := S.cycles) S.toCycles

Tactic:
have := hS.epi_toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this_1 : S.HasHomology
this : Epi (Y := S.cycles) S.toCycles
rw : CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles = CategoryStruct.comp (Y := S.cycles) S.toCycles 0
rw₁ : CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles = 0
rw₂ : S.f = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
⊢ Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0

Tactic:
rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.toCycles_i, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.toCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this_1 : S.HasHomology
this : Epi (Y := S.cycles) S.toCycles
⊢ Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0

Tactic:
have : S.iCycles = 0 := by rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this_1 : S.HasHomology
this_2 : Epi (Y := S.cycles) S.toCycles
this : Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0
h : ∀ {P : C} (g : P ⟶ S.X₂), g ≫ S.g = 0 → g = 0
⊢ Mono S.g

Tactic:
apply Preadditive.mono_of_cancel_zero

Premises used: CategoryTheory.Preadditive.mono_of_cancel_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this_1 : S.HasHomology
this_2 : Epi (Y := S.cycles) S.toCycles
this : Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
h : CategoryStruct.comp (Y := S.cycles) (S.liftCycles x₂ hx₂) S.iCycles = 0
h₁ : Eq (α := A ⟶ S.X₂) (CategoryStruct.comp (Y := S.cycles) (S.liftCycles x₂ hx₂) 0) 0
h₂ h₃ : Eq.{v_1 + 1} (α := A ⟶ S.X₂) 0 0
⊢ x₂ = 0

Tactic:
rw [← S.liftCycles_i x₂ hx₂, this, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.liftCycles_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hg : S.g = 0
⊢ S.HasHomology

Tactic:
have := hS.hasHomology
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hg : S.g = 0
this : S.HasHomology
⊢ Mono (X := S.opcycles) S.fromOpcycles

Tactic:
have := hS.mono_fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hg : S.g = 0
this_1 : S.HasHomology
this : Mono (X := S.opcycles) S.fromOpcycles
rw :
  CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles =
    CategoryStruct.comp (Y := S.opcycles) 0 S.fromOpcycles
rw₁ : CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles = 0
rw₂ : S.g = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
⊢ Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0

Tactic:
rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]

Premises used: CategoryTheory.ShortComplex.p_fromOpcycles, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.fromOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hg : S.g = 0
this_1 : S.HasHomology
this : Mono (X := S.opcycles) S.fromOpcycles
⊢ Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0

Tactic:
have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hg : S.g = 0
this_1 : S.HasHomology
this_2 : Mono (X := S.opcycles) S.fromOpcycles
this : Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0
h : ∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0
⊢ Epi S.f

Tactic:
apply Preadditive.epi_of_cancel_zero

Premises used: CategoryTheory.Preadditive.epi_of_cancel_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hg : S.g = 0
this_1 : S.HasHomology
this_2 : Mono (X := S.opcycles) S.fromOpcycles
this : Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 0
h : CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles x₂ hx₂) = 0
h₁ : Eq (α := S.X₂ ⟶ A) (CategoryStruct.comp (Y := S.opcycles) 0 (S.descOpcycles x₂ hx₂)) 0
h₂ h₃ : Eq.{v_1 + 1} (α := S.X₂ ⟶ A) 0 0
⊢ x₂ = 0

Tactic:
rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
mp : Mono S.g → S.f = 0
mpr : S.f = 0 → Mono S.g
⊢ Mono S.g ↔ S.f = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : Mono S.g
mp : S.f ≫ S.g = 0 ≫ S.g
mp₁ : Eq (α := S.X₁ ⟶ S.X₃) 0 (0 ≫ S.g)
mp₂ mp₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₃) 0 0
⊢ S.f = 0

Tactic:
rw [← cancel_mono S.g, zero, zero_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.zero, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
⊢ S.f = 0 → Mono S.g

Tactic:
hS.mono_g

Premises used: CategoryTheory.ShortComplex.Exact.mono_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
⊢ S.f = 0 → Mono S.g

Tactic:
exact hS.mono_g

Premises used: CategoryTheory.ShortComplex.Exact.mono_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
mp : Epi S.f → S.g = 0
mpr : S.g = 0 → Epi S.f
⊢ Epi S.f ↔ S.g = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : Epi S.f
mp : S.f ≫ S.g = S.f ≫ 0
mp₁ : Eq (α := S.X₁ ⟶ S.X₃) 0 (S.f ≫ 0)
mp₂ mp₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₃) 0 0
⊢ S.g = 0

Tactic:
rw [← cancel_epi S.f, zero, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.zero, CategoryTheory.ShortComplex.f, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
⊢ S.g = 0 → Epi S.f

Tactic:
hS.epi_f

Premises used: CategoryTheory.ShortComplex.Exact.epi_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
⊢ S.g = 0 → Epi S.f

Tactic:
exact hS.epi_f

Premises used: CategoryTheory.ShortComplex.Exact.epi_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ Mono S.g

Tactic:
have := hS.mono_g hf
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
mp : IsZero.{v_1, u_1} S.X₂ → S.f = 0 ∧ S.g = 0
mpr : S.f = 0 ∧ S.g = 0 → IsZero.{v_1, u_1} S.X₂
⊢ IsZero.{v_1, u_1} S.X₂ ↔ S.f = 0 ∧ S.g = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : IsZero.{v_1, u_1} S.X₂
⊢ S.f = 0 ∧ S.g = 0

Tactic:
⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, And.intro, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : IsZero.{v_1, u_1} S.X₂
⊢ S.f = 0 ∧ S.g = 0

Tactic:
exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero.{v_1, u_1} S.X₂

Tactic:
hS.isZero_X₂ hf hg

Premises used: CategoryTheory.ShortComplex.Exact.isZero_X₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero.{v_1, u_1} S.X₂

Tactic:
exact hS.isZero_X₂ hf hg

Premises used: CategoryTheory.ShortComplex.Exact.isZero_X₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
rw : s.r ≫ S.f = s.r ≫ S.f + S.g ≫ s.s - S.g ≫ s.s
rw₁ rw₂ : s.r ≫ S.f = s.r ≫ S.f
⊢ s.r ≫ S.f = 𝟙 S.X₂ - S.g ≫ s.s

Tactic:
rw [← s.id, add_sub_cancel_right]

Premises used: CategoryTheory.ShortComplex.Splitting.id, add_sub_cancel_right
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
rw : S.g ≫ s.s = s.r ≫ S.f + S.g ≫ s.s - s.r ≫ S.f
rw₁ rw₂ : S.g ≫ s.s = S.g ≫ s.s
⊢ S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f

Tactic:
rw [← s.id, add_sub_cancel_left]

Premises used: CategoryTheory.ShortComplex.Splitting.id, add_sub_cancel_left
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
⊢ IsSplitMono S.f

Tactic:
⟨⟨s.splitMono_f⟩⟩

Premises used: CategoryTheory.ShortComplex.Splitting.splitMono_f, Nonempty.intro, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
⊢ IsSplitMono S.f

Tactic:
have := s.isSplitMono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
this : IsSplitMono S.f
⊢ Mono S.f

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
⊢ IsSplitEpi S.g

Tactic:
⟨⟨s.splitEpi_g⟩⟩

Premises used: Nonempty.intro, CategoryTheory.IsSplitEpi.mk, CategoryTheory.ShortComplex.Splitting.splitEpi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
⊢ IsSplitEpi S.g

Tactic:
have := s.isSplitEpi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
this : IsSplitEpi S.g
⊢ Epi S.g

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
⊢ Epi S.g

Tactic:
have := s.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
this : Epi S.g
⊢ s.s ≫ s.r = 0

Tactic:
simp only [← cancel_epi S.g, comp_zero, g_s_assoc, sub_comp, id_comp,
    assoc, f_r, comp_id, sub_self]

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.Limits.comp_zero, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Splitting.g_s_assoc, CategoryTheory.ShortComplex.Splitting.f_r, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.g, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.r = s'.r
⊢ Epi S.g

Tactic:
have := s.epi_g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
⊢ s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂

Tactic:
have eq := s.id
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
⊢ s.s = s'.s

Tactic:
rw [← s'.id, h, add_right_inj, cancel_epi S.g] at eq

Premises used: CategoryTheory.ShortComplex.Splitting.id, CategoryTheory.cancel_epi, add_right_inj, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
eq : s.s = s'.s
mk :
  ∀ (r : S.X₂ ⟶ S.X₁) (s : S.X₃ ⟶ S.X₂) (f_r : S.f ≫ r = 𝟙 S.X₁) (s_g : s ≫ S.g = 𝟙 S.X₃)
    (id : r ≫ S.f + S.g ≫ s = 𝟙 S.X₂) (h : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.r = s'.r)
    (eq : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.s = s'.s),
    { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting } = s'
⊢ s = s'

Tactic:
cases s
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s' : S.Splitting
this : Epi S.g
r : S.X₂ ⟶ S.X₁
s : S.X₃ ⟶ S.X₂
f_r : S.f ≫ r = 𝟙 S.X₁
s_g : s ≫ S.g = 𝟙 S.X₃
id : r ≫ S.f + S.g ≫ s = 𝟙 S.X₂
h : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.r = s'.r
eq : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.s = s'.s
⊢ { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting } = s'

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.s = s'.s
⊢ Mono S.f

Tactic:
have := s.mono_f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
⊢ s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂

Tactic:
have eq := s.id
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
⊢ s.r = s'.r

Tactic:
rw [← s'.id, h, add_left_inj, cancel_mono S.f] at eq

Premises used: CategoryTheory.ShortComplex.Splitting.id, add_left_inj, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s s' : S.Splitting
h : s.s = s'.s
this : Mono S.f
eq : s.r = s'.r
mk :
  ∀ (r : S.X₂ ⟶ S.X₁) (s : S.X₃ ⟶ S.X₂) (f_r : S.f ≫ r = 𝟙 S.X₁) (s_g : s ≫ S.g = 𝟙 S.X₃)
    (id : r ≫ S.f + S.g ≫ s = 𝟙 S.X₂) (h : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.s = s'.s)
    (eq : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.r = s'.r),
    { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting } = s'
⊢ s = s'

Tactic:
cases s
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
s' : S.Splitting
this : Mono S.f
r : S.X₂ ⟶ S.X₁
s : S.X₃ ⟶ S.X₂
f_r : S.f ≫ r = 𝟙 S.X₁
s_g : s ≫ S.g = 𝟙 S.X₃
id : r ≫ S.f + S.g ≫ s = 𝟙 S.X₂
h : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.s = s'.s
eq : { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting }.r = s'.r
⊢ { r := r, s := s, f_r := f_r, s_g := s_g, id := id : S.Splitting } = s'

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
W' : C
x : W' ⟶ S.X₂
hx : x ≫ S.g = 0
⊢ (fun {W' : C} (x : W' ⟶ S.X₂) (x_1 : x ≫ S.g = 0) ↦ x ≫ s.r) x hx ≫ S.f = x

Tactic:
simp only [assoc, s.r_f, comp_sub, comp_id,
      sub_eq_self, reassoc_of% hx, zero_comp]

Premises used: CategoryTheory.Category.assoc, sub_eq_self, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Splitting.r_f, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
W' : C
x : W' ⟶ S.X₂
h : x ≫ S.g = 0
b : W' ⟶ S.X₁
hb : b ≫ S.f = x
⊢ b = (fun {W' : C} (x : W' ⟶ S.X₂) (x_1 : x ≫ S.g = 0) ↦ x ≫ s.r) x h

Tactic:
simp only [← hb, assoc, f_r, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.Splitting.f_r
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
have : (hi : IsLimit (KernelFork.ofι S.f ⋯)) → S.LeftHomologyData
⊢ S.LeftHomologyData

Tactic:
have hi := KernelFork.IsLimit.ofι S.f S.zero
    (fun x _ => x ≫ s.r)
    (fun x hx => by simp only [assoc, s.r_f, comp_sub, comp_id,
      sub_eq_self, reassoc_of% hx, zero_comp])
    (fun x _ b hb => by simp only [← hb, assoc, f_r, comp_id])
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
⊢ f' = 𝟙 (KernelFork.ofι S.f ⋯).pt

Tactic:
simp [f']
-- Module: Mathlib.Algebra.Homology.ShortComplex.Exact
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hi : IsLimit (KernelFork.ofι S.f ⋯)
f' : (KernelFork.ofι S.f ⋯).pt ⟶ (KernelFork.ofι S.f ⋯).pt := hi.lift (KernelFork.ofι S.f ⋯)
⊢ f' = 𝟙 (KernelFork.ofι S.f ⋯).pt

Tactic:
have hf' : f' = 𝟙 _ := by simp [f']