awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x x_1 : (↑s.1 : Type v)
simp :
  Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
      (HAdd.hAdd (α := Cochain K L n) (β := Cochain K L n)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x :
          Cochain K L n)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x_1 :
          Cochain K L n))
      ⋯ =
    HAdd.hAdd (α := Cocycle K L n) (β := Cocycle K L n)
      (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x)
          ⋯ :
        ↥(cocycle K L n))
      (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x_1)
          ⋯ :
        ↥(cocycle K L n))
⊢ Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) s.ι :
          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
        (x + x_1))
      ⋯ =
    HAdd.hAdd (α := Cocycle K L n) (β := Cocycle K L n)
      (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
            x)
          ⋯ :
        ↥(cocycle K L n))
      (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
            x_1)
          ⋯ :
        ↥(cocycle K L n))

Tactic:
simp +instances only [HomComplex_X, map_add]

Premises used: map_add, CochainComplex.HomComplex_X
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x x_1 : (↑s.1 : Type v)
⊢ Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
      (HAdd.hAdd (α := Cochain K L n) (β := Cochain K L n)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x :
          Cochain K L n)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x_1 :
          Cochain K L n))
      ⋯ =
    HAdd.hAdd (α := Cocycle K L n) (β := Cocycle K L n)
      (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x)
          ⋯ :
        ↥(cocycle K L n))
      (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) s.ι :
              (a : (↑s.pt : Type v)) → Cochain K L n)
            x_1)
          ⋯ :
        ↥(cocycle K L n))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (s : Fork ((K.HomComplex L).d n m) 0),
    (fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
            (AddCommGrpCat.ofHom
                {
                  toFun := fun (x : (↑s.1 : Type v)) ↦
                    Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                            (CC := AddCommGrpCat.carrier) s.ι :
                          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
                        x)
                      ⋯,
                  map_zero' := ⋯, map_add' := ⋯ } :
              AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
          s ≫
        Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) =
      s.ι
