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''
n : ℕ
⊢ (ComplexShape.embeddingUpIntGE 0).f n = (↑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' 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 : ℕ
dsimp :
  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) ⋯))
⊢ Eq (α := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X n ⟶ L.X (n + 1))
    (Iso.hom
        ((fun (n : ℕ) ↦
            (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯ :
              (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X n ≅ h.cochainComplex.X (↑n : ℤ)))
          n) ≫
      L.d n (n + 1))
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X (n + 1))
      ((restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).d n (n + 1))
      (Iso.hom
        ((fun (n : ℕ) ↦
            (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯ :
              (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X n ≅ h.cochainComplex.X (↑n : ℤ)))
          (n + 1))))

Tactic:
dsimp only
-- 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 : ℕ
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1) = (↑(n + 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 : ℕ
rw :
  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))
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X (n + 1))
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯) ≫
        L.d n (n + 1) ≫ Iso.inv (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯))
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯)))
⊢ 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) ⋯))

Tactic:
rw [restriction_d_eq (e := (ComplexShape.embeddingUpIntGE 0)) _ (i' := n)
      (j' := (n + 1 : ℕ)) (by simp) (by simp), cochainComplex_d, h.d_ofNat]

Premises used: CochainComplex.ConnectData.d_ofNat, HomologicalComplex.restriction_d_eq, CochainComplex.ConnectData.cochainComplex_d, ComplexShape.embeddingUpIntGE, OfNat.ofNat
-- 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 : ℕ
⊢ 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))
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).X (n + 1))
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯) ≫
        L.d n (n + 1) ≫ Iso.inv (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯))
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 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''
n : ℕ
⊢ HSub.hSub (α := ℤ) (-1) (↑n : ℤ) = Int.negSucc n

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 : ℕ
dsimp :
  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)) ⋯))
⊢ Eq (α := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X (n + 1) ⟶ K.X n)
    (CategoryStruct.comp (Y := K.X (n + 1))
      (Iso.hom
        ((fun (n : ℕ) ↦
            (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯ :
              (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X n ≅
                h.cochainComplex.X (Int.negSucc n)))
          (n + 1)))
      (K.d (n + 1) n))
    ((restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d (n + 1) n ≫
      Iso.hom
        ((fun (n : ℕ) ↦
            (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯ :
              (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X n ≅
                h.cochainComplex.X (Int.negSucc n)))
          n))

Tactic:
dsimp only
-- 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 : ℕ
⊢ -1 - HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = Int.negSucc (n + 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 : ℕ
rw :
  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)
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X n)
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯) ≫
        K.d (n + 1) n ≫ Iso.inv (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯))
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯)))
⊢ 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)) ⋯))

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]

Premises used: ComplexShape.embeddingUpIntLE, HomologicalComplex.restriction_d_eq, CochainComplex.ConnectData.d_negSucc, CochainComplex.ConnectData.cochainComplex_d, OfNat.ofNat, Neg.neg
-- 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 : ℕ
⊢ 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)
    (CategoryStruct.comp (Y := (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).X n)
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯) ≫
        K.d (n + 1) n ≫ Iso.inv (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯))
      (Iso.hom (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-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 : ℤ)
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
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
⊢ (ComplexShape.up ℕ).prev n = n - 1

Tactic:
cases n
-- 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 = (↑0 : ℤ)
inst_4 : HasHomology L 0
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
⊢ (ComplexShape.up ℕ).prev 0 = HSub.hSub (α := ℕ) 0 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''
m : ℤ
inst_2 : HasHomology h.cochainComplex m
n : ℕ
inst_3 : NeZero (n + 1)
hm : m = (↑(n + 1) : ℤ)
inst_4 : HasHomology L (n + 1)
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n + 1)
⊢ (ComplexShape.up ℕ).prev (n + 1) = n + 1 - 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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.up ℕ).next n = n + 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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- 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 : ℤ)
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
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
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1

Tactic:
cases n
-- 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) : ℤ)
inst_4 : HasHomology L (n + 1)
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n + 1)
this : n + 1 ≠ 0
succ : (↑n : ℤ) = m - 1
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1 - 1) = 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''
m : ℤ
inst_2 : HasHomology h.cochainComplex m
inst_3 : NeZero (R := ℕ) 0
hm : m = (↑0 : ℤ)
inst_4 : HasHomology L 0
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology 0
this : Ne (α := ℕ) 0 0
⊢ 0 = 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) : ℤ)
inst_4 : HasHomology L (n + 1)
this_1 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology (n + 1)
this : n + 1 ≠ 0
⊢ (↑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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
simp : (↑n : ℤ) = m
⊢ (ComplexShape.embeddingUpIntGE 0).f n = 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''
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
⊢ (↑n : ℤ) = m

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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
simp : (↑n : ℤ) = m
⊢ (ComplexShape.embeddingUpIntGE 0).f (n + 1) = 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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).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 : ℤ)
inst_3 : HasHomology h.cochainComplex m
inst_4 : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).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''
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 ℕ).prev n = n + 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
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
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
⊢ (ComplexShape.down ℕ).next n = n - 1

Tactic:
cases n
-- 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 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology 0
⊢ (ComplexShape.down ℕ).next 0 = HSub.hSub (α := ℕ) 0 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''
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 : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology (n + 1)
⊢ (ComplexShape.down ℕ).next (n + 1) = n + 1 - 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
⊢ -1 - HAdd.hAdd (α := ℤ) (↑n : ℤ) 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''
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
⊢ HSub.hSub (α := ℤ) (-1) (↑n : ℤ) = m

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
⊢ n ≠ 0

Tactic:
have := NeZero.ne n
-- 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_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
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
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1

Tactic:
cases n
-- 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
succ : HSub.hSub (α := ℤ) (-1) (↑n : ℤ) = m + 1
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n + 1 - 1) = m + 1

Tactic:
simp