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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ Eq (α := X K L (Int.ofNat n) ⟶ X K L p)
    (CategoryStruct.comp (Y := X K L (Int.ofNat (n + 1))) (h.d (Int.ofNat n) (Int.ofNat (n + 1)))
      (h.d (Int.ofNat (n + 1)) p))
    0
have pos : ∀ (hmp : Int.ofNat (n + 1) + 1 = Int.ofNat (n + 2)),
  Eq (α := X K L (Int.ofNat n) ⟶ X K L (Int.ofNat (n + 2)))
    (CategoryStruct.comp (Y := X K L (Int.ofNat (n + 1))) (h.d (Int.ofNat n) (Int.ofNat (n + 1)))
      (h.d (Int.ofNat (n + 1)) (Int.ofNat (n + 2))))
    0
Tactic: obtain rfl : p = .ofNat (n + 2) := by simp [← hmp]; lia
Cleared hypotheses: p, hmp
-- 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc 0 + 1 = m
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L p) (h.d (Int.negSucc 0) m ≫ h.d m p) 0
have pos : ∀ (hmp : HAdd.hAdd (α := ℤ) 0 1 = p) (hnm : Int.negSucc 0 + 1 = 0),
  Eq (α := X K L (Int.negSucc 0) ⟶ X K L p) (CategoryStruct.comp (Y := X K L 0) (h.d (Int.negSucc 0) 0) (h.d 0 p)) 0
Tactic: obtain rfl : m = 0 := by lia
Cleared hypotheses: m, hmp, hnm
-- 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
p : ℤ
hmp : HAdd.hAdd (α := ℤ) 0 1 = p
hnm : Int.negSucc 0 + 1 = 0
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L p) (CategoryStruct.comp (Y := X K L 0) (h.d (Int.negSucc 0) 0) (h.d 0 p)) 0
have pos : ∀ (hmp : HAdd.hAdd (α := ℤ) 0 1 = 1),
  Eq (α := X K L (Int.negSucc 0) ⟶ X K L 1) (CategoryStruct.comp (Y := X K L 0) (h.d (Int.negSucc 0) 0) (h.d 0 1)) 0
Tactic: obtain rfl : p = 1 := by lia
Cleared hypotheses: p, hmp
-- 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc (HAdd.hAdd (α := ℕ) 0 1) + 1 = m
⊢ Eq (α := X K L (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) ⟶ X K L p)
    (h.d (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) m ≫ h.d m p) 0
have pos : ∀ (hmp : HAdd.hAdd (α := ℤ) (-1) 1 = p) (hnm : Int.negSucc (HAdd.hAdd (α := ℕ) 0 1) + 1 = -1),
  Eq (α := X K L (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) ⟶ X K L p)
    (CategoryStruct.comp (Y := X K L (-1)) (h.d (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) (-1)) (h.d (-1) p)) 0
Tactic: obtain rfl : m = -1 := by lia
Cleared hypotheses: m, hmp, hnm
-- 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
p : ℤ
hmp : HAdd.hAdd (α := ℤ) (-1) 1 = p
hnm : Int.negSucc (HAdd.hAdd (α := ℕ) 0 1) + 1 = -1
⊢ Eq (α := X K L (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) ⟶ X K L p)
    (CategoryStruct.comp (Y := X K L (-1)) (h.d (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) (-1)) (h.d (-1) p)) 0
have pos : ∀ (hmp : HAdd.hAdd (α := ℤ) (-1) 1 = 0),
  Eq (α := X K L (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) ⟶ X K L 0)
    (CategoryStruct.comp (Y := X K L (-1)) (h.d (Int.negSucc (HAdd.hAdd (α := ℕ) 0 1)) (-1)) (h.d (-1) 0)) 0
Tactic: obtain rfl : p = 0 := by lia
Cleared hypotheses: p, hmp
-- 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = m
⊢ Eq (α := X K L (Int.negSucc (n + 1 + 1)) ⟶ X K L p) (h.d (Int.negSucc (n + 1 + 1)) m ≫ h.d m p) 0
have pos : ∀ (hmp : Int.negSucc (n + 1) + 1 = p) (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)),
  Eq (α := X K L (Int.negSucc (n + 1 + 1)) ⟶ X K L p)
    (CategoryStruct.comp (Y := X K L (Int.negSucc (n + 1))) (h.d (Int.negSucc (n + 1 + 1)) (Int.negSucc (n + 1)))
      (h.d (Int.negSucc (n + 1)) p))
    0
