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' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst_2 : HasHomology h.cochainComplex m
inst_3 : NeZero (R := ℕ) 0
hm : m = -(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)
inst_4 : HasHomology K 0
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
this : Ne (α := ℕ) 0 0
⊢ -1 = m + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
m : ℤ
inst_2 : HasHomology h.cochainComplex m
n : ℕ
inst_3 : NeZero (n + 1)
hm : m = -(↑(n + 1 + 1) : ℤ)
inst_4 : HasHomology K (n + 1)
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n + 1)
this : n + 1 ≠ 0
⊢ HSub.hSub (α := ℤ) (-1) (↑n : ℤ) = m + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.up ℤ).prev m = m - 1

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' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.up ℤ).next m = m + 1

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' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ Eq.{v + 1} (α := h.cochainComplex.X (Int.negSucc 0) ⟶ h'.cochainComplex.X (Int.negSucc 0 + 1))
    (CategoryStruct.comp (Y := h'.cochainComplex.X (Int.negSucc 0))
        (match (motive := (x : ℤ) → h.cochainComplex.X x ⟶ h'.cochainComplex.X x) Int.negSucc 0 with
        | Int.ofNat n => fL.f n
        | Int.negSucc n => fK.f n)
        (h'.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1)) :
      h.cochainComplex.X (Int.negSucc 0) ⟶ h'.cochainComplex.X (Int.negSucc 0 + 1))
    (CategoryStruct.comp (Y := h.cochainComplex.X (Int.negSucc 0 + 1))
        (h.cochainComplex.d (Int.negSucc 0) (Int.negSucc 0 + 1))
        (match (motive := (x : ℤ) → h.cochainComplex.X x ⟶ h'.cochainComplex.X x) Int.negSucc 0 + 1 with
        | Int.ofNat n => fL.f n
        | Int.negSucc n => fK.f n) :
      h.cochainComplex.X (Int.negSucc 0) ⟶ h'.cochainComplex.X (Int.negSucc 0 + 1))

Tactic:
simpa
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ Hom.f (𝟙 K) 0 ≫ h.d₀ = h.d₀ ≫ Hom.f (𝟙 L) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h₁ :
  ∀ (m : ℕ),
    Eq (α := h.cochainComplex.X (Int.ofNat m) ⟶ h.cochainComplex.X (Int.ofNat m))
      ((h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.ofNat m)) (Hom.f (𝟙 h.cochainComplex) (Int.ofNat m))
h₂ :
  Eq (α := h.cochainComplex.X (Int.negSucc 0) ⟶ h.cochainComplex.X (Int.negSucc 0))
    ((h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc 0)) (Hom.f (𝟙 h.cochainComplex) (Int.negSucc 0))
h₃ :
  ∀ (m : ℕ),
    Eq (α := h.cochainComplex.X (Int.negSucc (m + 1)) ⟶ h.cochainComplex.X (Int.negSucc (m + 1)))
      ((h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc (m + 1))) (Hom.f (𝟙 h.cochainComplex) (Int.negSucc (m + 1)))
⊢ h.map h (𝟙 K) (𝟙 L) ⋯ = 𝟙 h.cochainComplex

Tactic:
ext (m | _ | m)
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
m : ℕ
⊢ Eq (α := h.cochainComplex.X (Int.ofNat m) ⟶ h.cochainComplex.X (Int.ofNat m))
    ((h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.ofNat m)) (Hom.f (𝟙 h.cochainComplex) (Int.ofNat m))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
h₁ :
  Eq.{v + 1} (α := K.X 0 ⟶ K.X 0)
    (match (motive := (x : ℤ) → X K L x ⟶ X K L x) -1 with
      | Int.ofNat n => 𝟙 (L.X n)
      | Int.negSucc n => 𝟙 (K.X n) :
      X K L (-1) ⟶ X K L (-1))
    (𝟙 (K.X 0) : K.X 0 ⟶ K.X 0)
⊢ Eq (α := h.cochainComplex.X (Int.negSucc 0) ⟶ h.cochainComplex.X (Int.negSucc 0))
    ((h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc 0)) (Hom.f (𝟙 h.cochainComplex) (Int.negSucc 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
m : ℕ
⊢ Eq (α := h.cochainComplex.X (Int.negSucc (m + 1)) ⟶ h.cochainComplex.X (Int.negSucc (m + 1)))
    ((h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc (m + 1))) (Hom.f (𝟙 h.cochainComplex) (Int.negSucc (m + 1)))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
⊢ Eq.{v + 1} (α := K.X 0 ⟶ K.X 0)
    (match (motive := (x : ℤ) → X K L x ⟶ X K L x) -1 with
      | Int.ofNat n => 𝟙 (L.X n)
      | Int.negSucc n => 𝟙 (K.X n) :
      X K L (-1) ⟶ X K L (-1))
    (𝟙 (K.X 0) : K.X 0 ⟶ K.X 0)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (fK ≫ fK').f 0 ≫ h''.d₀ = h.d₀ ≫ (fL ≫ fL').f 0

Tactic:
simp [f_comm', reassoc_of% f_comm]
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
h₁ :
  ∀ (m : ℕ),
    Eq (α := h.cochainComplex.X (Int.ofNat m) ⟶ h''.cochainComplex.X (Int.ofNat m))
      ((h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.ofNat m))
      ((h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.ofNat m))
h₂ :
  Eq (α := h.cochainComplex.X (Int.negSucc 0) ⟶ h''.cochainComplex.X (Int.negSucc 0))
    ((h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc 0))
    ((h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc 0))
h₃ :
  ∀ (m : ℕ),
    Eq (α := h.cochainComplex.X (Int.negSucc (m + 1)) ⟶ h''.cochainComplex.X (Int.negSucc (m + 1)))
      ((h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc (m + 1)))
      ((h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc (m + 1)))
⊢ h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm' = h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯

Tactic:
ext (m | _ | m)
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K K' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ Eq (α := h.cochainComplex.X (Int.ofNat m) ⟶ h''.cochainComplex.X (Int.ofNat m))
    ((h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.ofNat m))
    ((h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.ofNat m))

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' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
h₁ :
  Eq.{v + 1} (α := K.X 0 ⟶ K''.X 0)
    (CategoryStruct.comp (Y := K'.X 0)
        (match (motive := (x : ℤ) → X K L x ⟶ X K' L' x) -1 with
        | Int.ofNat n => fL.f n
        | Int.negSucc n => fK.f n)
        (match (motive := (x : ℤ) → X K' L' x ⟶ X K'' L'' x) -1 with
        | Int.ofNat n => fL'.f n
        | Int.negSucc n => fK'.f n) :
      K.X 0 ⟶ K''.X 0)
    (match (motive := (x : ℤ) → X K L x ⟶ X K'' L'' x) -1 with
      | Int.ofNat n => fL.f n ≫ fL'.f n
      | Int.negSucc n => fK.f n ≫ fK'.f n :
      X K L (-1) ⟶ X K'' L'' (-1))
⊢ Eq (α := h.cochainComplex.X (Int.negSucc 0) ⟶ h''.cochainComplex.X (Int.negSucc 0))
    ((h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc 0))
    ((h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc 0))

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' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ Eq (α := h.cochainComplex.X (Int.negSucc (m + 1)) ⟶ h''.cochainComplex.X (Int.negSucc (m + 1)))
    ((h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc (m + 1)))
    ((h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc (m + 1)))

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' K'' : ChainComplex.{v, u, 0} C ℕ
L L' L'' : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
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
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ Eq.{v + 1} (α := K.X 0 ⟶ K''.X 0)
    (CategoryStruct.comp (Y := K'.X 0)
        (match (motive := (x : ℤ) → X K L x ⟶ X K' L' x) -1 with
        | Int.ofNat n => fL.f n
        | Int.negSucc n => fK.f n)
        (match (motive := (x : ℤ) → X K' L' x ⟶ X K'' L'' x) -1 with
        | Int.ofNat n => fL'.f n
        | Int.negSucc n => fK'.f n) :
      K.X 0 ⟶ K''.X 0)
    (match (motive := (x : ℤ) → X K L x ⟶ X K'' L'' x) -1 with
      | Int.ofNat n => fL.f n ≫ fL'.f n
      | Int.negSucc n => fK.f n ≫ fK'.f n :
      X K L (-1) ⟶ X K'' L'' (-1))

Tactic:
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
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
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 L n) (Iso.hom (h.homologyIsoPos n m hmn))
        (CategoryStruct.comp (Y := homology L' n) (homologyMap fL n) (Iso.inv (h'.homologyIsoPos 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 L n) (Iso.hom (h.homologyIsoPos n m hmn))
      (CategoryStruct.comp (Y := homology L' n) (homologyMap fL n) (Iso.inv (h'.homologyIsoPos 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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology L' 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 L n)
        (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).homology n)
          (Iso.inv
            (restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n (n + 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯))
          (homologyMap h.restrictionGEIso.hom n))
        (CategoryStruct.comp (Y := homology L' n) (homologyMap fL n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntGE 0)).homology n)
            (homologyMap h'.restrictionGEIso.inv n)
            (Iso.hom
              (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (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 L n) (Iso.hom (h.homologyIsoPos n m hmn))
        (CategoryStruct.comp (Y := homology L' n) (homologyMap fL n) (Iso.inv (h'.homologyIsoPos n m hmn))) ≫
      homologyι h'.cochainComplex m)

Tactic:
dsimp [homologyIsoPos]

Premises used: CochainComplex.ConnectData.homologyIsoPos
-- 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
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.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 (α := 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 L n)
        (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).homology n)
          (Iso.inv
            (restrictionHomologyIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n (n + 1) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯))
          (homologyMap h.restrictionGEIso.hom n))
        (CategoryStruct.comp (Y := homology L' n) (homologyMap fL n)
          (CategoryStruct.comp (Y := (restriction h'.cochainComplex (ComplexShape.embeddingUpIntGE 0)).homology n)
            (homologyMap h'.restrictionGEIso.inv n)
            (Iso.hom
              (restrictionHomologyIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology L' 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.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 (α := 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.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:
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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
inst_5 : HasHomology h'.cochainComplex m
inst_6 : HasHomology L' 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.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 (α := opcycles h.cochainComplex m ⟶ opcycles h'.cochainComplex m) (opcyclesMap (h.map h' fK fL f_comm) 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:
rw [← cancel_epi (HomologicalComplex.pOpcycles ..)]

Premises used: HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi