awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
hij : ¬c.Rel i j
neg :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
neg₁ :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op 0) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
⊢ Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)
have neg₂ : Eq (α := op (K.X j) ⟶ K.op.cycles i)
  (CategoryStruct.comp (Y := op (K.opcycles i)) 0 (Iso.inv (K.cyclesOpIso i)) : op (K.X j) ⟶ K.op.cycles i)
  (0 : K.op.X j ⟶ K.op.cycles i)
Tactic: rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
ι : Type u_1
V : Type u_2
inst : Category.{v_1, u_2} V
c : ComplexShape ι
inst_1 : HasZeroMorphisms.{v_1, u_2} V
K : HomologicalComplex.{v_1, u_2, u_1} V c
i : ι
inst_2 : K.HasHomology i
j : ι
hij : ¬c.Rel i j
neg :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
neg₁ :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op 0) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
neg₂ :
  Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) 0 (Iso.inv (K.cyclesOpIso i)) : op (K.X j) ⟶ K.op.cycles i)
    (0 : K.op.X j ⟶ K.op.cycles i)
⊢ Eq (α := op (K.X j) ⟶ K.op.cycles i)
    (CategoryStruct.comp (Y := op (K.opcycles i)) (Quiver.Hom.op (K.fromOpcycles i j)) (Iso.inv (K.cyclesOpIso i)) :
      op (K.X j) ⟶ K.op.cycles i)
    (K.op.toCycles j i : K.op.X j ⟶ K.op.cycles i)
have neg₃ : Eq.{v_1 + 1} (α := op (K.X j) ⟶ K.op.cycles i) 0 0
Tactic: rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ Quiver.Hom.unop (Hom.f (CategoryTheory.Functor.map (opFunctor V c) φ₁.op) n) =
    (HAdd.hAdd (α :=
          (Functor.obj (opFunctor V c) (Opposite.op G)).X n ⟶ (Functor.obj (opFunctor V c) (Opposite.op F)).X n)
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := Functor.obj (opFunctor V c) (Opposite.op G)) (D :=
                  Functor.obj (opFunctor V c) (Opposite.op F)) n :
                ((i j : ι) →
                    (Functor.obj (opFunctor V c) (Opposite.op G)).X i ⟶
                      (Functor.obj (opFunctor V c) (Opposite.op F)).X j) →+
                  ((Functor.obj (opFunctor V c) (Opposite.op G)).X n ⟶
                    (Functor.obj (opFunctor V c) (Opposite.op F)).X n)) :
              (a : (i j : ι) → ((opFunctor V c).obj (Opposite.op G)).X i ⟶ ((opFunctor V c).obj (Opposite.op F)).X j) →
                ((opFunctor V c).obj (Opposite.op G)).X n ⟶ ((opFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := Functor.obj (opFunctor V c) (Opposite.op G)) (D :=
                  Functor.obj (opFunctor V c) (Opposite.op F)) n :
                ((i j : ι) →
                    (Functor.obj (opFunctor V c) (Opposite.op G)).X i ⟶
                      (Functor.obj (opFunctor V c) (Opposite.op F)).X j) →+
                  ((Functor.obj (opFunctor V c) (Opposite.op G)).X n ⟶
                    (Functor.obj (opFunctor V c) (Opposite.op F)).X n)) :
              (a : (i j : ι) → ((opFunctor V c).obj (Opposite.op G)).X i ⟶ ((opFunctor V c).obj (Opposite.op F)).X j) →
                ((opFunctor V c).obj (Opposite.op G)).X n ⟶ ((opFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).op) +
        Hom.f (CategoryTheory.Functor.map (opFunctor V c) φ₂.op) n).unop
have dsimp : φ₁.f n =
  (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
              ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
            (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          fun (i j : ι) ↦ (h.hom j i).op)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
              ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
            (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          fun (i j : ι) ↦ (h.hom j i).op) +
      (φ₂.f n).op).unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ φ₁.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop
