awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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
⊢ QuasiIso (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
have this : ∀ (i : ι) (i' : ι'),
  e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
Tactic: have : ∀ (i : ι) (i' : ι') (_ : e.f i = i'),
      QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i' := by
    rintro i _ rfl
    rw [← quasiIsoAt_iff_comp_left (K.πTruncGE e), πTruncGE_naturality φ e,
      quasiIsoAt_iff_comp_right]
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ QuasiIso (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
have rw : (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) ↔
  ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
Tactic: rw [quasiIso_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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
have mp : (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) →
  ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
Tactic: constructor
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
mp :
  (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) →
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
⊢ (∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
have mpr : (∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i') →
  ∀ (i : ι'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i
Tactic: constructor
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
have pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
have neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
Tactic: by_cases hi' : ∃ i, e.f i = i'
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
have pos : ∀ (i : ι) (hi : e.f i = i'), QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
Tactic: obtain ⟨i, hi⟩ := hi'
Cleared hypotheses: hi'
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
have neg : (L.truncGE e).ExactAt i'
Tactic: rw [quasiIsoAt_iff_exactAt]
-- 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 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
this :
  ∀ (i : ι) (i' : ι'),
    e.f i = i' → (QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
neg : (L.truncGE e).ExactAt i'
⊢ QuasiIsoAt (K := K.truncGE e) (L := L.truncGE e) (truncGEMap φ e) i'
have neg₁ : (K.truncGE e).ExactAt i'
Tactic: rw [quasiIsoAt_iff_exactAt]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLE (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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ Eq (α := (K.truncLE' e).X i ⟶ (L.truncLE' e).X i) (Hom.f (truncLE'Map φ e) i)
    (Iso.hom (K.truncLE'XIsoCycles e h hi) ≫ cyclesMap φ i' ≫ Iso.inv (L.truncLE'XIsoCycles e h hi))
have a : Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
  (Quiver.Hom.op (Hom.f (truncLE'Map φ e) i))
  (Quiver.Hom.op (Iso.hom (K.truncLE'XIsoCycles e h hi) ≫ cyclesMap φ i' ≫ Iso.inv (L.truncLE'XIsoCycles e h hi)))
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLE (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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
    (Quiver.Hom.op (Hom.f (truncLE'Map φ e) i))
    (Quiver.Hom.op (Iso.hom (K.truncLE'XIsoCycles e h hi) ≫ cyclesMap φ i' ≫ Iso.inv (L.truncLE'XIsoCycles e h hi)))
have a : Eq (α := Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
  (Hom.f (truncGE'Map (CategoryTheory.Functor.map (opFunctor C c') φ.op) e.op) i :
    { X := truncGE'.X L.op e.op,
            d := (truncGE'.d L.op e.op : (i j : ι) → truncGE'.X L.op e.op i ⟶ truncGE'.X L.op e.op j), shape := sorry,
            d_comp_d' := sorry : HomologicalComplex.{v_1, u_3, u_1} Cᵒᵖ c.symm }.X
        i ⟶
      { X := truncGE'.X K.op e.op,
            d := (truncGE'.d K.op e.op : (i j : ι) → truncGE'.X K.op e.op i ⟶ truncGE'.X K.op e.op j), shape := sorry,
            d_comp_d' := sorry : HomologicalComplex.{v_1, u_3, u_1} Cᵒᵖ c.symm }.X
        i)
  (CategoryStruct.comp (Y := Opposite.op (K.cycles i'))
      (CategoryStruct.comp (Y := Opposite.op (L.cycles i'))
        (Iso.hom (L.op.truncGE'XIsoOpcycles e.op h sorry) ≫ Iso.hom (L.opcyclesOpIso i')) (Quiver.Hom.op (cyclesMap φ i')))
      (Iso.inv (K.opcyclesOpIso i') ≫ Iso.inv (K.op.truncGE'XIsoOpcycles e.op h sorry)) :
    Opposite.op ((L.truncLE' e).X i) ⟶ Opposite.op ((K.truncLE' e).X i))
Tactic: dsimp [truncLE'Map, truncLE'XIsoCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLE (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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ IsIso (X := (K.truncLE' e).X i) (Hom.f (K.truncLE'ToRestriction e) i)
have change : IsIso (X := Opposite.unop ((K.op.truncGE' e.op).X i)) (Quiver.Hom.unop (Hom.f (K.op.restrictionToTruncGE' e.op) i))
Tactic: change IsIso ((K.op.restrictionToTruncGE' e.op).f i).unop
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLE (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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ IsIso (X := Opposite.unop ((K.op.truncGE' e.op).X i)) (Quiver.Hom.unop (Hom.f (K.op.restrictionToTruncGE' e.op) i))
have this : IsIso (X := (K.op.restriction e.op).X i) (Y := (K.op.truncGE' e.op).X i) (Hom.f (K.op.restrictionToTruncGE' e.op) i)
Tactic: have := K.op.isIso_restrictionToTruncGE' e.op i (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLE (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.IsTruncLE
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
⊢ (K.truncLE e).IsStrictlySupported e
have rw : (K.truncLE e).op.IsStrictlySupported e.op
Tactic: rw [← isStrictlySupported_op_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncLE (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.IsTruncLE
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'
⊢ (K.truncLE e).IsStrictlySupported e'
have rw : (K.truncLE e).op.IsStrictlySupported e'.op
Tactic: rw [← isStrictlySupported_op_iff]
-- 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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncLE' e).HasHomology j
⊢ QuasiIsoAt (K := K.truncLE' e) (L := K.restriction e)
    (CategoryTheory.Functor.map (unopFunctor C c.symm) (Quiver.Hom.op (K.op.restrictionToTruncGE' e.op)) :
      Functor.obj (unopFunctor C c.symm) (Opposite.op (K.op.truncGE' e.op)) ⟶
        Functor.obj (unopFunctor C c.symm) (Opposite.op (K.op.restriction e.op)))
    j
have this : (K.op.restriction e.op).HasHomology j
Tactic: have : (K.op.restriction e.op).HasHomology j :=
    inferInstanceAs ((K.restriction e).op.HasHomology 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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst_4 : (K.restriction e).HasHomology j
inst_5 : (K.truncLE' e).HasHomology j
this : (K.op.restriction e.op).HasHomology j
⊢ QuasiIsoAt (K := K.truncLE' e) (L := K.restriction e)
    (CategoryTheory.Functor.map (unopFunctor C c.symm) (Quiver.Hom.op (K.op.restrictionToTruncGE' e.op)) :
      Functor.obj (unopFunctor C c.symm) (Opposite.op (K.op.truncGE' e.op)) ⟶
        Functor.obj (unopFunctor C c.symm) (Opposite.op (K.op.restriction e.op)))
    j
have rw : QuasiIsoAt (K := K.op.restriction e.op) (L := K.op.truncGE' e.op) (K.op.restrictionToTruncGE' e.op) j
Tactic: rw [quasiIsoAt_unopFunctor_map_iff]
-- 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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ QuasiIsoAt (K := K.truncLE e) (K.ιTruncLE e) j'
have this : QuasiIsoAt (L := K.op.truncGE e.op) (K.op.πTruncGE e.op) j'
Tactic: have := K.op.quasiIsoAt_πTruncGE e.op hj'
-- 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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ QuasiIso (K := K.truncLE e) (K.ιTruncLE e) ↔ K.IsSupported e
have rw : QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op K)) (L :=
    Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
    (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (K.ιTruncLE e))) ↔
  K.op.IsSupported e.op
Tactic: rw [← quasiIso_opFunctor_map_iff, ← isSupported_op_iff]
-- 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 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
⊢ (K.truncLE e).Acyclic ↔ K.IsSupportedOutside e
have rw : (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op
Tactic: rw [← acyclic_op_iff, ← isSupportedOutside_op_iff]
-- 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 : 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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
⊢ QuasiIso (K := K.truncLE e) (L := L.truncLE e) (truncLEMap φ e) ↔ ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
have rw : QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
    Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
    (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
  ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
Tactic: rw [← quasiIso_opFunctor_map_iff]
-- 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 : 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.IsTruncLE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
⊢ QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
      Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
      (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
    ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
have simp : QuasiIso (K := Functor.obj (opFunctor C c') (Opposite.op (L.truncLE e))) (L :=
    Functor.obj (opFunctor C c') (Opposite.op (K.truncLE e)))
    (CategoryTheory.Functor.map (opFunctor C c') (Quiver.Hom.op (truncLEMap φ e))) ↔
  ∀ (i : ι) (i' : ι'),
    e.f i = i' →
      QuasiIsoAt (K := Functor.obj (opFunctor C c') (Opposite.op L)) (CategoryTheory.Functor.map (opFunctor C c') φ.op)
        i'
Tactic: simp only [← quasiIsoAt_opFunctor_map_iff φ]
-- 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
⊢ Mono (K.shortComplexTruncLE e).f
have dsimp : Mono (X := K.truncLE e) (K.ιTruncLE e)
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
⊢ Epi (K.shortComplexTruncLE e).g
have dsimp : Epi (Y := cokernel (X := K.truncLE e) (K.ιTruncLE e)) (cokernel.π (K.ιTruncLE e))
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' : ι'
hij' : c'.Rel i' j'
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0
have pos : ∀ (hj : ∃ (j : ι), e.f j = j'),
  Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ sorry i' j' hij') 0
Tactic: by_cases hj : ∃ j, e.f j = 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' j' : ι'
hij' : c'.Rel i' j'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
      (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0
have neg : ∀ (hj : ¬∃ (j : ι), e.f j = j'),
  Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ sorry i' j' hij') 0
Tactic: by_cases hj : ∃ j, e.f j = 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' j' : ι'
hij' : c'.Rel i' j'
hj : ∃ (j : ι), e.f j = j'
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology j')
    (ShortComplex.ShortExact.δ ⋯ i' j' hij') 0
have pos : ∀ (j : ι) (hij' : c'.Rel i' (e.f j)),
  Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology (e.f j))
    (ShortComplex.ShortExact.δ sorry i' (e.f j) hij') 0
Tactic: obtain ⟨j, rfl⟩ := hj
Cleared hypotheses: j', hij', hj
-- 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 : ι
hij' : c'.Rel i' (e.f j)
⊢ Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ (K.shortComplexTruncLE e).X₁.homology (e.f j))
    (ShortComplex.ShortExact.δ ⋯ i' (e.f j) hij') 0
have pos : Eq (α := (K.shortComplexTruncLE e).X₃.homology i' ⟶ K.homology (e.f j))
  (ShortComplex.ShortExact.δ sorry i' (e.f j) hij' ≫ homologyMap (K.ιTruncLE e) (e.f j)) 0
Tactic: rw [← cancel_mono (homologyMap (K.ιTruncLE e) (e.f j)), zero_comp]
-- 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' : ι'
⊢ Epi (X := (K.shortComplexTruncLE e).X₂.homology i') (Y := (K.shortComplexTruncLE e).X₃.homology i')
    (homologyMap (K.shortComplexTruncLE e).g i')
have 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')
Tactic: by_cases hi' : ∃ j', c'.Rel i' j'