awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : S.Splitting
⊢ (h.s.op ≫ S.op.f + S.op.g ≫ h.r.op).unop = Quiver.Hom.unop (𝟙 S.op.X₂)
have simp : S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
Tactic: simp only [op_X₂, Opposite.unop_op, op_X₁, op_f, op_X₃, op_g, unop_add, unop_comp,
      Quiver.Hom.unop_op, unop_id, ← h.id]
-- 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_1 : ShortComplex.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} Cᵒᵖ
h : Splitting.{v_1, u_1} (C := Cᵒᵖ) S
⊢ (h.s.unop ≫ S.unop.f + S.unop.g ≫ h.r.unop).op = Quiver.Hom.op (𝟙 S.unop.X₂)
have simp : S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
Tactic: simp only [unop_X₂, Opposite.op_unop, unop_X₁, unop_f, unop_X₃, unop_g, op_add,
      op_comp, Quiver.Hom.op_unop, op_id, ← h.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
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
inst_3 : Mono S.f
⊢ IsIso h.f'
have this : Epi h.f'
Tactic: have := hS.epi_f' h
-- 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
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
inst_3 : Mono S.f
this : Epi h.f'
⊢ IsIso h.f'
have this₁ : Mono h.f'
Tactic: have := mono_of_mono_fac h.f'_i
-- 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
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
inst_3 : Epi S.g
⊢ IsIso h.g'
have this : Mono h.g'
Tactic: have := hS.mono_g' h
-- 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
inst_2 : Balanced.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
inst_3 : Epi S.g
this : Mono h.g'
⊢ IsIso h.g'
have this₁ : Epi h.g'
Tactic: have := epi_of_epi_fac h.p_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 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Mono S.f
⊢ IsLimit (KernelFork.ofι 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
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 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Mono S.f
this : S.HasHomology
⊢ IsLimit (KernelFork.ofι S.f ⋯)
have this₁ : IsIso (Y := S.cycles) S.toCycles
Tactic: have := hS.isIso_toCycles
-- 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 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Epi S.g
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)
have this : S.HasHomology
Tactic: have := hS.hasHomology
-- 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 : Balanced.{v_1, u_1} C
hS : S.Exact
inst_5 : Epi S.g
this : S.HasHomology
⊢ IsColimit (CokernelCofork.ofπ S.g ⋯)
have this₁ : IsIso (X := S.opcycles) S.fromOpcycles
Tactic: have := hS.isIso_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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
⊢ Mono φ.τ₂
have rw : ∀ (P : C) (g : P ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0
Tactic: rw [mono_iff_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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
⊢ x₂ = 0
have obtain : ∀ (x₁ : A ⟶ S₁.X₁) (hx₁ : x₁ ≫ S₁.f = x₂), x₂ = 0
Tactic: obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S₁.f = x₂ := ⟨_, h₁.lift_f x₂
    (by simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂])⟩
-- 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ x₂ = 0
have rw : x₁ ≫ S₁.f = 0
Tactic: rw [← 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
rw : x₁ ≫ S₁.f = 0
⊢ x₂ = 0
have rw₁ : Eq (α := A ⟶ S₁.X₂) (0 ≫ S₁.f) 0
Tactic: rw [← 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
rw : x₁ ≫ S₁.f = 0
rw₁ : Eq (α := A ⟶ S₁.X₂) (0 ≫ S₁.f) 0
⊢ x₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := A ⟶ S₁.X₂) 0 0
Tactic: rw [← 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst_3 : Mono S₁.f
inst_4 : Mono S₂.f
inst_5 : Mono φ.τ₁
inst_6 : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
⊢ x₂ = 0
have suffices : x₁ = 0
Tactic: suffices x₁ = 0 by rw [← hx₁, this, zero_comp]
-- 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
⊢ Epi φ.τ₂
have this : Mono S₁.op.f
Tactic: have : Mono S₁.op.f := by dsimp; infer_instance
-- 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Epi φ.τ₂
have this₁ : Mono S₂.op.f
Tactic: have : Mono S₂.op.f := by dsimp; infer_instance
-- 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Epi φ.τ₂
have this₁ : Mono (opMap φ).τ₁
Tactic: have : Mono (opMap φ).τ₁ := by dsimp; infer_instance
-- 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Epi φ.τ₂
have this₁ : Mono (opMap φ).τ₃
Tactic: have : Mono (opMap φ).τ₃ := by dsimp; infer_instance
-- 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
inst_2 : Balanced.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂ : S₂.Exact
inst_3 : Epi S₁.g
inst_4 : Epi S₂.g
inst_5 : Epi φ.τ₁
inst_6 : Epi φ.τ₃
this_1 : Mono S₁.op.f
this_2 : Mono S₂.op.f
this_3 : Mono (opMap φ).τ₁
this : Mono (opMap φ).τ₃
⊢ Epi φ.τ₂
have this₁ : Mono (opMap φ).τ₂
Tactic: have := mono_τ₂_of_exact_of_mono (opMap φ) h₂.op
-- 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
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
⊢ S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))
have mp : S.Exact ∧ Mono S.f → Nonempty (IsLimit (KernelFork.ofι S.f sorry))
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
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
mp : S.Exact ∧ Mono S.f → Nonempty (IsLimit (KernelFork.ofι S.f ⋯))
⊢ S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))
have mpr : Nonempty (IsLimit (KernelFork.ofι S.f sorry)) → S.Exact ∧ Mono 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
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
⊢ S.Exact ∧ Epi S.g ↔ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))
have mp : S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g sorry))
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
inst_2 : Balanced.{v_1, u_1} C
inst_3 : S.HasHomology
mp : S.Exact ∧ Epi S.g → Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))
⊢ S.Exact ∧ Epi S.g ↔ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯))
have mpr : Nonempty (IsColimit (CokernelCofork.ofπ S.g sorry)) → S.Exact ∧ Epi S.g
Tactic: constructor
-- 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 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Mono (X := X₁ (kernelSequence f)) (ShortComplex.f (kernelSequence f))
have dsimp : Mono (X := kernel f) (kernel.ι f)
Tactic: dsimp
-- 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 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi (X := X₂ (cokernelSequence f)) (g (cokernelSequence f))
have dsimp : Epi (Y := cokernel f) (cokernel.π f)
Tactic: dsimp
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw : S₁.g ≫ φ.τ₃ = 0
Tactic: rw [φ.comm₂₃, hg₁, 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [φ.comm₂₃, hg₁, 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
Tactic: rw [φ.comm₂₃, hg₁, 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw : S₁.g ≫ φ.τ₃ = 0
Tactic: rw [φ.comm₂₃, hg₁, 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [φ.comm₂₃, hg₁, 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
rw : S₁.g ≫ φ.τ₃ = 0
rw₁ : Eq (α := S₁.X₂ ⟶ S₂.X₃) (0 ≫ φ.τ₃) 0
⊢ φ.τ₂ ≫ S₂.g = 0
have rw₂ : Eq.{v_1 + 1} (α := S₁.X₂ ⟶ S₂.X₃) 0 0
Tactic: rw [φ.comm₂₃, hg₁, zero_comp]
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
have w : φ.τ₂ ≫ S₂.g = 0
Tactic: have w : φ.τ₂ ≫ S₂.g = 0 := by rw [φ.comm₂₃, hg₁, 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ QuasiIso φ ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
have rw : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) ↔
  { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂
Tactic: rw [quasiIso_iff_isIso_liftCycles φ hf₁ hg₁ 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
⊢ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
have mp : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) →
  { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂
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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
mp :
  IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) →
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
⊢ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) ↔
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
      Mono φ.τ₂
have mpr : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂ →
  IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry)
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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono φ.τ₂
have rw : Mono (CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ w) S₂.iCycles)
Tactic: rw [← S₂.liftCycles_i φ.τ₂ w]
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂
have this : Mono φ.τ₂
Tactic: have : Mono φ.τ₂ := by
      rw [← S₂.liftCycles_i φ.τ₂ w]
      apply mono_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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact ∧
    Mono φ.τ₂
have mp : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := sorry : ShortComplex.{v_1, u_1} C }.Exact
Tactic: refine ⟨?_, this⟩
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
have mp : IsLimit
  (KernelFork.ofι
    { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := sorry : ShortComplex.{v_1, u_1} C }.f sorry)
Tactic: apply exact_of_f_is_kernel
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
⊢ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
have mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) (h₁.lift S₂.iCycles sorry) = 𝟙 S₁.X₂
Tactic: refine ⟨⟨h₁.lift S₂.iCycles (by simp), ?_, ?_⟩⟩
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
⊢ IsIso (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯)
have mpr₁ : h₁.lift S₂.iCycles sorry ≫ S₂.liftCycles φ.τ₂ sorry = 𝟙 S₂.cycles
Tactic: refine ⟨⟨h₁.lift S₂.iCycles (by simp), ?_, ?_⟩⟩
-- 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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
⊢ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
have mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) (h₁.lift S₂.iCycles sorry) ≫ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
Tactic: rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) ≫ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
⊢ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
have mpr₁ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) (h₁.lift S₂.iCycles sorry ≫ φ.τ₂) = 𝟙 S₁.X₂ ≫ φ.τ₂
Tactic: rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) ≫ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₁ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂) = 𝟙 S₁.X₂ ≫ φ.τ₂
⊢ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
have mpr₂ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ sorry) S₂.iCycles = 𝟙 S₁.X₂ ≫ φ.τ₂
Tactic: rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_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 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ : ShortComplex.{v_1, u_1} C }.Exact
h₂ : Mono φ.τ₂
mpr : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) ≫ φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₁ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂) = 𝟙 S₁.X₂ ≫ φ.τ₂
mpr₂ : CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) S₂.iCycles = 𝟙 S₁.X₂ ≫ φ.τ₂
⊢ CategoryStruct.comp (Y := S₂.cycles) (S₂.liftCycles φ.τ₂ ⋯) (h₁.lift S₂.iCycles ⋯) = 𝟙 S₁.X₂
have mpr₃ : φ.τ₂ = 𝟙 S₁.X₂ ≫ φ.τ₂
Tactic: rw [← cancel_mono φ.τ₂, assoc, h₁.lift_f, liftCycles_i, id_comp]