have rw : HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
      ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
      ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
    φ₂.f n =
  (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
              ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
            (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          fun (i j : ι) ↦ (h.hom j i).op)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
              ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
            (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          fun (i j : ι) ↦ (h.hom j i).op) +
      (φ₂.f n).op).unop
Tactic: rw [h.comm n]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
        ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op)
          (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
                ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
              (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
            fun (i j : ι) ↦ (h.hom j i).op) +
        (φ₂.f n).op).unop
have nth_rw : HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
      ((prevD n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n)
      ((dNext n : (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n) h.hom : F.X n ⟶ G.X n) +
    φ₂.f n =
  (HAdd.hAdd (α := Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
              ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
            (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          fun (i j : ι) ↦ (h.hom j i).op)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c.symm) (C := G.op) (D := F.op) n :
              ((i j : ι) → G.op.X i ⟶ F.op.X j) →+ (G.op.X n ⟶ F.op.X n)) :
            (a : (i j : ι) → Opposite.op (G.X i) ⟶ Opposite.op (F.X j)) → Opposite.op (G.X n) ⟶ Opposite.op (F.X n))
          fun (i j : ι) ↦ (h.hom j i).op) +
      (φ₂.f n).op).unop
Tactic: nth_rw 2 [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
⊢ Quiver.Hom.op (Hom.f (CategoryTheory.Functor.map (unopFunctor V c) φ₁.op) n) =
    (HAdd.hAdd (α :=
          (Functor.obj (unopFunctor V c) (Opposite.op G)).X n ⟶ (Functor.obj (unopFunctor V c) (Opposite.op F)).X n)
          ((dNext n :
              (a :
                  (i j : ι) →
                    ((unopFunctor V c).obj (Opposite.op G)).X i ⟶ ((unopFunctor V c).obj (Opposite.op F)).X j) →
                ((unopFunctor V c).obj (Opposite.op G)).X n ⟶ ((unopFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).unop)
          ((prevD n :
              (a :
                  (i j : ι) →
                    ((unopFunctor V c).obj (Opposite.op G)).X i ⟶ ((unopFunctor V c).obj (Opposite.op F)).X j) →
                ((unopFunctor V c).obj (Opposite.op G)).X n ⟶ ((unopFunctor V c).obj (Opposite.op F)).X n)
            fun (i j : ι) ↦ (h.hom j i).unop) +
        Hom.f (CategoryTheory.Functor.map (unopFunctor V c) φ₂.op) n).op
have dsimp : φ₁.f n =
  (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
        (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
            (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
              Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          fun (i j : ι) ↦ (h.hom j i).unop)
        (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
            (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
              Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          fun (i j : ι) ↦ (h.hom j i).unop) +
      (φ₂.f n).unop).op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
⊢ φ₁.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op
have rw : HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
      (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
              ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
            (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
          h.hom :
        F.X n ⟶ G.X n)
      (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
              ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
            (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
          h.hom :
        F.X n ⟶ G.X n) +
    φ₂.f n =
  (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
        (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
            (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
              Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          fun (i j : ι) ↦ (h.hom j i).unop)
        (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
            (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
              Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          fun (i j : ι) ↦ (h.hom j i).unop) +
      (φ₂.f n).unop).op
Tactic: rw [h.comm n]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Opposite (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst_1 : Preadditive.{v_1, u_1} V
F G : HomologicalComplex.{v_1, u_1, u_2} Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy.{v_1, u_1, u_2} (ι := ι) (V := Vᵒᵖ) (c := c) (C := F) (D := G) φ₁ φ₂
n : ι
⊢ HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
        (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n)
        (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
                ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
              (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
            h.hom :
          F.X n ⟶ G.X n) +
      φ₂.f n =
    (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop)
          (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
              (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
                Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
            fun (i j : ι) ↦ (h.hom j i).unop) +
        (φ₂.f n).unop).op
have nth_rw : HAdd.hAdd (α := F.X n ⟶ G.X n) (β := F.X n ⟶ G.X n)
      (((prevD.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
              ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
            (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
          h.hom :
        F.X n ⟶ G.X n)
      (((dNext.{v_1, u_1, u_2} (V := Vᵒᵖ) (c := c) (C := F) (D := G) n :
              ((i j : ι) → F.X i ⟶ G.X j) →+ (F.X n ⟶ G.X n)) :
            (a : (i j : ι) → F.X i ⟶ G.X j) → F.X n ⟶ G.X n)
          h.hom :
        F.X n ⟶ G.X n) +
    φ₂.f n =
  (HAdd.hAdd (α := Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
        (((dNext n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
            (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
              Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          fun (i j : ι) ↦ (h.hom j i).unop)
        (((prevD n : ((i j : ι) → G.unop.X i ⟶ F.unop.X j) →+ (G.unop.X n ⟶ F.unop.X n)) :
            (a : (i j : ι) → Opposite.unop (G.X i) ⟶ Opposite.unop (F.X j)) →
              Opposite.unop (G.X n) ⟶ Opposite.unop (F.X n))
          fun (i j : ι) ↦ (h.hom j i).unop) +
      (φ₂.f n).unop).op
Tactic: nth_rw 2 [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ QuasiIsoAt f i ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
have mp : QuasiIsoAt f i →
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
mp :
  QuasiIsoAt f i →
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
⊢ QuasiIsoAt f i ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
have mpr : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f) →
  QuasiIsoAt f i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L M K' L' : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
inst_2 : IsIso f
i : ι
inst_3 : K.HasHomology i
inst_4 : L.HasHomology i
⊢ QuasiIsoAt f i
have rw : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
  (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
Tactic: rw [quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : L.HasHomology j
inst_4 : (K.sc' i j k).HasHomology
inst_5 : (L.sc' i j k).HasHomology
⊢ QuasiIsoAt f j ↔
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C c i j k) K)
      (CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) f)
have rw : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c j) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c j) f) ↔
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor' C c i j k) K)
    (CategoryTheory.Functor.map (shortComplexFunctor' C c i j k) f)
Tactic: rw [quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L K' L' : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : K'.HasHomology i
inst_5 : L'.HasHomology i
hf' : QuasiIsoAt f' i
⊢ QuasiIsoAt f i
have rw : ∀
  (hf' :
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K')
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) f')),
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c i) K)
    (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)
Tactic: rw [quasiIsoAt_iff] at hf' ⊢
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ QuasiIsoAt f i ↔ IsIso (X := K.homology i) (Y := L.homology i) (homologyMap f i)
have rw : IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
  IsIso (X := K.homology i) (Y := L.homology i) (homologyMap f i)
Tactic: rw [quasiIsoAt_iff, ShortComplex.quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : K.ExactAt i
⊢ QuasiIsoAt f i ↔ L.ExactAt i
have simp : ∀ (hK : IsZero.{v, u} (K.sc i).homology),
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (L.sc i).homology
Tactic: simp only [quasiIsoAt_iff, ShortComplex.quasiIso_iff, exactAt_iff,
    ShortComplex.exact_iff_isZero_homology] at hK ⊢
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (L.sc i).homology
have mp : IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) →
  IsZero.{v, u} (L.sc i).homology
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.QuasiIso (goal)
Goal:
ι : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
c : ComplexShape ι
K L : HomologicalComplex.{v, u, u_1} C c
f : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
hK : IsZero.{v, u} (K.sc i).homology
mp :
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) →
    IsZero.{v, u} (L.sc i).homology
⊢ IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
      (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f)) ↔
    IsZero.{v, u} (L.sc i).homology
have mpr : IsZero.{v, u} (L.sc i).homology →
  IsIso (X := (Functor.obj (shortComplexFunctor C c i) K).homology) (Y :=
    (Functor.obj (shortComplexFunctor C c i) L).homology)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) f))
Tactic: constructor