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 : 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
h :
  ∀ (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
⊢ CategoryStruct.comp (Y := Functor.obj (single C (up ℤ) n) (K.X n)) (mkHomToSingle (𝟙 (K.X n)) ⋯)
      (mkHomFromSingle (𝟙 (K.X n)) ⋯) =
    𝟙 K

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
h₂ :
  ∀ (hi : 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
⊢ (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

Tactic:
obtain hi | rfl | hi := lt_trichotomy i n

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
hi : i < n
⊢ i < n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
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

Tactic:
apply (K.isZero_of_isStrictlyGE n i (by lia)).eq_of_src

Premises used: CochainComplex.isZero_of_isStrictlyGE, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
i : ℤ
inst_3 : K.IsStrictlyGE i
inst_4 : 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

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
hi : n < i
⊢ n < i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
hi : 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

Tactic:
apply (K.isZero_of_isStrictlyLE n i (by lia)).eq_of_tgt

Premises used: CochainComplex.isZero_of_isStrictlyLE, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v_1, u_1, 0} C ℤ) (Functor.obj (single C (up ℤ) n) (K.X n))
      (Functor.obj (single C (up ℤ) n) (K.X n)))
    (mkHomFromSingle (𝟙 (K.X n)) ⋯ ≫ mkHomToSingle (𝟙 (K.X n)) ⋯) (𝟙 (Functor.obj (single C (up ℤ) n) (K.X n)))

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
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)
⊢ IsStrictlyGE.{v_1, u_1} (Functor.obj (single C (up ℤ) n) A) n

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ i ≠ n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 i : ℤ
hi : 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:
exact isZero_single_obj_X _ _ _ _ (by lia)

Premises used: HomologicalComplex.isZero_single_obj_X
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
rw : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (X.{v_1, u_1, 0} (Functor.obj (single C (up ℤ) n) A) i)
⊢ IsStrictlyLE.{v_1, u_1} (Functor.obj (single C (up ℤ) n) A) n

Tactic:
rw [isStrictlyLE_iff]

Premises used: CochainComplex.isStrictlyLE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 i : ℤ
hi : n < i
⊢ i ≠ n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 i : ℤ
hi : n < i
⊢ IsZero.{v_1, u_1} (X.{v_1, u_1, 0} (Functor.obj (single C (up ℤ) n) A) i)

Tactic:
exact isZero_single_obj_X _ _ _ _ (by lia)

Premises used: HomologicalComplex.isZero_single_obj_X
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst_5 : K.IsStrictlyGE n
⊢ IsIso (Y := K.truncGE n) (HomologicalComplex.πTruncGE K (embeddingUpIntGE n))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst_5 : K.IsStrictlyLE n
⊢ IsIso (X := K.truncLE n) (HomologicalComplex.ιTruncLE K (embeddingUpIntLE n))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
n : ℤ
⊢ IsIso (Y := K.truncGE n) (K.πTruncGE n) ↔ K.IsStrictlyGE n

Tactic:
apply HomologicalComplex.isIso_πTruncGE_iff

Premises used: HomologicalComplex.isIso_πTruncGE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
n : ℤ
⊢ IsIso (X := K.truncLE n) (K.ιTruncLE n) ↔ K.IsStrictlyLE n

Tactic:
apply HomologicalComplex.isIso_ιTruncLE_iff

Premises used: HomologicalComplex.isIso_ιTruncLE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
n : ℤ
⊢ QuasiIso (L := K.truncGE n) (K.πTruncGE n) ↔ K.IsGE n

Tactic:
quasiIso_πTruncGE_iff_isSupported K (embeddingUpIntGE n)

Premises used: HomologicalComplex.quasiIso_πTruncGE_iff_isSupported, ComplexShape.embeddingUpIntGE, CochainComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
n : ℤ
⊢ QuasiIso (K := K.truncLE n) (K.ιTruncLE n) ↔ K.IsLE n

Tactic:
quasiIso_ιTruncLE_iff_isSupported K (embeddingUpIntLE n)

Premises used: ComplexShape.embeddingUpIntLE, CochainComplex.ιTruncLE, HomologicalComplex.quasiIso_ιTruncLE_iff_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst_5 rw : K.IsGE n
⊢ QuasiIso (L := K.truncGE n) (K.πTruncGE n)

Tactic:
rw [quasiIso_πTruncGE_iff]

Premises used: CochainComplex.quasiIso_πTruncGE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst_5 : K.IsGE n
⊢ K.IsGE n

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst_5 rw : K.IsLE n
⊢ QuasiIso (K := K.truncLE n) (K.ιTruncLE n)

Tactic:
rw [quasiIso_ιTruncLE_iff]

Premises used: CochainComplex.quasiIso_ιTruncLE_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
inst_3 : ∀ (i : ℤ), HasHomology K i
inst_4 : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst_5 : K.IsLE n
⊢ K.IsLE n

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
rw : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
⊢ QuasiIso (K := K.truncGE n) (L := L.truncGE n) (truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Tactic:
rw [HomologicalComplex.quasiIso_truncGEMap_iff]

Premises used: HomologicalComplex.quasiIso_truncGEMap_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
mpr : (∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i) → ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i'
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
mp : ∀ (k : ℕ) (hi : n ≤ n + (↑k : ℤ)), QuasiIsoAt φ (n + (↑k : ℤ))
⊢ QuasiIsoAt φ i

Tactic:
obtain ⟨k, rfl⟩ := Int.le.dest hi

Premises used: Int.le.dest, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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'
k : ℕ
hi : n ≤ n + (↑k : ℤ)
⊢ QuasiIsoAt φ (n + (↑k : ℤ))

Tactic:
h k _ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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'
k : ℕ
hi : n ≤ n + (↑k : ℤ)
⊢ QuasiIsoAt φ (n + (↑k : ℤ))

Tactic:
exact h k _ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ), n ≤ i → QuasiIsoAt φ i
i : ℕ
⊢ n ≤ n + (↑i : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ), n ≤ i → QuasiIsoAt φ i
i : ℕ
⊢ QuasiIsoAt φ ((embeddingUpIntGE n).f i)

