awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyGE q
⊢ K.IsStrictlyGE p
have rw : ∀ (i : ℤ), autoParam (i < p) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsLE p
⊢ K.IsLE q
have rw : ∀ (i : ℤ), q < i → ExactAt K i
Tactic: rw [isLE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsGE q
⊢ K.IsGE p
have rw : ∀ i < p, ExactAt K i
Tactic: rw [isGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : K.IsStrictlyLE n
⊢ CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
      (mkHomFromSingle (𝟙 (K.X n)) ⋯) =
    𝟙 K
have h : ∀ (i : ℤ),
  (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) sorry)
          (mkHomFromSingle (𝟙 (K.X n)) sorry)).f
      i =
    Hom.f (𝟙 K) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : K.IsStrictlyLE n
i : ℤ
⊢ (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
          (mkHomFromSingle (𝟙 (K.X n)) ⋯)).f
      i =
    Hom.f (𝟙 K) i
have h : ∀ (hi : i < n),
  (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) sorry)
          (mkHomFromSingle (𝟙 (K.X n)) sorry)).f
      i =
    Hom.f (𝟙 K) i
Tactic: obtain hi | rfl | hi := lt_trichotomy i n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : K.IsStrictlyLE n
i : ℤ
h :
  ∀ (hi : i < n),
    (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
            (mkHomFromSingle (𝟙 (K.X n)) ⋯)).f
        i =
      Hom.f (𝟙 K) i
⊢ (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
          (mkHomFromSingle (𝟙 (K.X n)) ⋯)).f
      i =
    Hom.f (𝟙 K) i
have h₁ : ∀ [inst_5 : K.IsStrictlyGE i] [inst_6 : K.IsStrictlyLE i],
  (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) i) (K.X i)) (mkHomToSingle (𝟙 (K.X i)) sorry)
          (mkHomFromSingle (𝟙 (K.X i)) sorry)).f
      i =
    Hom.f (𝟙 K) i
Tactic: obtain hi | rfl | hi := lt_trichotomy i n
Cleared hypotheses: n, inst_3, inst_4
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
n : ℤ
inst_3 : K.IsStrictlyGE n
inst_4 : K.IsStrictlyLE n
i : ℤ
h :
  ∀ (hi : i < n),
    (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
            (mkHomFromSingle (𝟙 (K.X n)) ⋯)).f
        i =
      Hom.f (𝟙 K) i
h₁ :
  ∀ [inst_5 : K.IsStrictlyGE i] [inst_6 : K.IsStrictlyLE i],
    (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) i) (K.X i)) (mkHomToSingle (𝟙 (K.X i)) ⋯)
            (mkHomFromSingle (𝟙 (K.X i)) ⋯)).f
        i =
      Hom.f (𝟙 K) i
⊢ (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
          (mkHomFromSingle (𝟙 (K.X n)) ⋯)).f
      i =
    Hom.f (𝟙 K) i
have h₂ : ∀ (hi : n < i),
  (CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) sorry)
          (mkHomFromSingle (𝟙 (K.X n)) sorry)).f
      i =
    Hom.f (𝟙 K) i
