awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm' = h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯
have 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') sorry).f (Int.negSucc 0))
Tactic: ext (m | _ | m)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm' = h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯
have 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') sorry).f (Int.negSucc (m + 1)))
Tactic: ext (m | _ | m)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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 (α := 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))
have 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))
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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))))
have 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)
Tactic: rw [← cancel_mono (HomologicalComplex.homologyι ..)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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)
have 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) sorry sorry sorry sorry sorry sorry sorry))
        (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) sorry sorry sorry sorry sorry sorry
              sorry)))) ≫
    homologyι h'.cochainComplex m)
Tactic: dsimp [homologyIsoPos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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)
have 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 sorry sorry sorry sorry))
      (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 sorry sorry sorry sorry))))))
Tactic: simp only [homologyι_naturality, Category.assoc, restrictionHomologyIso_hom_homologyι,
    homologyι_naturality_assoc, restrictionHomologyIso_inv_homologyι_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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 ⋯ ⋯ ⋯ ⋯))))))
have 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 sorry sorry sorry sorry))
    (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 sorry sorry sorry sorry))))))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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 ⋯ ⋯ ⋯ ⋯))))))
have 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 sorry sorry sorry sorry))
      (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 sorry sorry sorry sorry)))))))
Tactic: rw [← cancel_epi (HomologicalComplex.pOpcycles ..)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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 ⋯ ⋯ ⋯ ⋯)))))))
have 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 sorry sorry sorry sorry))
        (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 sorry sorry sorry sorry)))))))
Tactic: subst hmn
Cleared hypotheses: m, hmn, inst_3, inst_5
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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))))
have 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)
Tactic: rw [← cancel_mono (HomologicalComplex.homologyι ..)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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)
have 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) sorry sorry sorry sorry sorry sorry
            sorry))
        (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) sorry sorry sorry sorry sorry sorry
              sorry)))) ≫
    homologyι h'.cochainComplex m)
Tactic: dsimp [homologyIsoNeg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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)
have 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 sorry sorry sorry sorry))
      (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 sorry sorry sorry sorry))))))
Tactic: simp only [homologyι_naturality, Category.assoc, restrictionHomologyIso_hom_homologyι,
    homologyι_naturality_assoc, restrictionHomologyIso_inv_homologyι_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (goal)
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
⊢ 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 ⋯ ⋯ ⋯ ⋯))))))
have 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 sorry sorry sorry sorry))
    (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 sorry sorry sorry sorry))))))
Tactic: congr 1