Tactic: obtain rfl : m = .negSucc (n + 1) := by lia
Cleared hypotheses: m, hmp, hnm
-- 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.negSucc (n + 1) + 1 = p
hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)
⊢ Eq (α := X K L (Int.negSucc (n + 1 + 1)) ⟶ X K L p)
    (CategoryStruct.comp (Y := X K L (Int.negSucc (n + 1))) (h.d (Int.negSucc (n + 1 + 1)) (Int.negSucc (n + 1)))
      (h.d (Int.negSucc (n + 1)) p))
    0
have pos : ∀ (hmp : Int.negSucc (n + 1) + 1 = Int.negSucc n),
  Eq (α := X K L (Int.negSucc (n + 1 + 1)) ⟶ X K L (Int.negSucc n))
    (CategoryStruct.comp (Y := X K L (Int.negSucc (n + 1))) (h.d (Int.negSucc (n + 1 + 1)) (Int.negSucc (n + 1)))
      (h.d (Int.negSucc (n + 1)) (Int.negSucc n)))
    0
Tactic: obtain rfl : p = .negSucc n := by lia
Cleared hypotheses: p, hmp
-- 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''
n : ℕ
⊢ Eq (α := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X n ⟶ L.X (n + 1))
    (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯) ≫ L.d n (n + 1))
    ((restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).d n (n + 1) ≫
      Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯))
have rw : Eq (α := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X n ⟶ L.X (n + 1))
  (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) sorry) ≫ L.d n (n + 1))
  (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X (n + 1))
    (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) sorry) ≫
      L.d n (n + 1) ≫ Iso.inv (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) sorry))
    (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) sorry)))
Tactic: rw [restriction_d_eq (e := (ComplexShape.embeddingUpIntGE 0)) _ (i' := n)
      (j' := (n + 1 : ℕ)) (by simp) (by simp), cochainComplex_d, h.d_ofNat]
-- 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''
n : ℕ
⊢ Eq (α := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X (n + 1) ⟶ K.X n)
    (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯) ≫ K.d (n + 1) n)
    ((restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d (n + 1) n ≫
      Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯))
have rw : Eq (α := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X (n + 1) ⟶ K.X n)
  (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) sorry) ≫ K.d (n + 1) n)
  (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X n)
    (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) sorry) ≫
      K.d (n + 1) n ≫ Iso.inv (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) sorry))
    (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) sorry)))
Tactic: rw [restriction_d_eq (e := (ComplexShape.embeddingUpIntLE (-1))) _
      (i' := Int.negSucc (n + 1)) (j' := Int.negSucc n) (by dsimp; lia) (by dsimp; lia),
      cochainComplex_d, d_negSucc]
-- 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''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = (↑n : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℕ).prev n = n - 1
have zero : ∀ [NeZero (R := ℕ) 0] (hm : m = (↑0 : ℤ)) [HasHomology L 0]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0),
  (ComplexShape.up ℕ).prev 0 = HSub.hSub (α := ℕ) 0 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this
-- 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''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = (↑n : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
zero :
  ∀ [NeZero (R := ℕ) 0] (hm : m = (↑0 : ℤ)) [HasHomology L 0]
    (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0),
    (ComplexShape.up ℕ).prev 0 = HSub.hSub (α := ℕ) 0 1
⊢ (ComplexShape.up ℕ).prev n = n - 1
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (hm : m = (↑(n + 1) : ℤ)) [HasHomology L (n + 1)]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n + 1)),
  (ComplexShape.up ℕ).prev (n + 1) = n + 1 - 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (hypothesis)
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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1
have this₁ : n ≠ 0
Tactic: have := NeZero.ne n
-- 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''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = (↑n : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1
have zero : ∀ [NeZero (R := ℕ) 0] (hm : m = (↑0 : ℤ)) [HasHomology L 0]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0) (this : Ne (α := ℕ) 0 0),
  (ComplexShape.embeddingUpIntGE 0).f (HSub.hSub (α := ℕ) 0 1) = m - 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this_1, this
-- 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''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = (↑n : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
this : n ≠ 0
zero :
  ∀ [NeZero (R := ℕ) 0] (hm : m = (↑0 : ℤ)) [HasHomology L 0]
    (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0) (this : Ne (α := ℕ) 0 0),
    (ComplexShape.embeddingUpIntGE 0).f (HSub.hSub (α := ℕ) 0 1) = m - 1
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (hm : m = (↑(n + 1) : ℤ)) [HasHomology L (n + 1)]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n + 1)) (this : n + 1 ≠ 0),
  (ComplexShape.embeddingUpIntGE 0).f (n + 1 - 1) = m - 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this_1, this
