awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
inst_3 : K.IsLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ IsZero.{v_1, u_1} (homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i)

Tactic:
exact IsZero.of_iso (K.isZero_of_isLE n (a + i) (by lia))
    (((homologyFunctor C _ (0 : ℤ)).shiftIso a i _ rfl).app K)

Premises used: HomologicalComplex.homologyFunctor, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, CategoryTheory.Functor.shiftIso, CategoryTheory.Iso.app, OfNat.ofNat, rfl, CochainComplex.isZero_of_isLE
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
inst_3 : K.IsGE n
a n' : ℤ
h : a + n' = n
rw : ∀ i < n', ExactAt (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsGE n'

Tactic:
rw [isGE_iff]

Premises used: CochainComplex.isGE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
inst_3 : K.IsGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : i < n'
rw : IsZero.{v_1, u_1} (homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i)
⊢ ExactAt (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i

Tactic:
rw [exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
inst_3 : K.IsGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : i < n'
⊢ a + i < n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
inst_3 : K.IsGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : i < n'
⊢ IsZero.{v_1, u_1} (homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i)

Tactic:
exact IsZero.of_iso (K.isZero_of_isGE n (a + i) (by lia))
    (((homologyFunctor C _ (0 : ℤ)).shiftIso a i _ rfl).app K)

Premises used: HomologicalComplex.homologyFunctor, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, CategoryTheory.Functor.shiftIso, CochainComplex.isZero_of_isGE, CategoryTheory.Iso.app, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
⊢ (K.shortComplexTruncLE n).ShortExact

Tactic:
apply HomologicalComplex.shortComplexTruncLE_shortExact

Premises used: HomologicalComplex.shortComplexTruncLE_shortExact
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (K.shortComplexTruncLE n₀).g ≫ K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.πTruncGE n₁

Tactic:
apply HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE

Premises used: HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE
-- 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 ℕ
n : ℕ
⊢ X K L (↑n : ℤ) = L.X n

Tactic:
rfl

Premises used: CochainComplex.ConnectData.X, rfl
-- 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 ℕ
n : ℕ
⊢ X K L (Int.negSucc n) = K.X n

Tactic:
rfl

Premises used: CochainComplex.ConnectData.X, rfl
-- 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 ℕ
⊢ X K L 0 = L.X 0

Tactic:
rfl

Premises used: CochainComplex.ConnectData.X, rfl
-- 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 ℕ
⊢ X K L (-1) = K.X 0

Tactic:
rfl

Premises used: CochainComplex.ConnectData.X, rfl
-- 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
n m : ℕ
⊢ h.d (↑n : ℤ) (↑m : ℤ) = L.d n m

Tactic:
rfl

Premises used: rfl, CochainComplex.ConnectData.d
-- 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
n m : ℕ
⊢ h.d (Int.negSucc n) (Int.negSucc m) = K.d n m

Tactic:
simp [d]

Premises used: CochainComplex.ConnectData.d
-- 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.d (-1) 0 = h.d₀

Tactic:
rfl

Premises used: rfl, CochainComplex.ConnectData.d
-- 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 (α := X K L 0 ⟶ X K L 1) (h.d 0 1) (L.d 0 1)

Tactic:
rfl

Premises used: rfl, CochainComplex.ConnectData.d
-- 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 (α := X K L (-2) ⟶ X K L (-1)) (h.d (-2) (-1)) (K.d 1 0)

Tactic:
rfl

Premises used: rfl, CochainComplex.ConnectData.d
-- 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
n_1 m_1 : ℤ
n m : ℕ
hnm : ¬HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = (↑m : ℤ)
⊢ ¬n + 1 = 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
n_1 m_1 : ℤ
n m : ℕ
hnm : ¬Int.negSucc n + 1 = Int.negSucc m
⊢ ¬m + 1 = 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
n_1 m_1 : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.negSucc m
⊢ Eq (α := X K L (Int.negSucc n) ⟶ X K L (Int.negSucc m)) (h.d (Int.negSucc n) (Int.negSucc m)) 0

Tactic:
simpa only [d_negSucc] using K.shape n m (by simp at hnm ⊢; lia)

Premises used: CochainComplex.ConnectData.d_negSucc, HomologicalComplex.shape
-- 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
n m : ℤ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat 0)) (h.d (Int.negSucc 0) (Int.ofNat 0)) 0

Tactic:
simp at hnm
-- 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
n_1 m_1 : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.ofNat m
zero :
  ∀ (hnm : Int.negSucc 0 + 1 ≠ Int.ofNat m),
    Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc 0) (Int.ofNat m)) 0
succ :
  ∀ (n : ℕ) (hnm : Int.negSucc (n + 1) + 1 ≠ Int.ofNat m),
    Eq (α := X K L (Int.negSucc (n + 1)) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc (n + 1)) (Int.ofNat m)) 0
⊢ Eq (α := X K L (Int.negSucc n) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc n) (Int.ofNat m)) 0

Tactic:
obtain _ | n := n
-- 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
n m_1 : ℤ
m : ℕ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat m
zero :
  ∀ (hnm : Int.negSucc 0 + 1 ≠ Int.ofNat 0),
    Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat 0)) (h.d (Int.negSucc 0) (Int.ofNat 0)) 0
zero₁ :
  ∀ (m : ℕ) (hnm : Int.negSucc 0 + 1 ≠ Int.ofNat (m + 1)),
    Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat (m + 1))) (h.d (Int.negSucc 0) (Int.ofNat (m + 1))) 0
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc 0) (Int.ofNat m)) 0