Tactic: obtain hi | rfl | hi := lt_trichotomy i n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
e : K ≅ L
inst_2 : HasZeroObject.{v_1, u_1} C
A : C
n : ℤ
⊢ IsStrictlyGE.{v_1, u_1} (Functor.obj (single C (up ℤ) n) A) n
have rw : ∀ (i : ℤ),
  autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (X.{v_1, u_1, 0} (Functor.obj (single C (up ℤ) n) A) i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
e : K ≅ L
inst_2 : HasZeroObject.{v_1, u_1} C
A : C
n : ℤ
⊢ IsStrictlyLE.{v_1, u_1} (Functor.obj (single C (up ℤ) n) A) n
have rw : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (X.{v_1, u_1, 0} (Functor.obj (single C (up ℤ) n) A) i)
Tactic: rw [isStrictlyLE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ QuasiIso (K := K.truncGE n) (L := L.truncGE n) (truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
have rw : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
Tactic: rw [HomologicalComplex.quasiIso_truncGEMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
have mp : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') → ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
mp : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') → ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
have mpr : (∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i) → ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
h : ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i'
i : ℤ
hi : n ≤ i
⊢ QuasiIsoAt φ i
have mp : ∀ (k : ℕ) (hi : n ≤ n + (↑k : ℤ)), QuasiIsoAt φ (n + (↑k : ℤ))
Tactic: obtain ⟨k, rfl⟩ := Int.le.dest hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ QuasiIso (K := K.truncLE n) (L := L.truncLE n) (truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i
have rw : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ i ≤ n, QuasiIsoAt φ i
Tactic: rw [HomologicalComplex.quasiIso_truncLEMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ i ≤ n, QuasiIsoAt φ i
have mp : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') → ∀ i ≤ n, QuasiIsoAt φ i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
mp : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') → ∀ i ≤ n, QuasiIsoAt φ i
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ i ≤ n, QuasiIsoAt φ i
have mpr : (∀ i ≤ n, QuasiIsoAt φ i) → ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
h : ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i'
i : ℤ
hi : i ≤ n
⊢ QuasiIsoAt φ i
have mp : ∀ (k : ℕ) (h : ∀ (i_1 : ℕ) (i' : ℤ), (embeddingUpIntLE (i + (↑k : ℤ))).f i_1 = i' → QuasiIsoAt φ i')
  (hi : i ≤ i + (↑k : ℤ)), QuasiIsoAt φ i
Tactic: obtain ⟨k, rfl⟩ := Int.le.dest hi
Cleared hypotheses: n, h, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
inst_2 : K.IsStrictlyLE n
a n' : ℤ
h : a + n' = n
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsStrictlyLE n'
have rw : ∀ (i : ℤ),
  n' < i → IsZero.{v_1, u_1} ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).X i)
Tactic: rw [isStrictlyLE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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 ℤ
n : ℤ
inst_2 : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsStrictlyGE n'
have rw : ∀ (i : ℤ),
  autoParam (i < n') isStrictlyGE_iff._auto_1 →
    IsZero.{v_1, u_1} ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsLE n'
have rw : ∀ (i : ℤ), n' < i → ExactAt (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i
Tactic: rw [isLE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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
⊢ ExactAt (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i
have rw : IsZero.{v_1, u_1} (homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i)
Tactic: rw [exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsGE n'
have rw : ∀ i < n', ExactAt (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i
Tactic: rw [isGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.CochainComplex (goal)
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'
⊢ ExactAt (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i
have rw : IsZero.{v_1, u_1} (homology (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K) i)
Tactic: rw [exactAt_iff_isZero_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 : 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
⊢ Eq (α := X K L (Int.negSucc n) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc n) (Int.ofNat m)) 0
have 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
Tactic: obtain _ | n := n
Cleared hypotheses: n, 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
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
⊢ Eq (α := X K L (Int.negSucc n) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc n) (Int.ofNat m)) 0
have 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
Tactic: obtain _ | n := n
Cleared hypotheses: n, 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
n m_1 : ℤ
m : ℕ
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
have 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
Tactic: obtain _ | m := m
Cleared hypotheses: m, 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
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
⊢ Eq (α := X K L (Int.negSucc 0) ⟶ X K L (Int.ofNat m)) (h.d (Int.negSucc 0) (Int.ofNat m)) 0
have 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
Tactic: obtain _ | m := m
Cleared hypotheses: m, 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
n m p : ℤ
⊢ h.d n m ≫ h.d m p = 0
have pos : ∀ (hnm : n + 1 = m), h.d n m ≫ h.d m p = 0
Tactic: by_cases hnm : n + 1 = 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
n m p : ℤ
pos : ∀ (hnm : n + 1 = m), h.d n m ≫ h.d m p = 0
⊢ h.d n m ≫ h.d m p = 0
have neg : ∀ (hnm : ¬n + 1 = m), h.d n m ≫ h.d m p = 0
Tactic: by_cases hnm : n + 1 = 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
n m p : ℤ
hnm : ¬n + 1 = m
⊢ h.d n m ≫ h.d m p = 0
have neg : Eq (α := X K L n ⟶ X K L p) (0 ≫ h.d m p) 0
Tactic: rw [h.shape n m hnm, zero_comp]
-- 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
n m p : ℤ
hnm : ¬n + 1 = m
neg : Eq (α := X K L n ⟶ X K L p) (0 ≫ h.d m p) 0
⊢ h.d n m ≫ h.d m p = 0
have neg₁ : Eq.{v + 1} (α := X K L n ⟶ X K L p) 0 0
Tactic: rw [h.shape n m hnm, zero_comp]
-- 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
n m p : ℤ
hnm : n + 1 = m
⊢ h.d n m ≫ h.d m p = 0
have pos : ∀ (hmp : m + 1 = p), h.d n m ≫ h.d m p = 0
Tactic: by_cases hmp : m + 1 = p
-- 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
n m p : ℤ
hnm : n + 1 = m
pos : ∀ (hmp : m + 1 = p), h.d n m ≫ h.d m p = 0
⊢ h.d n m ≫ h.d m p = 0
have neg : ∀ (hmp : ¬m + 1 = p), h.d n m ≫ h.d m p = 0
Tactic: by_cases hmp : m + 1 = p
-- 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
n m p : ℤ
hnm : n + 1 = m
hmp : ¬m + 1 = p
⊢ h.d n m ≫ h.d m p = 0
have neg : Eq (α := X K L n ⟶ X K L p) (h.d n m ≫ 0) 0
Tactic: rw [h.shape m p hmp, comp_zero]
-- 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
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
⊢ h.d n m ≫ h.d m p = 0
have neg₁ : Eq.{v + 1} (α := X K L n ⟶ X K L p) 0 0
Tactic: rw [h.shape m p hmp, comp_zero]
-- 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
n m p : ℤ
hnm : n + 1 = m
hmp : m + 1 = p
⊢ h.d n m ≫ h.d m p = 0
have 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
Tactic: obtain n | (_ | _ | n) := n
Cleared hypotheses: n, 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
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
⊢ h.d n m ≫ h.d m p = 0
have 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
Tactic: obtain n | (_ | _ | n) := n
Cleared hypotheses: n, 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
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
⊢ h.d n m ≫ h.d m p = 0
have 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
Tactic: obtain n | (_ | _ | n) := n
Cleared hypotheses: n, 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
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
⊢ h.d n m ≫ h.d m p = 0
have 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
Tactic: obtain n | (_ | _ | n) := n
Cleared hypotheses: n, 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
m p : ℤ
hmp : m + 1 = p
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
have 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
Tactic: obtain rfl : m = .ofNat (n + 1) := by simp [← hnm]
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.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ p = Int.ofNat (n + 2)
have simp : HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 = HAdd.hAdd (α := ℤ) (↑n : ℤ) 2
Tactic: simp [← hmp]