awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'
⊢ Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos :
  ∀ (i : ι),
    Eq (α := K.X (e.f i) ⟶ (L.extend e).X (e.f i)) (Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) (e.f i)) (ψ.f (e.f i))
⊢ Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i : ι
⊢ Eq (α := K.X (e.f i) ⟶ (L.extend e).X (e.f i)) (Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) (e.f i)) (ψ.f (e.f i))

Tactic:
simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

Premises used: ComplexShape.Embedding.liftExtend_f, ComplexShape.Embedding.homRestrict_f, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi'
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ Hom.f (e.liftExtend (e.homRestrict ψ) ⋯) i' = ψ.f i'

Tactic:
apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_tgt

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
h : ∀ (i : ι), Hom.f (e.homRestrict (e.liftExtend φ hφ)) i = φ.f i
⊢ e.homRestrict (e.liftExtend φ hφ) = φ

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i : ι
⊢ Hom.f (e.homRestrict (e.liftExtend φ hφ)) i = φ.f i

Tactic:
simp [e.homRestrict_f _ rfl, e.liftExtend_f _ _ rfl]

Premises used: ComplexShape.Embedding.liftExtend_f, ComplexShape.Embedding.homRestrict_f, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K K' : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
h :
  ∀ (i : ι),
    Eq (α := (K'.restriction e).X i ⟶ L.X i) (Hom.f (e.homRestrict (α ≫ ψ)) i)
      (Hom.f (restrictionMap α e ≫ e.homRestrict ψ) i)
⊢ Eq (α := K'.restriction e ⟶ L) (e.homRestrict (α ≫ ψ)) (restrictionMap α e ≫ e.homRestrict ψ)

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K K' : HomologicalComplex.{v_1, u_3, u_2} C c'
L : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
i : ι
⊢ Eq (α := (K'.restriction e).X i ⟶ L.X i) (Hom.f (e.homRestrict (α ≫ ψ)) i)
    (Hom.f (restrictionMap α e ≫ e.homRestrict ψ) i)

Tactic:
simp [homRestrict_f _ _ rfl, restrictionXIso]

Premises used: ComplexShape.Embedding.homRestrict_f, HomologicalComplex.restrictionXIso, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L L' : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
h :
  ∀ (i : ι),
    Eq (α := (K.restriction e).X i ⟶ L'.X i) (Hom.f (e.homRestrict (ψ ≫ extendMap β e)) i)
      (Hom.f (e.homRestrict ψ ≫ β) i)
⊢ Eq (α := K.restriction e ⟶ L') (e.homRestrict (ψ ≫ extendMap β e)) (e.homRestrict ψ ≫ β)

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
L L' : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
β : L ⟶ L'
i : ι
⊢ Eq (α := (K.restriction e).X i ⟶ L'.X i) (Hom.f (e.homRestrict (ψ ≫ extendMap β e)) i) (Hom.f (e.homRestrict ψ ≫ β) i)

Tactic:
simp [homRestrict_f _ _ rfl, extendMap_f β e rfl]

Premises used: HomologicalComplex.extendMap_f, ComplexShape.Embedding.homRestrict_f, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K K' : HomologicalComplex.{v_1, u_3, u_2} C c'
L L' : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
ψ : K ⟶ L.extend e
⊢ (fun (φ : { φ : K.restriction e ⟶ L // e.HasLift φ }) ↦ (e.liftExtend (↑φ : K.restriction e ⟶ L) ⋯ : K ⟶ L.extend e))
      ((fun (ψ : K ⟶ L.extend e) ↦
          (Subtype.mk (p := fun (φ : K.restriction e ⟶ L) ↦ e.HasLift φ) (e.homRestrict ψ) ⋯ :
            { φ : K.restriction e ⟶ L // e.HasLift φ }))
        ψ) =
    ψ

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.HomEquiv
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K K' : HomologicalComplex.{v_1, u_3, u_2} C c'
L L' : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : e.IsRelIff
φ : { φ : K.restriction e ⟶ L // e.HasLift φ }
⊢ (fun (ψ : K ⟶ L.extend e) ↦
        (Subtype.mk (p := fun (φ : K.restriction e ⟶ L) ↦ e.HasLift φ) (e.homRestrict ψ) ⋯ :
          { φ : K.restriction e ⟶ L // e.HasLift φ }))
      ((fun (φ : { φ : K.restriction e ⟶ L // e.HasLift φ }) ↦
          (e.liftExtend (↑φ : K.restriction e ⟶ L) ⋯ : K ⟶ L.extend e))
        φ) =
    φ

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_1, u_3} (K.X i')

Tactic:
IsStrictlySupported.isZero i' hi'

Premises used: HomologicalComplex.IsStrictlySupported.isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
⊢ K.op.IsStrictlySupported e.op ↔ K.IsStrictlySupported e

Tactic:
⟨(fun _ ↦ ⟨fun i' hi' ↦ (K.op.isZero_X_of_isStrictlySupported e.op i' hi').unop⟩),
    (fun _ ↦ ⟨fun i' hi' ↦ (K.isZero_X_of_isStrictlySupported e i' hi').op⟩)⟩

Premises used: CategoryTheory.Limits.IsZero.op, HomologicalComplex.op, HomologicalComplex.IsStrictlySupported.mk, ComplexShape.Embedding.op, Iff.intro, HomologicalComplex.isZero_X_of_isStrictlySupported, CategoryTheory.Limits.IsZero.unop
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst_2 rw : K.IsStrictlySupported e
⊢ K.op.IsStrictlySupported e.op

Tactic:
rw [isStrictlySupported_op_iff]

Premises used: HomologicalComplex.isStrictlySupported_op_iff
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst_2 : K.IsStrictlySupported e
⊢ K.IsStrictlySupported e

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : K.IsSupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ K.ExactAt i'

Tactic:
IsSupported.exactAt i' hi'

Premises used: HomologicalComplex.IsSupported.exactAt
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : ∀ (i : ι'), K.HasHomology i
inst_3 : ∀ (i : ι'), L.HasHomology i
inst_4 : QuasiIso φ
⊢ K.IsSupported e ↔ L.IsSupported e

Tactic:
simp [isSupported_iff, exactAt_iff_of_quasiIsoAt φ]

Premises used: exactAt_iff_of_quasiIsoAt, HomologicalComplex.isSupported_iff
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst_2 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (K.sc i').Exact

Tactic:
ShortComplex.exact_of_isZero_X₂ _ (K.isZero_X_of_isStrictlySupported e i' hi')

Premises used: HomologicalComplex.isZero_X_of_isStrictlySupported, CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst_2 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (K.sc i').Exact

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (K.isZero_X_of_isStrictlySupported e i' hi')

Premises used: CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
⊢ K.op.IsSupported e.op ↔ K.IsSupported e

Tactic:
⟨fun _ ↦ ⟨fun i' hi' ↦ (K.op.exactAt_of_isSupported e.op i' hi').unop⟩,
    fun _ ↦ ⟨fun i' hi' ↦ (K.exactAt_of_isSupported e i' hi').op⟩⟩

Premises used: HomologicalComplex.op, HomologicalComplex.IsSupported.mk, HomologicalComplex.exactAt_of_isSupported, ComplexShape.Embedding.op, Iff.intro, HomologicalComplex.ExactAt.op, HomologicalComplex.ExactAt.unop
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
⊢ K.op.IsStrictlySupportedOutside e.op ↔ K.IsStrictlySupportedOutside e

Tactic:
⟨fun h ↦ ⟨fun i ↦ (h.isZero i).unop⟩, fun h ↦ ⟨fun i ↦ (h.isZero i).op⟩⟩

Premises used: CategoryTheory.Limits.IsZero.op, HomologicalComplex.IsStrictlySupportedOutside.isZero, HomologicalComplex.IsStrictlySupportedOutside.mk, Iff.intro, CategoryTheory.Limits.IsZero.unop
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
⊢ K.op.IsSupportedOutside e.op ↔ K.IsSupportedOutside e

Tactic:
⟨fun h ↦ ⟨fun i ↦ (h.exactAt i).unop⟩, fun h ↦ ⟨fun i ↦ (h.exactAt i).op⟩⟩

Premises used: HomologicalComplex.IsSupportedOutside.exactAt, HomologicalComplex.IsSupportedOutside.mk, Iff.intro, HomologicalComplex.ExactAt.op, HomologicalComplex.ExactAt.unop
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
mp : IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
mpr : K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K
⊢ IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
mp : K.IsStrictlySupported e
mp₁ : K.IsStrictlySupportedOutside e
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
mp : ∀ (i' : ι') (hi' : ∀ (i : ι), e.f i ≠ i'), IsZero.{v_1, u_3} (K.X i')
⊢ K.IsStrictlySupported e

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_1, u_3} (K.X i')

Tactic:
(eval _ _ _).map_isZero hK

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_1, u_3} (K.X i')

Tactic:
exact (eval _ _ _).map_isZero hK

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
mp : ∀ (i : ι), IsZero.{v_1, u_3} (K.X (e.f i))
⊢ K.IsStrictlySupportedOutside e

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
i : ι
⊢ IsZero.{v_1, u_3} (K.X (e.f i))

Tactic:
(eval _ _ _).map_isZero hK

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
hK : IsZero K
i : ι
⊢ IsZero.{v_1, u_3} (K.X (e.f i))

Tactic:
exact (eval _ _ _).map_isZero hK

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
mpr : Eq (α := K ⟶ K) (𝟙 K) 0
⊢ IsZero K

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
mpr : ∀ (n : ι'), Hom.f (𝟙 K) n = Hom.f 0 n
⊢ Eq (α := K ⟶ K) (𝟙 K) 0

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
mpr : IsZero.{v_1, u_3} (K.X n)
⊢ Hom.f (𝟙 K) n = Hom.f 0 n

Tactic:
apply IsZero.eq_of_src

Premises used: CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
pos : ∀ (hn : ∃ (i : ι), e.f i = n), IsZero.{v_1, u_3} (K.X n)
neg : ∀ (hn : ¬∃ (i : ι), e.f i = n), IsZero.{v_1, u_3} (K.X n)
⊢ IsZero.{v_1, u_3} (K.X n)

Tactic:
by_cases hn : ∃ i, e.f i = n
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ∃ (i : ι), e.f i = n
pos : ∀ (i : ι), IsZero.{v_1, u_3} (K.X (e.f i))
⊢ IsZero.{v_1, u_3} (K.X n)

Tactic:
obtain ⟨i, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
i : ι
⊢ IsZero.{v_1, u_3} (K.X (e.f i))

Tactic:
h₂.isZero i

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
i : ι
⊢ IsZero.{v_1, u_3} (K.X (e.f i))

Tactic:
exact h₂.isZero i

Premises used: HomologicalComplex.IsStrictlySupportedOutside.isZero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ (i : ι), e.f i = n
⊢ ∀ (i : ι), e.f i ≠ n

Tactic:
simpa using hn
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ (i : ι), e.f i = n
⊢ IsZero.{v_1, u_3} (K.X n)

Tactic:
exact K.isZero_X_of_isStrictlySupported e _ (by simpa using hn)

Premises used: HomologicalComplex.isZero_X_of_isStrictlySupported
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
rw :
  Eq.{v_2 + 1} (α :=
    X (Functor.obj (F.mapHomologicalComplex c') K) i' ⟶ X (Functor.obj (F.mapHomologicalComplex c') K) i')
    (𝟙 (X (Functor.obj (F.mapHomologicalComplex c') K) i')) 0
⊢ IsZero.{v_2, u_4} (X (Functor.obj (F.mapHomologicalComplex c') K) i')

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
dsimp : Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (𝟙 (F.obj (K.X i'))) 0
⊢ Eq.{v_2 + 1} (α :=
    X (Functor.obj (F.mapHomologicalComplex c') K) i' ⟶ X (Functor.obj (F.mapHomologicalComplex c') K) i')
    (𝟙 (X (Functor.obj (F.mapHomologicalComplex c') K) i')) 0

Tactic:
dsimp