awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx : f' ≫ x = 0
rw : φ.τ₁ ≫ h.f' ≫ x = φ.τ₁ ≫ 0
rw₁ : f' ≫ x = φ.τ₁ ≫ 0
rw₂ : Eq (α := S₁.X₁ ⟶ Z') 0 (φ.τ₁ ≫ 0)
⊢ h.f' ≫ x = 0
have rw₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ Z') 0 0
Tactic: rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx_1 : f' ≫ x = 0
b : h.H ⟶ Z'
hx : h.π ≫ b = x
⊢ b = (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx_1
have rw : h.π ≫ b = h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x sorry) x hx_1
Tactic: rw [← cancel_epi h.π, π_descH, hx]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z' : C
x : h.K ⟶ Z'
hx_1 : f' ≫ x = 0
b : h.H ⟶ Z'
hx : h.π ≫ b = x
rw : h.π ≫ b = h.π ≫ (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx_1
rw₁ : h.π ≫ b = x
⊢ b = (fun {Z' : C} (x : h.K ⟶ Z') (hx : f' ≫ x = 0) ↦ h.descH x ⋯) x hx_1
have rw₂ : x = x
Tactic: rw [← cancel_epi h.π, π_descH, hx]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
⊢ S₁.LeftHomologyData
have have : (hπ : IsColimit (CokernelCofork.ofπ h.π wπ)) → S₁.LeftHomologyData
Tactic: have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) := CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => h.descH x (by rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]))
    (fun x hx => π_descH _ _ _)
    (fun x hx b hx => by rw [← cancel_epi h.π, π_descH, hx])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₃ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₃ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₄ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₃ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₄ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₅ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₃ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₄ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
rw₅ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₆ : S₁.f = S₁.f ≫ 𝟙 S₁.X₂
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
rw : (ofEpiOfIsIsoOfMono' φ h).f' ≫ (ofEpiOfIsIsoOfMono' φ h).i = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₁ : S₁.f = (φ.τ₁ ≫ h.f') ≫ (ofEpiOfIsIsoOfMono' φ h).i
rw₂ : S₁.f = (φ.τ₁ ≫ h.f') ≫ h.i ≫ inv φ.τ₂
rw₃ : S₁.f = φ.τ₁ ≫ h.f' ≫ h.i ≫ inv φ.τ₂
rw₄ : S₁.f = φ.τ₁ ≫ S₂.f ≫ inv φ.τ₂
rw₅ : S₁.f = S₁.f ≫ φ.τ₂ ≫ inv φ.τ₂
rw₆ : S₁.f = S₁.f ≫ 𝟙 S₁.X₂
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'
have rw₇ : S₁.f = S₁.f
Tactic: rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
    assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (leftHomologyMap' φ h₁ h₂')
have rw : IsIso (Y := h₂'.H) (LeftHomologyMapData.φH (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁))
Tactic: rw [(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (Y := h₂'.H) (LeftHomologyMapData.φH (LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁))
have dsimp : IsIso.{v_1, u_1} (𝟙 h₁.H)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (leftHomologyMap' φ h₁ h₂)
have this : IsIso (leftHomologyMap' φ h₁ h₂')
Tactic: have : IsIso (leftHomologyMap' φ h₁ h₂') := by
    rw [(LeftHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).leftHomologyMap'_eq]
    dsimp
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
⊢ IsIso (leftHomologyMap' φ h₁ h₂)
have eq : leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
Tactic: have eq := leftHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
eq : leftHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (leftHomologyMap' φ h₁ h₂)
have eq₁ : leftHomologyMap' φ h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
Tactic: rw [comp_id] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
inst_2 : Epi φ.τ₁
inst_3 : IsIso φ.τ₂
inst_4 : Mono φ.τ₃
h₂' : S₂.LeftHomologyData := LeftHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (leftHomologyMap' φ h₁ h₂')
eq : leftHomologyMap' φ h₁ h₂ = leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (leftHomologyMap' φ h₁ h₂)
have rw : IsIso (leftHomologyMap' φ h₁ h₂' ≫ leftHomologyMap' (𝟙 S₂) h₂' h₂)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
A' : C
α : A' ⟶ A
⊢ (α ≫ k) ≫ S.g = 0
have rw : α ≫ k ≫ S.g = 0
Tactic: rw [assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
A' : C
α : A' ⟶ A
rw : α ≫ k ≫ S.g = 0
⊢ (α ≫ k) ≫ S.g = 0
have rw₁ : Eq (α := A' ⟶ S.X₃) (α ≫ 0) 0
Tactic: rw [assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
A' : C
α : A' ⟶ A
rw : α ≫ k ≫ S.g = 0
rw₁ : Eq (α := A' ⟶ S.X₃) (α ≫ 0) 0
⊢ (α ≫ k) ≫ S.g = 0
have rw₂ : Eq.{v_1 + 1} (α := A' ⟶ S.X₃) 0 0
Tactic: rw [assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0
have rw : (x ≫ S.f) ≫ S.g = 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
⊢ k ≫ S.g = 0
have rw₁ : x ≫ S.f ≫ S.g = 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
rw₁ : x ≫ S.f ≫ S.g = 0
⊢ k ≫ S.g = 0
have rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
x : A ⟶ S.X₁
hx : k = x ≫ S.f
rw : (x ≫ S.f) ≫ S.g = 0
rw₁ : x ≫ S.f ≫ S.g = 0
rw₂ : Eq (α := A ⟶ S.X₃) (x ≫ 0) 0
⊢ k ≫ S.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
Tactic: rw [hx, assoc, S.zero, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
⊢ S.f = 𝟙 S.X₁ ≫ S.f
have rw : S.f = S.f
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
φ : S ⟶ S₁
inst_3 : S₁.HasLeftHomology
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0
have rw : k ≫ φ.τ₂ ≫ S₁.g = 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
φ : S ⟶ S₁
inst_3 : S₁.HasLeftHomology
rw : k ≫ φ.τ₂ ≫ S₁.g = 0
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0
have rw₁ : k ≫ S.g ≫ φ.τ₃ = 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
φ : S ⟶ S₁
inst_3 : S₁.HasLeftHomology
rw : k ≫ φ.τ₂ ≫ S₁.g = 0
rw₁ : k ≫ S.g ≫ φ.τ₃ = 0
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0
have rw₂ : Eq (α := A ⟶ S₁.X₃) (0 ≫ φ.τ₃) 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
φ : S ⟶ S₁
inst_3 : S₁.HasLeftHomology
rw : k ≫ φ.τ₂ ≫ S₁.g = 0
rw₁ : k ≫ S.g ≫ φ.τ₃ = 0
rw₂ : Eq (α := A ⟶ S₁.X₃) (0 ≫ φ.τ₃) 0
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ S₁.X₃) 0 0
Tactic: rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
⊢ Eq (α := A ⟶ S.cycles) (h.liftK k hk ≫ Iso.inv h.cyclesIso) (S.liftCycles k hk)
have rw : Eq (α := A ⟶ S.cycles)
  (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso) ≫ Iso.inv h.cyclesIso)
  (S.liftCycles k hk)
Tactic: rw [← h.liftCycles_comp_cyclesIso_hom, assoc, Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
rw :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso) ≫ Iso.inv h.cyclesIso)
    (S.liftCycles k hk)
⊢ Eq (α := A ⟶ S.cycles) (h.liftK k hk ≫ Iso.inv h.cyclesIso) (S.liftCycles k hk)
have rw₁ : Eq (α := A ⟶ S.cycles)
  (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso ≫ Iso.inv h.cyclesIso))
  (S.liftCycles k hk)
Tactic: rw [← h.liftCycles_comp_cyclesIso_hom, assoc, Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
rw :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso) ≫ Iso.inv h.cyclesIso)
    (S.liftCycles k hk)
rw₁ :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso ≫ Iso.inv h.cyclesIso))
    (S.liftCycles k hk)
⊢ Eq (α := A ⟶ S.cycles) (h.liftK k hk ≫ Iso.inv h.cyclesIso) (S.liftCycles k hk)
have rw₂ : S.liftCycles k hk ≫ 𝟙 S.cycles = S.liftCycles k hk
Tactic: rw [← h.liftCycles_comp_cyclesIso_hom, assoc, Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst_2 : S.HasLeftHomology
rw :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso) ≫ Iso.inv h.cyclesIso)
    (S.liftCycles k hk)
rw₁ :
  Eq (α := A ⟶ S.cycles)
    (CategoryStruct.comp (Y := S.cycles) (S.liftCycles k hk) (Iso.hom h.cyclesIso ≫ Iso.inv h.cyclesIso))
    (S.liftCycles k hk)
rw₂ : S.liftCycles k hk ≫ 𝟙 S.cycles = S.liftCycles k hk
⊢ Eq (α := A ⟶ S.cycles) (h.liftK k hk ≫ Iso.inv h.cyclesIso) (S.liftCycles k hk)
have rw₃ : Eq (α := A ⟶ S.cycles) (S.liftCycles k hk) (S.liftCycles k hk)
Tactic: rw [← h.liftCycles_comp_cyclesIso_hom, assoc, Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
inst_3 : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
⊢ HasCokernel (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
have this : HasColimit (parallelPair h.f' 0)
Tactic: haveI : HasColimit (parallelPair h.f' 0) := ⟨⟨⟨_, h.hπ'⟩⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (cyclesMap' φ h₁ h₂)
have refine_1 : (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0
Tactic: refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
refine_1 : (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0
⊢ IsIso (cyclesMap' φ h₁ h₂)
have refine_2 : cyclesMap' φ h₁ h₂ ≫ h₁.liftK (h₂.i ≫ inv φ.τ₂) sorry = 𝟙 h₁.K
Tactic: refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.LeftHomology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₂_1 : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
refine_1 : (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0
refine_2 : cyclesMap' φ h₁ h₂ ≫ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ = 𝟙 h₁.K
⊢ IsIso (cyclesMap' φ h₁ h₂)
have refine_3 : h₁.liftK (h₂.i ≫ inv φ.τ₂) sorry ≫ cyclesMap' φ h₁ h₂ = 𝟙 h₂.K
Tactic: refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