⊢ ∀ (s : Fork ((K.HomComplex L).d n m) 0),
    (fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
            (AddCommGrpCat.ofHom
                {
                  toFun := fun (x : (↑s.1 : Type v)) ↦
                    Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
                      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                            (CC := AddCommGrpCat.carrier) s.ι :
                          (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
                        x)
                      ⋯,
                  map_zero' := ⋯, map_add' := ⋯ } :
              AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
          s ≫
        Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) =
      s.ι

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
hf :
  ∀ (x : (↑s.pt : Type v)),
    Eq (α := (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
      ((AddCommGrpCat.Hom.hom l :
            (a : (↑s.pt : Type v)) →
              (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
          x :
        (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
      ((AddCommGrpCat.Hom.hom
              ((fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
                  (AddCommGrpCat.ofHom
                      {
                        toFun := fun (x : (↑s.1 : Type v)) ↦
                          Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
                            ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                                  (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier) s.ι :
                                (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
                              x)
                            ⋯,
                        map_zero' := ⋯, map_add' := ⋯ } :
                    AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
                s) :
            (a : (↑s.pt : Type v)) →
              (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
          x :
        (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
⊢ l =
    (fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
        (AddCommGrpCat.ofHom
            {
              toFun := fun (x : (↑s.1 : Type v)) ↦
                Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                        (CC := AddCommGrpCat.carrier) s.ι :
                      (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
                    x)
                  ⋯,
              map_zero' := ⋯, map_add' := ⋯ } :
          AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
      s

Tactic:
ext : 3
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
l : s.pt ⟶ (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt
hl : l ≫ Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) = s.ι
x : (↑s.pt : Type v)
⊢ Eq (α := (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
    ((AddCommGrpCat.Hom.hom l :
          (a : (↑s.pt : Type v)) →
            (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
        x :
      (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
    ((AddCommGrpCat.Hom.hom
            ((fun (s : Fork ((K.HomComplex L).d n m) 0) ↦
                (AddCommGrpCat.ofHom
                    {
                      toFun := fun (x : (↑s.1 : Type v)) ↦
                        Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n)
                          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                                (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier) s.ι :
                              (a : (↑s.pt : Type v)) → (↑((K.HomComplex L).X n) : Type v))
                            x)
                          ⋯,
                      map_zero' := ⋯, map_add' := ⋯ } :
                  AddCommGrpCat.of (↑s.1 : Type v) ⟶ AddCommGrpCat.of (Cocycle K L n)))
              s) :
          (a : (↑s.pt : Type v)) →
            (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))
        x :
      (↑(KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯).pt : Type v))

Tactic:
simp [← hl]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
pos : ∀ (hnm : n + 1 = m), δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯
neg : ∀ (hnm : ¬n + 1 = m), δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯
⊢ δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯

Tactic:
by_cases hnm : n + 1 = m
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : n + 1 = m
⊢ δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯

Tactic:
simp [δ_comp_zero_cochain _ _ _ hnm]

Premises used: CochainComplex.HomComplex.δ_comp_zero_cochain
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
z₂ : Cocycle G K 0
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m (z₁.comp (↑z₂ : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑z₂ : Cochain G K 0) ⋯

Tactic:
simp [δ_shape _ _ hnm]

Premises used: CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cochain F G n
f : G ⟶ K
m : ℤ
rw : δ n m (z₁.comp (↑(Cocycle.ofHom f) : Cochain G K 0) ⋯) = (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) ⋯
rw₁ rw₂ :
  (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) ⋯ = (δ n m z₁).comp (↑(Cocycle.ofHom f) : Cochain G K 0) ⋯
⊢ δ n m (z₁.comp (Cochain.ofHom f) ⋯) = (δ n m z₁).comp (Cochain.ofHom f) ⋯

Tactic:
rw [← Cocycle.ofHom_coe, δ_comp_zero_cocycle]

Premises used: CochainComplex.HomComplex.Cocycle.ofHom_coe, CochainComplex.HomComplex.δ_comp_zero_cocycle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
pos : ∀ (hnm : n + 1 = m), δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯
neg : ∀ (hnm : ¬n + 1 = m), δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯
⊢ δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯

Tactic:
by_cases hnm : n + 1 = m
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : n + 1 = m
⊢ δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯

Tactic:
simp [δ_zero_cochain_comp _ _ _ hnm]

Premises used: CochainComplex.HomComplex.δ_zero_cochain_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
z₁ : Cocycle F G 0
z₂ : Cochain G K n
m : ℤ
hnm : ¬n + 1 = m
⊢ δ n m ((↑z₁ : Cochain F G 0).comp z₂ ⋯) = (↑z₁ : Cochain F G 0).comp (δ n m z₂) ⋯

Tactic:
simp [δ_shape _ _ hnm]

Premises used: CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
F G K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : F ⟶ G
z : Cochain G K n
m : ℤ
rw : δ n m ((↑(Cocycle.ofHom f) : Cochain F G 0).comp z ⋯) = (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) ⋯
rw₁ rw₂ : (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) ⋯ = (↑(Cocycle.ofHom f) : Cochain F G 0).comp (δ n m z) ⋯
⊢ δ n m ((Cochain.ofHom f).comp z ⋯) = (Cochain.ofHom f).comp (δ n m z) ⋯

Tactic:
rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]

Premises used: CochainComplex.HomComplex.Cocycle.ofHom_coe, CochainComplex.HomComplex.δ_zero_cocycle_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n_1 m n : ℤ
z : Cocycle G K n
f : F ⟶ G
⊢ Eq (α := Cochain F K (n + 1)) (δ n (n + 1) ((Cochain.ofHom f).comp (↑z : Cochain G K n) ⋯)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n_1 m n : ℤ
z : Cocycle F G n
f : G ⟶ K
⊢ Eq (α := Cochain F K (n + 1)) (δ n (n + 1) ((↑z : Cochain F G n).comp (Cochain.ofHom f) ⋯)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
⊢ ofHom φ₁ = δ (-1) 0 (ofHomotopy ho) + ofHom φ₂

Tactic:
simp only [δ_ofHomotopy, sub_add_cancel]

Premises used: sub_add_cancel, CochainComplex.HomComplex.δ_ofHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
i j : ℤ
hij : j + 1 ≠ i
h : i + -1 = j
⊢ j + 1 = i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
⊢ (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯

Tactic:
have eq := Cochain.congr_v z.2 p p (add_zero p)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
⊢ (ComplexShape.up ℤ).Rel (p - 1) p

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
⊢ (ComplexShape.up ℤ).Rel (p - 1) p

Tactic:
have h₁ : (ComplexShape.up ℤ).Rel (p - 1) p := by simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
⊢ (ComplexShape.up ℤ).Rel p (p + 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
⊢ (ComplexShape.up ℤ).Rel p (p + 1)

Tactic:
have h₂ : (ComplexShape.up ℤ).Rel p (p + 1) := by simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
⊢ φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p

Tactic:
simp only [δ_neg_one_cochain, Cochain.ofHom_v, ComplexShape.up_Rel, Cochain.add_v,
          Homotopy.nullHomotopicMap'_f h₁ h₂] at eq

Premises used: ComplexShape.up_Rel, CochainComplex.HomComplex.Cochain.ofHom_v, Homotopy.nullHomotopicMap'_f, CochainComplex.HomComplex.δ_neg_one_cochain, CochainComplex.HomComplex.Cochain.add_v
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
hom :
  ∀ (i j : ℤ),
    Homotopy.hom (f := φ₁) (g := φ₂)
        ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
            ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
                comm := ⋯ } :
              Homotopy φ₁ φ₂))
          ((fun (ho : Homotopy φ₁ φ₂) ↦
              (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
                { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
            ho))
        i j =
      ho.hom i j
⊢ (fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
        ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
            comm := ⋯ } :
          Homotopy φ₁ φ₂))
      ((fun (ho : Homotopy φ₁ φ₂) ↦
          (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
            { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
        ho) =
    ho

Tactic:
ext i j
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
hom : (if hij : i + -1 = j then (ofHomotopy ho).v i j hij else 0) = ho.hom i j
⊢ Homotopy.hom (f := φ₁) (g := φ₂)
      ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
          ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
              comm := ⋯ } :
            Homotopy φ₁ φ₂))
        ((fun (ho : Homotopy φ₁ φ₂) ↦
            (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
              { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
          ho))
      i j =
    ho.hom i j

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
pos : ∀ (h : i + -1 = j), (ofHomotopy ho).v i j h = ho.hom i j
neg : ∀ (h : ¬i + -1 = j), 0 = ho.hom i j
⊢ (if hij : i + -1 = j then (ofHomotopy ho).v i j hij else 0) = ho.hom i j

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : i + -1 = j
⊢ (ofHomotopy ho).v i j h = ho.hom i j

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
h' : j + 1 = i
⊢ i + -1 = j

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
neg neg₁ : Eq.{v + 1} (α := F.X i ⟶ G.X j) 0 0
⊢ 0 = ho.hom i j

Tactic:
rw [ho.zero i j (fun h' => h (by dsimp at h'; lia))]

Premises used: Homotopy.zero