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
inst_3 : ∀ (i : ℤ), HasHomology K i
n q : ℤ
hq : n ≤ q
obtain : ∀ (k : ℕ) (hq : n ≤ n + (↑k : ℤ)), QuasiIsoAt (L := K.truncGE n) (K.πTruncGE n) (n + (↑k : ℤ))
⊢ QuasiIsoAt (L := K.truncGE n) (K.πTruncGE n) q

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

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 : CochainComplex.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : ∀ (i : ℤ), HasHomology K i
n : ℤ
k : ℕ
hq : n ≤ n + (↑k : ℤ)
⊢ (embeddingUpIntGE n).f k = n + (↑k : ℤ)

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
inst_3 : ∀ (i : ℤ), HasHomology K i
n : ℤ
k : ℕ
hq : n ≤ n + (↑k : ℤ)
⊢ QuasiIsoAt (L := K.truncGE n) (K.πTruncGE n) (n + (↑k : ℤ))

Tactic:
exact HomologicalComplex.quasiIsoAt_πTruncGE (j := k) _ _ (by simp)

Premises used: HomologicalComplex.quasiIsoAt_π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 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 : ℤ
⊢ n ≤ 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 : ℤ
⊢ Eq (α := K.truncLE n ⟶ L) (CategoryStruct.comp (Y := L.truncLE n) (truncLEMap φ n) (L.ιTruncLE n)) (K.ιTruncLE n ≫ φ)

Tactic:
apply HomologicalComplex.ιTruncLE_naturality

Premises used: HomologicalComplex.ιTruncLE_naturality
-- 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 : ℤ
⊢ Eq (α := K ⟶ L.truncGE n) (CategoryStruct.comp (Y := K.truncGE n) (K.πTruncGE n) (truncGEMap φ n)) (φ ≫ L.πTruncGE n)

Tactic:
apply HomologicalComplex.πTruncGE_naturality

Premises used: HomologicalComplex.πTruncGE_naturality
-- 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 ℤ
n i : ℤ
hi : i < n
inst_2 : K.IsStrictlyGE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntGE_iff] using hi

Premises used: ComplexShape.notMem_range_embeddingUpIntGE_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 ℤ
n i : ℤ
hi : n < i
inst_2 : K.IsStrictlyLE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntLE_iff] using hi

Premises used: ComplexShape.notMem_range_embeddingUpIntLE_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 ℤ
n i : ℤ
hi : i < n
inst_2 : K.IsGE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntGE_iff] using hi

Premises used: ComplexShape.notMem_range_embeddingUpIntGE_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 ℤ
n i : ℤ
hi : n < i
inst_2 : K.IsLE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntLE_iff] using hi

Premises used: ComplexShape.notMem_range_embeddingUpIntLE_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 ℤ
n i : ℤ
hi : i < n
inst_2 : K.IsGE n
inst_3 : HasHomology K i
⊢ IsZero.{v_1, u_1} (homology K i)

Tactic:
(K.exactAt_of_isGE n i hi).isZero_homology

Premises used: CochainComplex.exactAt_of_isGE, HomologicalComplex.ExactAt.isZero_homology
-- 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 ℤ
n i : ℤ
hi : n < i
inst_2 : K.IsLE n
inst_3 : HasHomology K i
⊢ IsZero.{v_1, u_1} (homology K i)

Tactic:
(K.exactAt_of_isLE n i hi).isZero_homology

Premises used: CochainComplex.exactAt_of_isLE, HomologicalComplex.ExactAt.isZero_homology
-- 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 ℤ
n : ℤ
mp : K.IsStrictlyGE n → ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
mpr : (∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)) → K.IsStrictlyGE n
⊢ K.IsStrictlyGE n ↔ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X 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 : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
h : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
K.isZero_of_isStrictlyGE n i hi

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- 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 ℤ
n : ℤ
h : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
exact K.isZero_of_isStrictlyGE n i hi

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE n

Tactic:
IsStrictlySupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsStrictlySupported.mk
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i), IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE n

Tactic:
refine IsStrictlySupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsStrictlySupported.mk
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ i < n

Tactic:
rw [notMem_range_embeddingUpIntGE_iff] at hi

Premises used: ComplexShape.notMem_range_embeddingUpIntGE_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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : i < n
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
h i hi
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : i < n
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
exact h i hi
-- 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 ℤ
n : ℤ
mp : K.IsStrictlyLE n → ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
mpr : (∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)) → K.IsStrictlyLE n
⊢ K.IsStrictlyLE n ↔ ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X 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 : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
h : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
K.isZero_of_isStrictlyLE n i hi

Premises used: CochainComplex.isZero_of_isStrictlyLE
-- 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 ℤ
n : ℤ
h : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
exact K.isZero_of_isStrictlyLE n i hi

Premises used: CochainComplex.isZero_of_isStrictlyLE
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyLE n

Tactic:
IsStrictlySupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsStrictlySupported.mk
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i), IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyLE n

Tactic:
refine IsStrictlySupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsStrictlySupported.mk
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ n < i

Tactic:
rw [notMem_range_embeddingUpIntLE_iff] at hi

Premises used: ComplexShape.notMem_range_embeddingUpIntLE_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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : n < i
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
h i hi
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero.{v_1, u_1} (K.X i)
i : ℤ
hi : n < i
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
exact h i hi
-- 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 ℤ
n : ℤ
mp : K.IsGE n → ∀ i < n, ExactAt K i
mpr : (∀ i < n, ExactAt K i) → K.IsGE n
⊢ K.IsGE n ↔ ∀ i < n, ExactAt K 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 : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
h : K.IsGE n
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
K.exactAt_of_isGE n i hi

