awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
⊢ f = g
have hfg : ∀ (i : I₁ × I₂) (hij : c₁.π c₂ c₁₂ i = i₁₂),
  K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ f = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ g
Tactic: apply GradedObject.mapObj_ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂)
have pos : ∀ (h : c₁.Rel i₁ (c₁.next i₁)),
  Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂)
Tactic: by_cases h : c₁.Rel i₁ (c₁.next i₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
pos :
  ∀ (h : c₁.Rel i₁ (c₁.next i₁)),
    Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
      (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂)
        (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
      ((φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂)
⊢ Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂)
have neg : ∀ (h : ¬c₁.Rel i₁ (c₁.next i₁)),
  Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₁ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂)
Tactic: by_cases h : c₁.Rel i₁ (c₁.next i₁)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂)
have pos : ∀ (h : c₂.Rel i₂ (c₂.next i₂)),
  Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂)
Tactic: by_cases h : c₂.Rel i₂ (c₂.next i₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
pos :
  ∀ (h : c₂.Rel i₂ (c₂.next i₂)),
    Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
      (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂)
        (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
      ((φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂)
⊢ Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂)
have neg : ∀ (h : ¬c₂.Rel i₂ (c₂.next i₂)),
  Eq (α := (K.X i₁).X i₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂)
    (CategoryStruct.comp (Y := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂) (K.d₂ c₁₂ i₁ i₂ i₁₂)
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂)
Tactic: by_cases h : c₂.Rel i₂ (c₂.next i₂)
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ (L.total c₁₂).d i₁₂ i₁₂' =
    (K.total c₁₂).d i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
have dsimp : GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫
    HAdd.hAdd (α := L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (L.D₁ c₁₂ i₁₂ i₁₂') (L.D₂ c₁₂ i₁₂ i₁₂') =
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
    GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
Tactic: dsimp [total]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫
      HAdd.hAdd (α := L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (L.D₁ c₁₂ i₁₂ i₁₂') (L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
have rw : HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
    (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
    GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
Tactic: rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h : c₁₂.Rel i₁₂ i₁₂'
rw :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫
      HAdd.hAdd (α := L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (L.D₁ c₁₂ i₁₂ i₁₂') (L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
have rw₁ : HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
    (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
Tactic: rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h : c₁₂.Rel i₁₂ i₁₂'
rw :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
rw₁ :
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂')
      (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
      (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
      (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫
      HAdd.hAdd (α := L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (L.D₁ c₁₂ i₁₂ i₁₂') (L.D₂ c₁₂ i₁₂ i₁₂') =
    HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
        (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₂ c₁₂ i₁₂ i₁₂') ≫
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
have rw₂ : HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
    (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂') =
  HAdd.hAdd (α := K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂ ⟶ L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂')
    (K.D₁ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
    (K.D₂ c₁₂ i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂')
Tactic: rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
⊢ map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)
have a : Eq (α :=
  Functor.obj (HomologicalComplex.forget C c₁₂) (K.total c₁₂) ⟶
    Functor.obj (HomologicalComplex.forget C c₁₂) (K.total c₁₂))
  (CategoryTheory.Functor.map (HomologicalComplex.forget C c₁₂) (map (𝟙 K) c₁₂))
  (CategoryTheory.Functor.map (HomologicalComplex.forget C c₁₂) (𝟙 (K.total c₁₂)))
Tactic: apply (HomologicalComplex.forget _ _).map_injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
⊢ Eq (α := K.total c₁₂ ⟶ M.total c₁₂) (map (φ ≫ ψ) c₁₂) (CategoryStruct.comp (Y := L.total c₁₂) (map φ c₁₂) (map ψ c₁₂))
have a : Eq (α :=
  Functor.obj (HomologicalComplex.forget C c₁₂) (K.total c₁₂) ⟶
    Functor.obj (HomologicalComplex.forget C c₁₂) (M.total c₁₂))
  (CategoryTheory.Functor.map (HomologicalComplex.forget C c₁₂) (map (φ ≫ ψ) c₁₂))
  (CategoryTheory.Functor.map (HomologicalComplex.forget C c₁₂)
    (CategoryStruct.comp (Y := L.total c₁₂) (map φ c₁₂) (map ψ c₁₂)))
Tactic: apply (HomologicalComplex.forget _ _).map_injective
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
⊢ CategoryStruct.comp (Y := L.total c₁₂) (map e.hom c₁₂) (map e.inv c₁₂) = 𝟙 (K.total c₁₂)
have rw : map (e.hom ≫ e.inv) c₁₂ = 𝟙 (K.total c₁₂)
Tactic: rw [← map_comp, e.hom_inv_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
rw : map (e.hom ≫ e.inv) c₁₂ = 𝟙 (K.total c₁₂)
⊢ CategoryStruct.comp (Y := L.total c₁₂) (map e.hom c₁₂) (map e.inv c₁₂) = 𝟙 (K.total c₁₂)
have rw₁ : map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)
Tactic: rw [← map_comp, e.hom_inv_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
rw : map (e.hom ≫ e.inv) c₁₂ = 𝟙 (K.total c₁₂)
rw₁ : map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)
⊢ CategoryStruct.comp (Y := L.total c₁₂) (map e.hom c₁₂) (map e.inv c₁₂) = 𝟙 (K.total c₁₂)
have rw₂ : 𝟙 (K.total c₁₂) = 𝟙 (K.total c₁₂)
Tactic: rw [← map_comp, e.hom_inv_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
⊢ CategoryStruct.comp (Y := K.total c₁₂) (map e.inv c₁₂) (map e.hom c₁₂) = 𝟙 (L.total c₁₂)
have rw : map (e.inv ≫ e.hom) c₁₂ = 𝟙 (L.total c₁₂)
Tactic: rw [← map_comp, e.inv_hom_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
rw : map (e.inv ≫ e.hom) c₁₂ = 𝟙 (L.total c₁₂)
⊢ CategoryStruct.comp (Y := K.total c₁₂) (map e.inv c₁₂) (map e.hom c₁₂) = 𝟙 (L.total c₁₂)
have rw₁ : map (𝟙 L) c₁₂ = 𝟙 (L.total c₁₂)
Tactic: rw [← map_comp, e.inv_hom_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst_2 : TotalComplexShape c₁ c₂ c₁₂
inst_3 : DecidableEq I₁₂
inst_4 : K.HasTotal c₁₂
inst_5 : L.HasTotal c₁₂
inst_6 : M.HasTotal c₁₂
rw : map (e.inv ≫ e.hom) c₁₂ = 𝟙 (L.total c₁₂)
rw₁ : map (𝟙 L) c₁₂ = 𝟙 (L.total c₁₂)
⊢ CategoryStruct.comp (Y := K.total c₁₂) (map e.inv c₁₂) (map e.hom c₁₂) = 𝟙 (L.total c₁₂)
have rw₂ : 𝟙 (L.total c₁₂) = 𝟙 (L.total c₁₂)
Tactic: rw [← map_comp, e.inv_hom_id, map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
a x a' : ℤ
h : a' = a + x
b : ℤ
⊢ ((Functor.obj (shiftFunctor₁ C x) K).X a).X b = (K.X a').X b
have subst : ((Functor.obj (shiftFunctor₁ C x) K).X a).X b = (K.X (a + x)).X b
Tactic: subst h
Cleared hypotheses: a', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
a b y b' : ℤ
h : b' = b + y
⊢ ((Functor.obj (shiftFunctor₂ C y) K).X a).X b = (K.X a).X b'
have subst : ((Functor.obj (shiftFunctor₂ C y) K).X a).X b = (K.X a).X (b + y)
Tactic: subst h
Cleared hypotheses: b', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (a + x, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
have h₁ : a + b = n
Tactic: simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n : ℤ
x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)
a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (a - x, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
have h₁ : a + b = n + x
Tactic: simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.TotalComplexShift (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst_2 : K.HasTotal (up ℤ)
n a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
        (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type))
            x_1 with
          | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) ⋯ :
          (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
      ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
          (match (motive := (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type))
              x_1 with
            | ⟨(a, b), h⟩ =>
              Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) ⋯ :
            (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
        (Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h)) =
    Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h
have a₁ : (↑((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) ↦
            (match (motive :=
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) x_1 with
              | ⟨(a, b), h⟩ => Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a - x, b) sorry :
              (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)))
          ((fun (x_1 : (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type)) ↦
              (match (motive :=
                  (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) : Type) → (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)) x_1 with
                | ⟨(a, b), h⟩ =>
                  Subtype.mk (p := fun (x_2 : ℤ × ℤ) ↦ x_2 ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) (a + x, b) sorry :
                (↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}) : Type)))
            (Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h))) :
      ℤ × ℤ).1 =
  (↑(Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h) : ℤ × ℤ).1
Tactic: ext