mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : ∀ (i : ι'), K.HasHomology i
inst✝¹ : ∀ (i : ι'), L.HasHomology i
inst✝ : QuasiIso φ
⊢ K.IsSupported e ↔ L.IsSupported e

Tactic:
by
  simp [isSupported_iff, exactAt_iff_of_quasiIsoAt φ]

Goal state after:
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).op = 0

Tactic:
X.shape j i hij,

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c
i j : ι
hij : ¬c.symm.Rel i j
⊢ Quiver.Hom.op 0 = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c.symm
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).op = 0

Tactic:
X.shape j i hij,

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c.symm
i j : ι
hij : ¬c.Rel i j
⊢ Quiver.Hom.op 0 = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex Vᵒᵖ c
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).unop = 0

Tactic:
X.shape j i hij,

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex Vᵒᵖ c
i j : ι
hij : ¬c.symm.Rel i j
⊢ Quiver.Hom.unop 0 = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex Vᵒᵖ c.symm
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).unop = 0

Tactic:
X.shape j i hij,

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex Vᵒᵖ c.symm
i j : ι
hij : ¬c.Rel i j
⊢ Quiver.Hom.unop 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ (XOpIso K (some i)).hom ≫ (d K (some j) (some i)).op = d K.op (some i) (some j) ≫ (XOpIso K (some j)).hom

Tactic:
dsimp [XOpIso]
      simp only [d_eq _ rfl rfl, op_comp, assoc, id_comp, comp_id]
      rfl

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

Tactic:
· obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

Tactic:
· obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Tactic:
· obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'

Tactic:
· obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ + φ') e).f i' = (extendMap φ e + extendMap φ' e).f i'
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : 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✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
hj' : ∃ j, e.f j = j'
⊢ 0 = K.d i' j' ≫ f φ j'

Tactic:
obtain ⟨j, rfl⟩ := hj'

Goal state after:
case pos
ι : 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✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ f φ (e.f j)
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
i : ι
hi : e.f i = c'.prev j'
⊢ Epi ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f (c'.prev j'))

Tactic:
e.epi_liftExtend_f_iff _ _ hi

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
i : ι
hi : e.f i = c'.prev j'
⊢ Epi ((K.restrictionToTruncGE' e).f i)
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.homologyι j' =
    (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv ≫
      (K.restriction e).homologyι j ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom

Tactic:
restrictionHomologyIso_inv_homologyι_assoc,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.homologyι j' =
    K.homologyι j' ≫
      (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
i' : ι'
i : ι
hi : e.f i = i'
⊢ Epi ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f i')

Tactic:
e.epi_liftExtend_f_iff _ _ hi

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
i' : ι'
i : ι
hi : e.f i = i'
⊢ Epi ((K.restrictionToTruncGE' e).f i)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
hj' : ∃ j, e.f j = j'
⊢ QuasiIsoAt (extendMap φ e) j'

Tactic:
obtain ⟨j, rfl⟩ := hj'

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j : ι
⊢ QuasiIsoAt (extendMap φ e) (e.f j)
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁷ : Category.{v_1, u_3} C
inst✝⁶ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
i : ι
hi : e.f i = i'
hi''' : e.BoundaryGE i
⊢ K.pOpcycles i' ≫ ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''').inv ≫ 𝟙 ((K.truncGE e).X i') =
    K.pOpcycles i' ≫ ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''').inv ≫ 0

Tactic:
apply (K.isZero_X_of_isStrictlySupported e' i' hi').eq_of_src

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
hK : K.IsSupportedOutside e
i : ι
⊢ (K.truncGE e).ExactAt (e.f i)

Tactic:
simpa only [← exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK.exactAt i

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case mpr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
a✝ : K.IsSupported e₂
⊢ K.IsSupportedOutside e₁

Tactic:
exact ⟨fun i₁ => K.exactAt_of_isSupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
⊢ K.IsStrictlyGE n

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

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
⊢ K.IsStrictlyLE n

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

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j ≫ opcyclesMap ((single C c j).map f) j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom

Tactic:
p_opcyclesMap,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).map f).f j ≫ ((single C c j).obj B).pOpcycles j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
inst✝² : Injective (K.X n₀)
inst✝¹ : Injective (K.X n₁)
inst✝ : K.IsStrictlyGE n₀
hK : ExactAt K n₀
h : n₀ + 1 = n₁
⊢ Injective (opcycles K n₁)

Tactic:
let S : ShortComplex C := ShortComplex.mk (K.d n₀ n₁) (K.pOpcycles n₁) (by simp)

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
inst✝² : Injective (K.X n₀)
inst✝¹ : Injective (K.X n₁)
inst✝ : K.IsStrictlyGE n₀
hK : ExactAt K n₀
h : n₀ + 1 = n₁
S : ShortComplex C :=
  { X₁ := K.X n₀, X₂ := K.X n₁, X₃ := opcycles K n₁, f := K.d n₀ n₁, g := pOpcycles K n₁, zero := ⋯ }
⊢ Injective (opcycles K n₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HasExt C

Tactic:
rw [hasExt_iff.{w}]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (mk₀ f).comp (mk₀ g) ⋯ = mk₀ (f ≫ g)

Tactic:
let := HasDerivedCategory.standard C; ext; simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
⊢ (mk₀ (𝟙 X)).comp α ⋯ = α

Tactic:
let := HasDerivedCategory.standard C; ext; simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α

Tactic:
let := HasDerivedCategory.standard C; ext; simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁) ≫
      ((Functor.commShiftIso Q 1).app S₂.X₁).hom =
    (((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
          inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
        Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      ((Functor.commShiftIso Q 1).app S₂.X₁).hom

Tactic:
Iso.cancel_iso_hom_right,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Q.map (CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1 ⋙ Q).map f.τ₁ =
    ((Q.map (CochainComplex.mappingCone.descShortComplex S₁) ≫ Q.map f.τ₃) ≫
        inv (Q.map (CochainComplex.mappingCone.descShortComplex S₂))) ≫
      Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ AddCommGrpCat.ofHom ((Ext.mk₀ (f ≫ f')).postcomp X ⋯) =
    AddCommGrpCat.ofHom ((Ext.mk₀ f).postcomp X ⋯) ≫ AddCommGrpCat.ofHom ((Ext.mk₀ f').postcomp X ⋯)

Tactic:
ext α

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
α : ↑(AddCommGrpCat.of (Ext X X✝ n))
⊢ (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ((Ext.mk₀ (f ≫ f')).postcomp X ⋯))) α =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom ((Ext.mk₀ f).postcomp X ⋯) ≫ AddCommGrpCat.ofHom ((Ext.mk₀ f').postcomp X ⋯)))
      α
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (extFunctorObj (Opposite.unop X₁) n).map g ≫
      AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) =
    AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫
      (extFunctorObj (Opposite.unop X₂) n).map g

Tactic:
ext α

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ (AddCommGrpCat.Hom.hom
        ((extFunctorObj (Opposite.unop X₁) n).map g ≫
          AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯)))
      α =
    (AddCommGrpCat.Hom.hom
        (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫
          (extFunctorObj (Opposite.unop X₂) n).map g))
      α
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ (shiftFunctorZero (OppositeShift C A) A).hom.app X = ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op

Tactic:
rw [← cancel_mono ((shiftFunctorZero (OppositeShift C A) A).inv.app X),
    Iso.hom_inv_id_app, oppositeShiftFunctorZero_inv_app, ← op_comp,
    Iso.hom_inv_id_app, op_id]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) = 𝟙 (Opposite.op ((shiftFunctor C 0).obj (Opposite.unop X)))