-- 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''
m : ℤ
inst_2 : HasHomology h.cochainComplex m
n : ℕ
inst_3 : NeZero (n + 1)
hm : m = (↑(n + 1) : ℤ)
inst_4 : HasHomology L (n + 1)
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n + 1)
this : n + 1 ≠ 0
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1 - 1) = m - 1
have succ : (↑n : ℤ) = m - 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' 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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f n = m
have simp : (↑n : ℤ) = m
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' 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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1) = m + 1
have simp : (↑n : ℤ) = m
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' 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.down ℕ).next n = n - 1
have zero : ∀ [NeZero (R := ℕ) 0] (hm : m = -(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) [HasHomology K 0]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0),
  (ComplexShape.down ℕ).next 0 = HSub.hSub (α := ℕ) 0 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this
-- 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''
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
zero :
  ∀ [NeZero (R := ℕ) 0] (hm : m = -(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) [HasHomology K 0]
    (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0),
    (ComplexShape.down ℕ).next 0 = HSub.hSub (α := ℕ) 0 1
⊢ (ComplexShape.down ℕ).next n = n - 1
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (hm : m = -(↑(n + 1 + 1) : ℤ)) [HasHomology K (n + 1)]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n + 1)),
  (ComplexShape.down ℕ).next (n + 1) = n + 1 - 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.Connect (hypothesis)
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.embeddingUpIntLE (-1)).f (n - 1) = m + 1
have this₁ : n ≠ 0
Tactic: have := NeZero.ne n
-- 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''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
this : n ≠ 0
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1
have zero : ∀ [NeZero (R := ℕ) 0] (hm : m = -(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) [HasHomology K 0]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0) (this : Ne (α := ℕ) 0 0),
  (ComplexShape.embeddingUpIntLE (-1)).f (HSub.hSub (α := ℕ) 0 1) = m + 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this_1, this
-- 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''
n : ℕ
inst_2 : NeZero n
m : ℤ
hm : m = -(↑(n + 1) : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology K n
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
this : n ≠ 0
zero :
  ∀ [NeZero (R := ℕ) 0] (hm : m = -(↑(HAdd.hAdd (α := ℕ) 0 1) : ℤ)) [HasHomology K 0]
    (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0) (this : Ne (α := ℕ) 0 0),
    (ComplexShape.embeddingUpIntLE (-1)).f (HSub.hSub (α := ℕ) 0 1) = m + 1
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (hm : m = -(↑(n + 1 + 1) : ℤ)) [HasHomology K (n + 1)]
  (this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n + 1)) (this : n + 1 ≠ 0),
  (ComplexShape.embeddingUpIntLE (-1)).f (n + 1 - 1) = m + 1
Tactic: cases n
Cleared hypotheses: n, inst_2, hm, inst_4, this_1, this
-- 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''
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
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n + 1 - 1) = m + 1
have succ : HSub.hSub (α := ℤ) (-1) (↑n : ℤ) = m + 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
⊢ h.map h (𝟙 K) (𝟙 L) ⋯ = 𝟙 h.cochainComplex
have h₁ : ∀ (m : ℕ),
  Eq (α := h.cochainComplex.X (Int.ofNat m) ⟶ h.cochainComplex.X (Int.ofNat m))
    ((h.map h (𝟙 K) (𝟙 L) sorry).f (Int.ofNat m)) (Hom.f (𝟙 h.cochainComplex) (Int.ofNat m))
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 : 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.map h (𝟙 K) (𝟙 L) ⋯ = 𝟙 h.cochainComplex
have h₂ : Eq (α := h.cochainComplex.X (Int.negSucc 0) ⟶ h.cochainComplex.X (Int.negSucc 0))
  ((h.map h (𝟙 K) (𝟙 L) sorry).f (Int.negSucc 0)) (Hom.f (𝟙 h.cochainComplex) (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 : 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.map h (𝟙 K) (𝟙 L) ⋯ = 𝟙 h.cochainComplex
have h₃ : ∀ (m : ℕ),
  Eq (α := h.cochainComplex.X (Int.negSucc (m + 1)) ⟶ h.cochainComplex.X (Int.negSucc (m + 1)))
    ((h.map h (𝟙 K) (𝟙 L) sorry).f (Int.negSucc (m + 1))) (Hom.f (𝟙 h.cochainComplex) (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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
⊢ 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))
have 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)
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' 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.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.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') sorry).f (Int.ofNat m))
Tactic: ext (m | _ | m)