awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
a :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (e.homRestrict (e.liftExtend (K.restrictionToTruncGE' e) ⋯))
      (truncGE'Map φ e))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₁ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₂ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (restrictionMap φ e ≫ e.homRestrict (e.liftExtend (L.restrictionToTruncGE' e) ⋯))
⊢ Eq (α := K.restriction e ⟶ L.truncGE' e)
    (e.homRestrict
      (CategoryStruct.comp (Y := K.truncGE e) (e.liftExtend (K.restrictionToTruncGE' e) ⋯)
        (extendMap (truncGE'Map φ e) e)))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
have a₃ : Eq (α := K.restriction e ⟶ L.truncGE' e)
  (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
  (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
Tactic: rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp,
    e.homRestrict_liftExtend, restrictionToTruncGE'_naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
a :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (e.homRestrict (e.liftExtend (K.restrictionToTruncGE' e) ⋯))
      (truncGE'Map φ e))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₁ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₂ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (restrictionMap φ e ≫ e.homRestrict (e.liftExtend (L.restrictionToTruncGE' e) ⋯))
a₃ :
  Eq (α := K.restriction e ⟶ L.truncGE' e)
    (CategoryStruct.comp (Y := K.truncGE' e) (K.restrictionToTruncGE' e) (truncGE'Map φ e))
    (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
⊢ Eq (α := K.restriction e ⟶ L.truncGE' e)
    (e.homRestrict
      (CategoryStruct.comp (Y := K.truncGE e) (e.liftExtend (K.restrictionToTruncGE' e) ⋯)
        (extendMap (truncGE'Map φ e) e)))
    (e.homRestrict (φ ≫ e.liftExtend (L.restrictionToTruncGE' e) ⋯))
have a₄ : Eq (α := K.restriction e ⟶ L.truncGE' e) (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
  (restrictionMap φ e ≫ L.restrictionToTruncGE' e)
Tactic: rw [e.homRestrict_comp_extendMap, e.homRestrict_liftExtend, e.homRestrict_precomp,
    e.homRestrict_liftExtend, restrictionToTruncGE'_naturality]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')
have pos : ∀ (hi'' : ∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
Tactic: by_cases hi'' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
pos : ∀ (hi'' : ∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')
have neg : ∀ (hi'' : ¬∃ (i : ι), e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
Tactic: by_cases hi'' : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ∃ (i : ι), e.f i = i'
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')
have pos : ∀ (i : ι) (hi : e.f i = i'), IsZero.{v_1, u_3} ((K.truncGE e).X i')
Tactic: obtain ⟨i, hi⟩ := hi''
Cleared hypotheses: hi''
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')
have pos : ∀ (hi''' : e.BoundaryGE i), IsZero.{v_1, u_3} ((K.truncGE e).X i')
Tactic: by_cases hi''' : e.BoundaryGE i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
pos : ∀ (hi''' : e.BoundaryGE i), IsZero.{v_1, u_3} ((K.truncGE e).X i')
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')
have neg : ∀ (hi''' : ¬e.BoundaryGE i), IsZero.{v_1, u_3} ((K.truncGE e).X i')
Tactic: by_cases hi''' : e.BoundaryGE i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst_7 : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
hi''' : e.BoundaryGE i
⊢ IsZero.{v_1, u_3} ((K.truncGE e).X i')
have pos : K.pOpcycles i' ≫
    Iso.inv ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''') ≫ 𝟙 ((K.truncGE e).X i') =
  K.pOpcycles i' ≫
    CategoryStruct.comp (Y := ((K.truncGE' e).extend e).X i')
      (Iso.inv ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''')) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi
          ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''').inv,
          ← cancel_epi (HomologicalComplex.pOpcycles _ _)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
⊢ IsIso (Y := K.truncGE e) (K.πTruncGE e)
have suffices : ∀ (i' : ι'), IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
Tactic: suffices ∀ (i' : ι'), IsIso ((K.πTruncGE e).f i') by
    apply Hom.isIso_of_components
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
i' : ι'
⊢ IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
have pos : ∀ (hn : ∃ (i : ι), e.f i = i'), IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
Tactic: by_cases! hn : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
i' : ι'
pos : ∀ (hn : ∃ (i : ι), e.f i = i'), IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
⊢ IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
have neg : ∀ (hn : ∀ (i : ι), e.f i ≠ i'), IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
Tactic: by_cases! hn : ∃ i, e.f i = i'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
i' : ι'
hn : ∃ (i : ι), e.f i = i'
⊢ IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
have pos : ∀ (i : ι) (hi : e.f i = i'), IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
Tactic: obtain ⟨i, hi⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
i' : ι'
i : ι
hi : e.f i = i'
⊢ IsIso (Y := (K.truncGE e).X i') (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) i')
have pos : IsIso (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
Tactic: rw [e.isIso_liftExtend_f_iff _ _ hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
i' : ι'
hn : ∀ (i : ι), e.f i ≠ i'
⊢ IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
have neg : CategoryStruct.comp (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i') 0 = 𝟙 (K.X i')
Tactic: refine ⟨0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGE (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 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : ∀ (i' : ι'), M.HasHomology i'
inst_6 : HasZeroObject.{v_1, u_3} C
inst_7 : K.IsStrictlySupported e
i' : ι'
hn : ∀ (i : ι), e.f i ≠ i'
neg : CategoryStruct.comp (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i') 0 = 𝟙 (K.X i')
⊢ IsIso (Y := (K.truncGE e).X i') (Hom.f (K.πTruncGE e) i')
have neg₁ : 0 ≫ Hom.f (K.πTruncGE e) i' = 𝟙 ((K.truncGE e).X i')
Tactic: refine ⟨0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
⊢ ((K.truncGE' e).sc' i j k).HasHomology
have this : (K.restriction e).HasHomology j
Tactic: have : (K.restriction e).HasHomology j :=
    restriction.hasHomology K e i j k hi hk rfl rfl rfl
      (e.prev_f_of_not_boundaryGE hi hj) (e.next_f hk)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this : (K.restriction e).HasHomology j
⊢ ((K.truncGE' e).sc' i j k).HasHomology
have this₁ : ((K.restriction e).sc' i j k).HasHomology
Tactic: have := ShortComplex.hasHomology_of_iso ((K.restriction e).isoSc' i j k hi hk)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this_1 : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : Functor.obj (shortComplexFunctor' C c i j k) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor' C c i j k) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) (K.restrictionToTruncGE' e)
⊢ Epi φ.τ₁
have dsimp : Epi (X := K.X (e.f i)) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this_1 : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : Functor.obj (shortComplexFunctor' C c i j k) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor' C c i j k) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) (K.restrictionToTruncGE' e)
⊢ ((K.truncGE' e).sc' i j k).HasHomology
have this₁ : Epi φ.τ₁
Tactic: have : Epi φ.τ₁ := by dsimp [φ]; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this_1 : (K.restriction e).HasHomology j
this_2 : ((K.restriction e).sc' i j k).HasHomology
φ : Functor.obj (shortComplexFunctor' C c i j k) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor' C c i j k) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) (K.restrictionToTruncGE' e)
this : Epi φ.τ₁
⊢ ((K.truncGE' e).sc' i j k).HasHomology
have this₁ : IsIso φ.τ₂
Tactic: have : IsIso φ.τ₂ := K.isIso_restrictionToTruncGE' e j hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this_1 : (K.restriction e).HasHomology j
this_2 : ((K.restriction e).sc' i j k).HasHomology
φ : Functor.obj (shortComplexFunctor' C c i j k) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor' C c i j k) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) (K.restrictionToTruncGE' e)
this_3 : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ((K.truncGE' e).sc' i j k).HasHomology
have this₁ : IsIso φ.τ₃
Tactic: have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e k (e.not_boundaryGE_next' hj hk)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncGE' e).HasHomology j
⊢ QuasiIsoAt (K := K.restriction e) (L := K.truncGE' e) (K.restrictionToTruncGE' e) j
have rw : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) (K.restriction e)) (S₂ :=
  Functor.obj (shortComplexFunctor C c j) (K.truncGE' e))
  (CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e))
Tactic: rw [quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncGE' e).HasHomology j
φ : Functor.obj (shortComplexFunctor C c j) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor C c j) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e)
⊢ Epi φ.τ₁
have dsimp : Epi (X := K.X (e.f (c.prev j))) (Y := (K.truncGE' e).X (c.prev j)) (Hom.f (K.restrictionToTruncGE' e) (c.prev j))
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncGE' e).HasHomology j
φ : Functor.obj (shortComplexFunctor C c j) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor C c j) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e)
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) (K.restriction e)) (S₂ :=
    Functor.obj (shortComplexFunctor C c j) (K.truncGE' e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e))
have this : Epi φ.τ₁
Tactic: have : Epi φ.τ₁ := by dsimp [φ]; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncGE' e).HasHomology j
φ : Functor.obj (shortComplexFunctor C c j) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor C c j) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e)
this : Epi φ.τ₁
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) (K.restriction e)) (S₂ :=
    Functor.obj (shortComplexFunctor C c j) (K.truncGE' e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e))
have this₁ : IsIso φ.τ₂
Tactic: have : IsIso φ.τ₂ := K.isIso_restrictionToTruncGE' e j hj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncGE' e).HasHomology j
φ : Functor.obj (shortComplexFunctor C c j) (K.restriction e) ⟶
  Functor.obj (shortComplexFunctor C c j) (K.truncGE' e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e)
this_1 : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) (K.restriction e)) (S₂ :=
    Functor.obj (shortComplexFunctor C c j) (K.truncGE' e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c j) (K.restrictionToTruncGE' e))
have this₁ : IsIso φ.τ₃
Tactic: have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)