awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₂) 0 0
Tactic: rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ Mono S.g
have this₁ : Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0
Tactic: have : S.iCycles = 0 := by rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Mono S.g
have h : ∀ {P : C} (g : P ⟶ S.X₂), g ≫ S.g = 0 → g = 0
Tactic: apply Preadditive.mono_of_cancel_zero
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ x₂ = 0
have h : CategoryStruct.comp (Y := S.cycles) (S.liftCycles x₂ hx₂) S.iCycles = 0
Tactic: rw [← S.liftCycles_i x₂ hx₂, this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ x₂ = 0
have h₁ : Eq (α := A ⟶ S.X₂) (CategoryStruct.comp (Y := S.cycles) (S.liftCycles x₂ hx₂) 0) 0
Tactic: rw [← S.liftCycles_i x₂ hx₂, this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ x₂ = 0
have h₂ : Eq.{v_1 + 1} (α := A ⟶ S.X₂) 0 0
Tactic: rw [← S.liftCycles_i x₂ hx₂, this, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ Epi S.f
have this : S.HasHomology
Tactic: have := hS.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ Epi S.f
have this₁ : Mono (X := S.opcycles) S.fromOpcycles
Tactic: have := hS.mono_fromOpcycles
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
have rw : CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles =
  CategoryStruct.comp (Y := S.opcycles) 0 S.fromOpcycles
Tactic: rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0
have rw₁ : CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles = 0
Tactic: rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0
have rw₃ : Eq.{v_1 + 1} (α := S.X₂ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ Epi S.f
have this₁ : Eq (α := S.X₂ ⟶ S.opcycles) S.pOpcycles 0
Tactic: have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Epi S.f
have h : ∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0
Tactic: apply Preadditive.epi_of_cancel_zero
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ x₂ = 0
have h : CategoryStruct.comp (Y := S.opcycles) S.pOpcycles (S.descOpcycles x₂ hx₂) = 0
Tactic: rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ x₂ = 0
have h₁ : Eq (α := S.X₂ ⟶ A) (CategoryStruct.comp (Y := S.opcycles) 0 (S.descOpcycles x₂ hx₂)) 0
Tactic: rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ x₂ = 0
have h₂ : Eq.{v_1 + 1} (α := S.X₂ ⟶ A) 0 0
Tactic: rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Mono S.g ↔ S.f = 0
have mp : Mono S.g → S.f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Mono S.g ↔ S.f = 0
have mpr : S.f = 0 → Mono S.g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f = 0
have mp : S.f ≫ S.g = 0 ≫ S.g
Tactic: rw [← cancel_mono S.g, zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.f = 0
have mp₁ : Eq (α := S.X₁ ⟶ S.X₃) 0 (0 ≫ S.g)
Tactic: rw [← cancel_mono S.g, zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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)
⊢ S.f = 0
have mp₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_mono S.g, zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Epi S.f ↔ S.g = 0
have mp : Epi S.f → S.g = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ Epi S.f ↔ S.g = 0
have mpr : S.g = 0 → Epi S.f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.g = 0
have mp : S.f ≫ S.g = S.f ≫ 0
Tactic: rw [← cancel_epi S.f, zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.g = 0
have mp₁ : Eq (α := S.X₁ ⟶ S.X₃) 0 (S.f ≫ 0)
Tactic: rw [← cancel_epi S.f, zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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)
⊢ S.g = 0
have mp₂ : Eq.{v_1 + 1} (α := S.X₁ ⟶ S.X₃) 0 0
Tactic: rw [← cancel_epi S.f, zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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₂
have this : Mono S.g
Tactic: have := hS.mono_g hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ IsZero.{v_1, u_1} S.X₂ ↔ S.f = 0 ∧ S.g = 0
have mp : IsZero.{v_1, u_1} S.X₂ → S.f = 0 ∧ S.g = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ IsZero.{v_1, u_1} S.X₂ ↔ S.f = 0 ∧ S.g = 0
have mpr : S.f = 0 ∧ S.g = 0 → IsZero.{v_1, u_1} S.X₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ s.r ≫ S.f = 𝟙 S.X₂ - S.g ≫ s.s
have rw : s.r ≫ S.f = s.r ≫ S.f + S.g ≫ s.s - S.g ≫ s.s
Tactic: rw [← s.id, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ s.r ≫ S.f = 𝟙 S.X₂ - S.g ≫ s.s
have rw₁ : s.r ≫ S.f = s.r ≫ S.f
Tactic: rw [← s.id, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f
have rw : S.g ≫ s.s = s.r ≫ S.f + S.g ≫ s.s - s.r ≫ S.f
Tactic: rw [← s.id, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f
have rw₁ : S.g ≫ s.s = S.g ≫ s.s
Tactic: rw [← s.id, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ Mono S.f
have this : IsSplitMono S.f
Tactic: have := s.isSplitMono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
have this : IsSplitEpi S.g
Tactic: have := s.isSplitEpi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ s.s ≫ s.r = 0
have this : Epi S.g
Tactic: have := s.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ s = s'
have this : Epi S.g
Tactic: have := s.epi_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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 = s'
have eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
Tactic: have eq := s.id
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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'
have eq₁ : s.s = s'.s
Tactic: rw [← s'.id, h, add_right_inj, cancel_epi S.g] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ s = s'
have 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'
Tactic: cases s
Cleared hypotheses: s, h, eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
⊢ s = s'
have this : Mono S.f
Tactic: have := s.mono_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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 = s'
have eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
Tactic: have eq := s.id
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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 = s'
have eq₁ : s.r = s'.r
Tactic: rw [← s'.id, h, add_left_inj, cancel_mono S.f] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ s = s'
have 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'
Tactic: cases s
Cleared hypotheses: s, h, eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.LeftHomologyData
have have : (hi : IsLimit (KernelFork.ofι S.f sorry)) → 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])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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 ⋯)
⊢ S.LeftHomologyData
have hf' : f' = 𝟙 (KernelFork.ofι S.f sorry).pt
Tactic: have hf' : f' = 𝟙 _ := by simp [f']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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 ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
⊢ S.LeftHomologyData
have wπ : Eq (α := (KernelFork.ofι S.f sorry).pt ⟶ 0) (f' ≫ 0) 0
Tactic: have wπ : f' ≫ (0 : S.X₁ ⟶ 0) = 0 := comp_zero
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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 ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0
⊢ Epi f'
have rw : Epi.{v_1, u_1} (𝟙 (KernelFork.ofι S.f sorry).pt)
Tactic: rw [hf']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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 ⋯)
hf' : f' = 𝟙 (KernelFork.ofι S.f ⋯).pt
wπ : Eq (α := (KernelFork.ofι S.f ⋯).pt ⟶ 0) (f' ≫ 0) 0
⊢ S.LeftHomologyData
have have : (hπ : IsColimit (CokernelCofork.ofπ 0 wπ)) → S.LeftHomologyData
Tactic: have hπ : IsColimit (CokernelCofork.ofπ 0 wπ) := CokernelCofork.IsColimit.ofEpiOfIsZero _
      (by rw [hf']; infer_instance) (isZero_zero _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
⊢ S.RightHomologyData
have have : (hp : IsColimit (CokernelCofork.ofπ S.g sorry)) → S.RightHomologyData
Tactic: have hp := CokernelCofork.IsColimit.ofπ S.g S.zero
    (fun x _ => s.s ≫ x)
    (fun x hx => by simp only [s.g_s_assoc, sub_comp, id_comp, sub_eq_self, assoc, hx, comp_zero])
    (fun x _ b hb => by simp only [← hb, s.s_g_assoc])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
⊢ S.RightHomologyData
have hg' : g' = 𝟙 (CokernelCofork.ofπ S.g sorry).pt
Tactic: have hg' : g' = 𝟙 _ := by simp [g']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
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
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
⊢ S.RightHomologyData
have wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g sorry).pt) (0 ≫ g') 0
Tactic: have wι : (0 : 0 ⟶ S.X₃) ≫ g' = 0 := zero_comp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
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
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
⊢ Mono g'
have rw : Mono.{v_1, u_1} (𝟙 (CokernelCofork.ofπ S.g sorry).pt)
Tactic: rw [hg']