awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.TotalComplex
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
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ f =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ g

Tactic:
exact h i₁ i₂ hi
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂)
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₁₂)
⊢ 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₁)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
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:
simp [totalAux.d₁_eq' _ c₁₂ h]

Premises used: HomologicalComplex₂.totalAux.d₁_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
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:
simp [d₁_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

Premises used: HomologicalComplex₂.d₁_eq_zero
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂)
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₁₂)
⊢ 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₂)

Premises used: ComplexShape.next, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
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:
simp [totalAux.d₂_eq' _ c₁₂ i₁ h]

Premises used: HomologicalComplex₂.totalAux.d₂_eq'
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂'
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₁₂'
⊢ 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₁₂'

Tactic:
dsimp [total]

Premises used: HomologicalComplex₂.total
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
⊢ Eq (α :=
    Functor.obj (HomologicalComplex.forget C c₁₂) (K.total c₁₂) ⟶
      Functor.obj (HomologicalComplex.forget C c₁₂) (L.total c₁₂))
    (CategoryTheory.Functor.map (HomologicalComplex.forget C c₁₂) (map φ c₁₂))
    (GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂))

Tactic:
rfl

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.GradedObject.descMapObj, CategoryTheory.GradedObject.mapMap, rfl
-- Module: Mathlib.Algebra.Homology.TotalComplex
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 :
  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₁₂)))
⊢ map (𝟙 K) c₁₂ = 𝟙 (K.total c₁₂)

Tactic:
apply (HomologicalComplex.forget _ _).map_injective

Premises used: HomologicalComplex.forget, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
⊢ 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 GradedObject.mapMap_id

Premises used: CategoryTheory.GradedObject.mapMap_id
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
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₁₂)))
⊢ Eq (α := K.total c₁₂ ⟶ M.total c₁₂) (map (φ ≫ ψ) c₁₂) (CategoryStruct.comp (Y := L.total c₁₂) (map φ c₁₂) (map ψ c₁₂))

Tactic:
apply (HomologicalComplex.forget _ _).map_injective

Premises used: HomologicalComplex.forget, CategoryTheory.Functor.map_injective
-- Module: Mathlib.Algebra.Homology.TotalComplex
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 (α :=
    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:
GradedObject.mapMap_comp (toGradedObjectMap φ) (toGradedObjectMap ψ) _

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, HomologicalComplex₂.toGradedObject, CategoryTheory.GradedObject.descMapObj, HomologicalComplex₂.toGradedObjectMap, CategoryTheory.GradedObject.mapMap_comp, CategoryTheory.Limits.colimit, CategoryTheory.GradedObject.mapMap, CategoryTheory.GradedObject.mapObj
-- Module: Mathlib.Algebra.Homology.TotalComplex
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 (α :=
    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:
exact GradedObject.mapMap_comp (toGradedObjectMap φ) (toGradedObjectMap ψ) _

Premises used: HomologicalComplex₂.toGradedObjectMap, CategoryTheory.GradedObject.mapMap_comp
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂)
rw₂ rw₃ : 𝟙 (K.total c₁₂) = 𝟙 (K.total c₁₂)
⊢ CategoryStruct.comp (Y := L.total c₁₂) (map e.hom c₁₂) (map e.inv c₁₂) = 𝟙 (K.total c₁₂)

Tactic:
rw [← map_comp, e.hom_inv_id, map_id]

Premises used: CategoryTheory.Iso.hom_inv_id, HomologicalComplex₂.total.map_comp, HomologicalComplex₂.total.map_id
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂)
rw₂ rw₃ : 𝟙 (L.total c₁₂) = 𝟙 (L.total c₁₂)
⊢ CategoryStruct.comp (Y := K.total c₁₂) (map e.inv c₁₂) (map e.hom c₁₂) = 𝟙 (L.total c₁₂)

Tactic:
rw [← map_comp, e.inv_hom_id, map_id]

Premises used: CategoryTheory.Iso.inv_hom_id, HomologicalComplex₂.total.map_comp, HomologicalComplex₂.total.map_id
-- Module: Mathlib.Algebra.Homology.TotalComplex
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₁₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ Eq (α := (K.X i₁).X i₂ ⟶ (L.total c₁₂).X i₁₂)
    (CategoryStruct.comp (Y := (K.total c₁₂).X i₁₂) (K.ιTotal c₁₂ i₁ i₂ i₁₂ h)
      (HomologicalComplex.Hom.f (total.map φ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.ιTotal c₁₂ i₁ i₂ i₁₂ h)

Tactic:
simp [total.map, ιTotal]

Premises used: HomologicalComplex₂.ιTotal, HomologicalComplex₂.total.map
-- Module: Mathlib.Algebra.Homology.TotalComplex
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.total c₁₂).X i₁₂)
    (CategoryStruct.comp (Y := (K.total c₁₂).X i₁₂) (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)
      (HomologicalComplex.Hom.f (total.map φ c₁₂) i₁₂))
    ((φ.f i₁).f i₂ ≫ L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)

Tactic:
simp [total.map, ιTotalOrZero]

Premises used: HomologicalComplex₂.ιTotalOrZero, HomologicalComplex₂.total.map
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 : ℤ
subst : ((Functor.obj (shiftFunctor₁ C x) K).X a).X b = (K.X (a + x)).X b
⊢ ((Functor.obj (shiftFunctor₁ C x) K).X a).X b = (K.X a').X b

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 b : ℤ
⊢ ((Functor.obj (shiftFunctor₁ C x) K).X a).X b = (K.X (a + x)).X b

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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
subst : ((Functor.obj (shiftFunctor₂ C y) K).X a).X b = (K.X a).X (b + y)
⊢ ((Functor.obj (shiftFunctor₂ C y) K).X a).X b = (K.X a).X b'

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 : ℤ
⊢ ((Functor.obj (shiftFunctor₂ C y) K).X a).X b = (K.X a).X (b + y)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
a b x : ℤ
⊢ K.shiftFunctor₁XXIso a x (a + x) ⋯ b = Iso.refl (((Functor.obj (shiftFunctor₁ C x) K).X a).X b)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, HomologicalComplex₂.shiftFunctor₁XXIso, rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : HomologicalComplex₂.{v_1, u_1, 0, 0} C (up ℤ) (up ℤ)
a b y : ℤ
⊢ K.shiftFunctor₂XXIso a b y (b + y) ⋯ = Iso.refl (((Functor.obj (shiftFunctor₂ C y) K).X a).X b)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.eqToIso, CategoryTheory.Iso.refl, HomologicalComplex₂.shiftFunctor₂XXIso, rfl
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 + b = n

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Premises used: Set.mem_singleton_iff, ComplexShape.π_def, Set.mem_preimage
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 = n
⊢ a + x + b = n + x

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 + b = n + x

Tactic:
simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢

Premises used: Set.mem_singleton_iff, ComplexShape.π_def, Set.mem_preimage
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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 = n + x
⊢ a - x + b = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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}
a₁ : a + x - x = 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) ⋯ :
                (↑((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))) :
        ℤ × ℤ).1 =
    (↑(Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h) : ℤ × ℤ).1

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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}
⊢ a + x - x = a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.TotalComplexShift
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))) :
        ℤ × ℤ).2 =
    (↑(Subtype.mk (p := fun (x : ℤ × ℤ) ↦ x ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}) (a, b) h) : ℤ × ℤ).2

Tactic:
rfl