awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = (↑n : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology L' n
e_a :
  ∀ [inst_7 : HasHomology h.cochainComplex (↑n : ℤ)] [inst_8 : HasHomology h'.cochainComplex (↑n : ℤ)],
    Eq (α := h.cochainComplex.X (↑n : ℤ) ⟶ opcycles h'.cochainComplex (↑n : ℤ))
      (CategoryStruct.comp (Y := opcycles h.cochainComplex (↑n : ℤ)) (pOpcycles h.cochainComplex (↑n : ℤ))
        (opcyclesMap (h.map h' fK fL f_comm) (↑n : ℤ)))
      (CategoryStruct.comp (Y := opcycles h.cochainComplex (↑n : ℤ)) (pOpcycles h.cochainComplex (↑n : ℤ))
        (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).opcycles n)
          (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯))
          (CategoryStruct.comp (Y := opcycles L n) (opcyclesMap h.restrictionGEIso.hom n)
            (CategoryStruct.comp (Y := opcycles L' n) (opcyclesMap fL n)
              (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntGE 0)).opcycles n)
                (opcyclesMap h'.restrictionGEIso.inv n)
                (Iso.hom
                  (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯)))))))
⊢ Eq (α := h.cochainComplex.X m ⟶ opcycles h'.cochainComplex m)
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (opcyclesMap (h.map h' fK fL f_comm) m))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles L n) (opcyclesMap h.restrictionGEIso.hom n)
          (CategoryStruct.comp (Y := opcycles L' n) (opcyclesMap fL n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntGE 0)).opcycles n)
              (opcyclesMap h'.restrictionGEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯)))))))

Tactic:
subst hmn
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
inst_3 : HasHomology L n
inst_4 : HasHomology L' n
inst_5 : HasHomology h.cochainComplex (↑n : ℤ)
inst_6 : HasHomology h'.cochainComplex (↑n : ℤ)
⊢ Eq (α := h.cochainComplex.X (↑n : ℤ) ⟶ opcycles h'.cochainComplex (↑n : ℤ))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex (↑n : ℤ)) (pOpcycles h.cochainComplex (↑n : ℤ))
      (opcyclesMap (h.map h' fK fL f_comm) (↑n : ℤ)))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex (↑n : ℤ)) (pOpcycles h.cochainComplex (↑n : ℤ))
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles L n) (opcyclesMap h.restrictionGEIso.hom n)
          (CategoryStruct.comp (Y := opcycles L' n) (opcyclesMap fL n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntGE 0)).opcycles n)
              (opcyclesMap h'.restrictionGEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯)))))))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
rw :
  Eq (α := homology h.cochainComplex m ⟶ opcycles h'.cochainComplex m)
    (homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m)
    (CategoryStruct.comp (Y := homology K n) (Iso.hom (h.homologyIsoNeg n m hmn))
        (CategoryStruct.comp (Y := homology K' n) (homologyMap fK n) (Iso.inv (h'.homologyIsoNeg n m hmn))) ≫
      homologyι h'.cochainComplex m)
⊢ Eq (α := homology h.cochainComplex m ⟶ homology h'.cochainComplex m) (homologyMap (h.map h' fK fL f_comm) m)
    (CategoryStruct.comp (Y := homology K n) (Iso.hom (h.homologyIsoNeg n m hmn))
      (CategoryStruct.comp (Y := homology K' n) (homologyMap fK n) (Iso.inv (h'.homologyIsoNeg n m hmn))))

Tactic:
rw [← cancel_mono (HomologicalComplex.homologyι ..)]

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.homologyι
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
dsimp :
  Eq (α := homology h.cochainComplex m ⟶ opcycles h'.cochainComplex m)
    (homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m)
    (CategoryStruct.comp (Y := homology K n)
        (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).homology n)
          (Iso.inv
            (restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              ⋯))
          (homologyMap h.restrictionLEIso.hom n))
        (CategoryStruct.comp (Y := homology K' n) (homologyMap fK n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).homology n)
            (homologyMap h'.restrictionLEIso.inv n)
            (Iso.hom
              (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯ ⋯)))) ≫
      homologyι h'.cochainComplex m)
⊢ Eq (α := homology h.cochainComplex m ⟶ opcycles h'.cochainComplex m)
    (homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m)
    (CategoryStruct.comp (Y := homology K n) (Iso.hom (h.homologyIsoNeg n m hmn))
        (CategoryStruct.comp (Y := homology K' n) (homologyMap fK n) (Iso.inv (h'.homologyIsoNeg n m hmn))) ≫
      homologyι h'.cochainComplex m)

Tactic:
dsimp [homologyIsoNeg]

Premises used: CochainComplex.ConnectData.homologyIsoNeg
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
simp :
  Eq (α := homology h.cochainComplex m ⟶ opcycles h'.cochainComplex m)
    (homologyι h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m)
    (homologyι h.cochainComplex m ≫
      CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))))))
⊢ Eq (α := homology h.cochainComplex m ⟶ opcycles h'.cochainComplex m)
    (homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m)
    (CategoryStruct.comp (Y := homology K n)
        (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).homology n)
          (Iso.inv
            (restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
              ⋯))
          (homologyMap h.restrictionLEIso.hom n))
        (CategoryStruct.comp (Y := homology K' n) (homologyMap fK n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).homology n)
            (homologyMap h'.restrictionLEIso.inv n)
            (Iso.hom
              (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n (n - 1) ⋯ ⋯ ⋯ ⋯ ⋯
                ⋯ ⋯)))) ≫
      homologyι h'.cochainComplex m)

Tactic:
simp only [homologyι_naturality, Category.assoc, restrictionHomologyIso_hom_homologyι,
    homologyι_naturality_assoc, restrictionHomologyIso_inv_homologyι_assoc]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc, HomologicalComplex.restrictionHomologyIso_hom_homologyι, HomologicalComplex.homologyι_naturality, HomologicalComplex.homologyι_naturality_assoc
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
e_a :
  Eq (α := opcycles h.cochainComplex m ⟶ opcycles h'.cochainComplex m) (opcyclesMap (h.map h' fK fL f_comm) m)
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
      (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
      (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
        (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
            (opcyclesMap h'.restrictionLEIso.inv n)
            (Iso.hom
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))))))
⊢ Eq (α := homology h.cochainComplex m ⟶ opcycles h'.cochainComplex m)
    (homologyι h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m)
    (homologyι h.cochainComplex m ≫
      CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))))))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
e_a :
  Eq (α := h.cochainComplex.X m ⟶ opcycles h'.cochainComplex m)
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (opcyclesMap (h.map h' fK fL f_comm) m))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯)))))))
⊢ Eq (α := opcycles h.cochainComplex m ⟶ opcycles h'.cochainComplex m) (opcyclesMap (h.map h' fK fL f_comm) m)
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
      (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
      (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
        (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
            (opcyclesMap h'.restrictionLEIso.inv n)
            (Iso.hom
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))))))

Tactic:
rw [← cancel_epi (HomologicalComplex.pOpcycles ..)]

Premises used: HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
⊢ m = Int.negSucc n

Tactic:
hmn

Premises used: Int.neg, Int.negOfNat
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
m : ℤ
hmn : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology K' n
e_a :
  ∀ [inst_7 : HasHomology h.cochainComplex (Int.negSucc n)] [inst_8 : HasHomology h'.cochainComplex (Int.negSucc n)],
    Eq (α := h.cochainComplex.X (Int.negSucc n) ⟶ opcycles h'.cochainComplex (Int.negSucc n))
      (CategoryStruct.comp (Y := opcycles h.cochainComplex (Int.negSucc n)) (pOpcycles h.cochainComplex (Int.negSucc n))
        (opcyclesMap (h.map h' fK fL f_comm) (Int.negSucc n)))
      (CategoryStruct.comp (Y := opcycles h.cochainComplex (Int.negSucc n)) (pOpcycles h.cochainComplex (Int.negSucc n))
        (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
          (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
          (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
            (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
              (CategoryStruct.comp (Y :=
                (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
                (opcyclesMap h'.restrictionLEIso.inv n)
                (Iso.hom
                  (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯
                    ⋯)))))))
⊢ Eq (α := h.cochainComplex.X m ⟶ opcycles h'.cochainComplex m)
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (opcyclesMap (h.map h' fK fL f_comm) m))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex m) (pOpcycles h.cochainComplex m)
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯)))))))

Tactic:
obtain rfl : m = .negSucc n := hmn

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' : ChainComplex.{v, u, 0} C ℕ
L L' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst_2 : NeZero n
inst_3 : HasHomology K n
inst_4 : HasHomology K' n
inst_5 : HasHomology h.cochainComplex (Int.negSucc n)
inst_6 : HasHomology h'.cochainComplex (Int.negSucc n)
⊢ Eq (α := h.cochainComplex.X (Int.negSucc n) ⟶ opcycles h'.cochainComplex (Int.negSucc n))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex (Int.negSucc n)) (pOpcycles h.cochainComplex (Int.negSucc n))
      (opcyclesMap (h.map h' fK fL f_comm) (Int.negSucc n)))
    (CategoryStruct.comp (Y := opcycles h.cochainComplex (Int.negSucc n)) (pOpcycles h.cochainComplex (Int.negSucc n))
      (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
        (Iso.inv (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯))
        (CategoryStruct.comp (Y := opcycles K n) (opcyclesMap h.restrictionLEIso.hom n)
          (CategoryStruct.comp (Y := opcycles K' n) (opcyclesMap fK n)
            (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).opcycles n)
              (opcyclesMap h'.restrictionLEIso.inv n)
              (Iso.hom
                (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯)))))))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i : Option ι
j : ι
hj : i = some j
subst : X K (some j) = K.X j
⊢ X K i = K.X j

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
j : ι
⊢ X K (some j) = K.X j

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i : Option ι
hi : i = none
subst : IsZero.{v_1, u_3} (X K none)
⊢ IsZero.{v_1, u_3} (X K i)

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
⊢ IsZero.{v_1, u_3} (X K none)

Tactic:
Limits.isZero_zero _

Premises used: CategoryTheory.Limits.isZero_zero, HomologicalComplex.extend.X
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
⊢ IsZero.{v_1, u_3} (X K none)

Tactic:
exact Limits.isZero_zero _

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
hi : i = none
subst : Eq (α := X K none ⟶ X K j) (d K none j) 0
⊢ Eq (α := X K i ⟶ X K j) (d K i j) 0

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
j : Option ι
⊢ Eq (α := X K none ⟶ X K j) (d K none j) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
hj : j = none
subst : Eq (α := X K i ⟶ X K none) (d K i none) 0
⊢ Eq (α := X K i ⟶ X K j) (d K i j) 0

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i : Option ι
none : Eq (α := X K Option.none ⟶ X K Option.none) (d K Option.none Option.none) 0
some : ∀ (val : ι), Eq (α := X K (Option.some val) ⟶ X K Option.none) (d K (Option.some val) Option.none) 0
⊢ Eq (α := X K i ⟶ X K Option.none) (d K i Option.none) 0

Tactic:
cases i
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
⊢ Eq (α := X K none ⟶ X K none) (d K none none) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
val : ι
⊢ Eq (α := X K (some val) ⟶ X K none) (d K (some val) none) 0

Tactic:
rfl