Tactic:
exact h _ (by dsimp; lia)
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 : ℤ
rw : (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ i ≤ n, QuasiIsoAt φ i
⊢ QuasiIso (K := K.truncLE n) (L := L.truncLE n) (truncLEMap φ n) ↔ ∀ i ≤ n, QuasiIsoAt φ i

Tactic:
rw [HomologicalComplex.quasiIso_truncLEMap_iff]

Premises used: HomologicalComplex.quasiIso_truncLEMap_iff
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
mpr : (∀ i ≤ n, QuasiIsoAt φ i) → ∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i'
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntLE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ i ≤ n, QuasiIsoAt φ i

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
mp :
  ∀ (k : ℕ) (h : ∀ (i_1 : ℕ) (i' : ℤ), (embeddingUpIntLE (i + (↑k : ℤ))).f i_1 = i' → QuasiIsoAt φ i')
    (hi : i ≤ i + (↑k : ℤ)), QuasiIsoAt φ i
⊢ QuasiIsoAt φ i

Tactic:
obtain ⟨k, rfl⟩ := Int.le.dest hi

Premises used: Int.le.dest, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
i : ℤ
k : ℕ
h : ∀ (i_1 : ℕ) (i' : ℤ), (embeddingUpIntLE (i + (↑k : ℤ))).f i_1 = i' → QuasiIsoAt φ i'
hi : i ≤ i + (↑k : ℤ)
⊢ i + (↑k : ℤ) - (↑k : ℤ) = i

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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
i : ℤ
k : ℕ
h : ∀ (i_1 : ℕ) (i' : ℤ), (embeddingUpIntLE (i + (↑k : ℤ))).f i_1 = i' → QuasiIsoAt φ i'
hi : i ≤ i + (↑k : ℤ)
⊢ QuasiIsoAt φ i

Tactic:
exact h k _ (by dsimp; lia)
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 ≤ n, QuasiIsoAt φ i
i : ℕ
⊢ n - (↑i : ℤ) ≤ n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.Embedding.CochainComplex
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 ≤ n, QuasiIsoAt φ i
i : ℕ
⊢ QuasiIsoAt φ ((embeddingUpIntLE n).f i)

Tactic:
exact h _ (by dsimp; 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
inst_2 : HasZeroObject.{v_1, u_1} C
A : C
n : ℤ
⊢ IsStrictlyGE.{v_1, u_1} (Functor.obj (singleFunctor C n) A) n

Tactic:
inferInstanceAs (IsStrictlyGE ((single C (ComplexShape.up ℤ) n).obj A) n)

Premises used: _private.0.CochainComplex.instIsStrictlyGEObjIntSingleFunctor._proof_1
-- 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
inst_2 : HasZeroObject.{v_1, u_1} C
A : C
n : ℤ
⊢ IsStrictlyLE.{v_1, u_1} (Functor.obj (singleFunctor C n) A) n

Tactic:
inferInstanceAs (IsStrictlyLE ((single C (ComplexShape.up ℤ) n).obj A) n)

Premises used: _private.0.CochainComplex.instIsStrictlyLEObjIntSingleFunctor._proof_1
-- 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 ℤ
n : ℤ
inst_2 : K.IsStrictlyLE n
a n' : ℤ
h : a + n' = n
rw :
  ∀ (i : ℤ),
    n' < i → IsZero.{v_1, u_1} ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).X i)
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsStrictlyLE n'

Tactic:
rw [isStrictlyLE_iff]

Premises used: CochainComplex.isStrictlyLE_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 ℤ
n : ℤ
inst_2 : K.IsStrictlyLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ n < i + a

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 ℤ
n : ℤ
inst_2 : K.IsStrictlyLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ IsZero.{v_1, u_1} ((Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).X i)

Tactic:
exact IsZero.of_iso (K.isZero_of_isStrictlyLE n _ (by lia)) (K.shiftFunctorObjXIso a i _ rfl)

Premises used: CochainComplex.isZero_of_isStrictlyLE, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Limits.IsZero.of_iso, rfl
-- 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 ℤ
n : ℤ
inst_2 : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
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)
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) a) K).IsStrictlyGE n'

Tactic:
rw [isStrictlyGE_iff]

Premises used: CochainComplex.isStrictlyGE_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 ℤ
n : ℤ
inst_2 : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : autoParam (i < n') isStrictlyGE_iff._auto_1
⊢ i + a < 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 ℤ
n : ℤ
inst_2 : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : 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:
exact IsZero.of_iso (K.isZero_of_isStrictlyGE n _ (by lia)) (K.shiftFunctorObjXIso a i _ rfl)

Premises used: CochainComplex.shiftFunctorObjXIso, CategoryTheory.Limits.IsZero.of_iso, CochainComplex.isZero_of_isStrictlyGE, rfl
-- 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
rw : ∀ (i : ℤ), n' < i → 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).IsLE n'

Tactic:
rw [isLE_iff]

Premises used: CochainComplex.isLE_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.IsLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
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.IsLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ n < a + i

Tactic:
lia