Tactic:
obtain _ | 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
n m_1 : ℤ
m : ℕ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat (m + 1)
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat (m + 1))) (h.d (Int.negSucc 0) (Int.ofNat (m + 1))) 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 : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
n_1 m_1 : ℤ
m n : ℕ
hnm : Int.negSucc (n + 1) + 1 ≠ Int.ofNat m
⊢ Eq (α := X K L (Int.negSucc (n + 1)) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc (n + 1)) (Int.ofNat m)) 0

Tactic:
simp only [d]

Premises used: CochainComplex.ConnectData.d
-- 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
n m p : ℤ
pos : ∀ (hnm : n + 1 = m), h.d n m ≫ h.d m p = 0
neg : ∀ (hnm : ¬n + 1 = m), h.d n m ≫ h.d m p = 0
⊢ h.d n m ≫ h.d m p = 0

Tactic:
by_cases hnm : n + 1 = 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
n m p : ℤ
hnm : ¬n + 1 = m
neg : Eq (α := X K L n ⟶ X K L p) (0 ≫ h.d m p) 0
neg₁ neg₂ : Eq.{v + 1} (α := X K L n ⟶ X K L p) 0 0
⊢ h.d n m ≫ h.d m p = 0

Tactic:
rw [h.shape n m hnm, zero_comp]

Premises used: CochainComplex.ConnectData.shape, CategoryTheory.Limits.zero_comp
-- 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
n m p : ℤ
hnm : n + 1 = m
pos : ∀ (hmp : m + 1 = p), h.d n m ≫ h.d m p = 0
neg : ∀ (hmp : ¬m + 1 = p), h.d n m ≫ h.d m p = 0
⊢ h.d n m ≫ h.d m p = 0

Tactic:
by_cases hmp : m + 1 = p
-- 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
n m p : ℤ
hnm : n + 1 = m
hmp : ¬m + 1 = p
neg : Eq (α := X K L n ⟶ X K L p) (h.d n m ≫ 0) 0
neg₁ neg₂ : Eq.{v + 1} (α := X K L n ⟶ X K L p) 0 0
⊢ h.d n m ≫ h.d m p = 0

Tactic:
rw [h.shape m p hmp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CochainComplex.ConnectData.shape
-- 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
n m p : ℤ
hnm : n + 1 = m
hmp : m + 1 = p
pos : ∀ (n : ℕ) (hnm : Int.ofNat n + 1 = m), Eq (α := X K L (Int.ofNat n) ⟶ X K L p) (h.d (Int.ofNat n) m ≫ h.d m p) 0
pos₁ : ∀ (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
pos₂ :
  ∀ (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
pos₃ :
  ∀ (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
⊢ h.d n m ≫ h.d m p = 0

Tactic:
obtain n | (_ | _ | n) := n
-- 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 p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.ofNat n + 1 = m
⊢ m = Int.ofNat (n + 1)

Tactic:
simp [← hnm]
-- 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 p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.ofNat n + 1 = m
pos :
  ∀ (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
⊢ Eq (α := X K L (Int.ofNat n) ⟶ X K L p) (h.d (Int.ofNat n) m ≫ h.d m p) 0

Tactic:
obtain rfl : m = .ofNat (n + 1) := by simp [← hnm]

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : 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)
simp : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 2
⊢ p = Int.ofNat (n + 2)

Tactic:
simp [← hmp]
-- 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
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 2

Tactic:
lia
-- 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
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
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
⊢ 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

Tactic:
obtain rfl : p = .ofNat (n + 2) := by simp [← hmp]; lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
n : ℕ
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
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:
simp only [Int.ofNat_eq_natCast, X_ofNat, d_ofNat, HomologicalComplex.d_comp_d]

Premises used: CochainComplex.ConnectData.d_ofNat, Int.ofNat_eq_natCast, CochainComplex.ConnectData.X_ofNat, HomologicalComplex.d_comp_d
-- 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 p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc 0 + 1 = m
⊢ m = 0

Tactic:
lia
-- 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 p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc 0 + 1 = m
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
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L p) (h.d (Int.negSucc 0) m ≫ h.d m p) 0

Tactic:
obtain rfl : m = 0 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : 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
⊢ p = 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 : 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
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
⊢ 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 : p = 1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
hnm : Int.negSucc 0 + 1 = 0
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:
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 p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc (HAdd.hAdd (α := ℕ) 0 1) + 1 = m
⊢ 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 : 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
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
⊢ 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

Tactic:
obtain rfl : m = -1 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : 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
⊢ p = 0

Tactic:
lia
-- 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
p : ℤ
hmp : HAdd.hAdd (α := ℤ) (-1) 1 = p
hnm : Int.negSucc (HAdd.hAdd (α := ℕ) 0 1) + 1 = -1
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
⊢ 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 : p = 0 := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
hnm : Int.negSucc (HAdd.hAdd (α := ℕ) 0 1) + 1 = -1
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:
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 p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = m
⊢ m = 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 : 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
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
⊢ 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

Tactic:
obtain rfl : m = .negSucc (n + 1) := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : 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)
⊢ p = 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 : 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)
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
⊢ 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 : p = .negSucc n := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Connect
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
K : ChainComplex.{v, u, 0} C ℕ
L : CochainComplex.{v, u, 0} C ℕ
h : ConnectData K L
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)
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:
simp