Premises used: CochainComplex.exactAt_of_isGE
-- 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 ℤ
n : ℤ
h : K.IsGE n
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
exact K.exactAt_of_isGE n i hi

Premises used: CochainComplex.exactAt_of_isGE
-- 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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
⊢ K.IsGE n

Tactic:
IsSupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsSupported.mk
-- 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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i), ExactAt K i
⊢ K.IsGE n

Tactic:
refine IsSupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsSupported.mk
-- 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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ i < n

Tactic:
rw [notMem_range_embeddingUpIntGE_iff] at hi

Premises used: ComplexShape.notMem_range_embeddingUpIntGE_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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
h i hi
-- 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 ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
exact h i hi
-- 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 ℤ
n : ℤ
mp : K.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i
mpr : (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n
⊢ K.IsLE n ↔ ∀ (i : ℤ), n < i → ExactAt K 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 : CochainComplex.{v_1, u_1, 0} C ℤ
n : ℤ
h : K.IsLE n
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
K.exactAt_of_isLE n i hi

Premises used: CochainComplex.exactAt_of_isLE
-- 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 ℤ
n : ℤ
h : K.IsLE n
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
exact K.exactAt_of_isLE n i hi

Premises used: CochainComplex.exactAt_of_isLE
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
⊢ K.IsLE n

Tactic:
IsSupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsSupported.mk
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
mpr : ∀ (i : ℤ) (hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i), ExactAt K i
⊢ K.IsLE n

Tactic:
refine IsSupported.mk (fun i hi ↦ ?_)

Premises used: HomologicalComplex.IsSupported.mk
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ n < i

Tactic:
rw [notMem_range_embeddingUpIntLE_iff] at hi

Premises used: ComplexShape.notMem_range_embeddingUpIntLE_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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
h i hi
-- 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 ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
exact h i hi
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyLE p
rw : ∀ (i : ℤ), q < i → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyLE q

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 : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyLE p
i : ℤ
hi : q < i
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
K.isZero_of_isStrictlyLE p _

Premises used: CochainComplex.isZero_of_isStrictlyLE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyLE p
i : ℤ
hi : q < i
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
exact K.isZero_of_isStrictlyLE p _

Premises used: CochainComplex.isZero_of_isStrictlyLE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyGE q
rw : ∀ (i : ℤ), autoParam (i < p) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (K.X i)
⊢ K.IsStrictlyGE p

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 : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyGE q
i : ℤ
hi : autoParam (i < p) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
K.isZero_of_isStrictlyGE q _

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsStrictlyGE q
i : ℤ
hi : autoParam (i < p) isStrictlyGE_iff._auto_1
⊢ IsZero.{v_1, u_1} (K.X i)

Tactic:
exact K.isZero_of_isStrictlyGE q _

Premises used: CochainComplex.isZero_of_isStrictlyGE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsLE p
rw : ∀ (i : ℤ), q < i → ExactAt K i
⊢ K.IsLE q

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 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsLE p
i : ℤ
hi : q < i
⊢ ExactAt K i

Tactic:
K.exactAt_of_isLE p _

Premises used: CochainComplex.exactAt_of_isLE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsLE p
i : ℤ
hi : q < i
⊢ ExactAt K i

Tactic:
exact K.exactAt_of_isLE p _

Premises used: CochainComplex.exactAt_of_isLE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsGE q
rw : ∀ i < p, ExactAt K i
⊢ K.IsGE p

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 : HasZeroMorphisms.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsGE q
i : ℤ
hi : i < p
⊢ ExactAt K i

Tactic:
K.exactAt_of_isGE q _

Premises used: CochainComplex.exactAt_of_isGE
-- 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 ℤ
p q : ℤ
hpq : p ≤ q
inst_2 : K.IsGE q
i : ℤ
hi : i < p
⊢ ExactAt K i

Tactic:
exact K.exactAt_of_isGE q _

Premises used: CochainComplex.exactAt_of_isGE
-- 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 ℤ
e : K ≅ L
n : ℤ
inst_2 : K.IsStrictlyLE n
⊢ L.IsStrictlyLE n

Tactic:
apply isStrictlySupported_of_iso e

Premises used: HomologicalComplex.isStrictlySupported_of_iso
-- 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 ℤ
e : K ≅ L
n : ℤ
inst_2 : K.IsStrictlyGE n
⊢ L.IsStrictlyGE n

Tactic:
apply isStrictlySupported_of_iso e

Premises used: HomologicalComplex.isStrictlySupported_of_iso
-- 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 ℤ
e : K ≅ L
n : ℤ
inst_2 : K.IsLE n
⊢ L.IsLE n

Tactic:
apply isSupported_of_iso e

Premises used: HomologicalComplex.isSupported_of_iso
-- 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 ℤ
e : K ≅ L
n : ℤ
inst_2 : K.IsGE n
⊢ L.IsGE n

Tactic:
apply isSupported_of_iso e

Premises used: HomologicalComplex.isSupported_of_iso
-- 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
X : CochainComplex.{v_1, u_1, 0} C ℕ
x : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE 0).f i ≠ x
⊢ ∀ (i : ℕ), embeddingUpNat.f i ≠ x

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
X : ChainComplex.{v_1, u_1, 0} C ℕ
x : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE 0).f i ≠ x
⊢ ∀ (i : ℕ), embeddingDownNat.f i ≠ x

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 : 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 + 1 = 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 : n + 1 = i
⊢ n < i

Tactic:
lia