awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
pos :
  ∀ (hi' : ∃ (j' : ι'), c'.Rel i' j'),
    Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
      (homologyMap (K.shortComplexTruncLE e).g i')
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
have neg : ∀ (hi' : ¬∃ (j' : ι'), c'.Rel i' j'),
  Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
Tactic: by_cases hi' : ∃ j', c'.Rel i' j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∃ (j' : ι'), c'.Rel i' j'
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
have pos : ∀ (j' : ι') (hj' : c'.Rel i' j'),
  Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
Tactic: obtain ⟨j', hj'⟩ := hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsIso (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
have this : Mono (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
  (homologyMap (K.shortComplexTruncLE e).g i')
Tactic: have := K.mono_homologyMap_shortComplexTruncLE_g e i' hi'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ QuasiIsoAt (K.shortComplexTruncLE e).g i'
have rw : IsIso (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
  (homologyMap (K.shortComplexTruncLE e).g i')
Tactic: rw [quasiIsoAt_iff_isIso_homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
⊢ (K.shortComplexTruncLE e).X₃.ExactAt (e.f i)
have rw : IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
Tactic: rw [exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have pos : ∀ (hi : ∃ (j' : ι'), c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
Tactic: by_cases hi : ∃ j', c'.Rel (e.f i) j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
pos : ∀ (hi : ∃ (j' : ι'), c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg : ∀ (hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
Tactic: by_cases hi : ∃ j', c'.Rel (e.f i) j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ∃ (j' : ι'), c'.Rel (e.f i) j'
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have pos : ∀ (j' : ι') (hj' : c'.Rel (e.f i) j'), IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
Tactic: obtain ⟨j', hj'⟩ := hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have pos : { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
      X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
      g := ShortComplex.ShortExact.δ sorry (e.f i) j' hj', zero := sorry : ShortComplex.{v_1, u_3} C }.f =
  0
Tactic: apply ((K.shortComplexTruncLE_shortExact e).homology_exact₃ (e.f i) j' hj').isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f =
    0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have pos₁ : { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
      X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
      g := ShortComplex.ShortExact.δ sorry (e.f i) j' hj', zero := sorry : ShortComplex.{v_1, u_3} C }.g =
  0
Tactic: apply ((K.shortComplexTruncLE_shortExact e).homology_exact₃ (e.f i) j' hj').isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f =
    0
have pos : Eq (α :=
  (K.truncLE e).homology (e.f i) ⟶
    { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ sorry (e.f i) j' hj', zero := sorry : ShortComplex.{v_1, u_3} C }.X₂)
  (homologyMap (K.ιTruncLE e) (e.f i) ≫
    { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ShortComplex.ShortExact.δ sorry (e.f i) j' hj', zero := sorry : ShortComplex.{v_1, u_3} C }.f)
  0
Tactic: rw [← cancel_epi (homologyMap (K.ιTruncLE e) (e.f i)), comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ Eq (α :=
    (K.truncLE e).homology (e.f i) ⟶
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.X₂)
    (homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ShortComplex.ShortExact.δ ⋯ (e.f i) j' hj', zero := ⋯ : ShortComplex.{v_1, u_3} C }.f)
    0
have pos : Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
  (CategoryStruct.comp (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
    (homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i)))
  0
Tactic: dsimp [shortComplexTruncLE]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (CategoryStruct.comp (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
      (homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i)))
    0
have pos : Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
  (homologyMap (K.ιTruncLE e ≫ cokernel.π (K.ιTruncLE e)) (e.f i)) 0
Tactic: rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (homologyMap (K.ιTruncLE e ≫ cokernel.π (K.ιTruncLE e)) (e.f i)) 0
⊢ Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (CategoryStruct.comp (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
      (homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i)))
    0
have pos₁ : Eq.{v_1 + 1} (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
  (homologyMap 0 (e.f i)) 0
Tactic: rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
pos :
  Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (homologyMap (K.ιTruncLE e ≫ cokernel.π (K.ιTruncLE e)) (e.f i)) 0
pos₁ :
  Eq.{v_1 + 1} (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (homologyMap 0 (e.f i)) 0
⊢ Eq (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i))
    (CategoryStruct.comp (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
      (homologyMap (cokernel.π (K.ιTruncLE e)) (e.f i)))
    0
have pos₂ : Eq.{v_1 + 1} (α := (K.truncLE e).homology (e.f i) ⟶ (cokernel (X := K.truncLE e) (K.ιTruncLE e)).homology (e.f i)) 0 0
Tactic: rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
⊢ IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
have dsimp : IsIso (X := (K.truncLE e).homology (e.f i)) (Y := K.homology (e.f i)) (homologyMap (K.ιTruncLE e) (e.f i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have this : IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
  (homologyMap (K.shortComplexTruncLE e).f (e.f i))
Tactic: have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg : Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₁ : Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
  (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₂ : Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (homologyMap (K.shortComplexTruncLE e).g (e.f i))
  (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₃ : Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : Abelian.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
i : ι
hi : ¬∃ (j' : ι'), c'.Rel (e.f i) j'
this :
  IsIso (X := (K.shortComplexTruncLE e).X₁.homology (e.f i)) (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i))
neg :
  Eq.{v_1 + 1} (α := (K.shortComplexTruncLE e).X₃.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i))) 0
neg₁ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i) ≫ 𝟙 ((K.shortComplexTruncLE e).X₃.homology (e.f i)))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₂ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i))
    (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₃.homology (e.f i))
      (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0)
neg₃ :
  Eq (α := (K.shortComplexTruncLE e).X₂.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).g (e.f i)) 0
⊢ IsZero.{v_1, u_3} ((K.shortComplexTruncLE e).X₃.homology (e.f i))
have neg₄ : Eq (α := (K.shortComplexTruncLE e).X₁.homology (e.f i) ⟶ (K.shortComplexTruncLE e).X₃.homology (e.f i))
  (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i)) (homologyMap (K.shortComplexTruncLE e).g (e.f i)))
  (CategoryStruct.comp (Y := (K.shortComplexTruncLE e).X₂.homology (e.f i))
    (homologyMap (K.shortComplexTruncLE e).f (e.f i)) 0)
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]