mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
        inv (L.mapTriangle.map ψ)).hom₁ =
    a

Tactic:
← cancel_mono (L.mapTriangle.map ψ).hom₁,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
          inv (L.mapTriangle.map ψ)).hom₁ ≫
      (L.mapTriangle.map ψ).hom₁ =
    a ≫ (L.mapTriangle.map ψ).hom₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact

Tactic:
rw [distinguished_iff_iso_trianglehOfDegreewiseSplit] at hT

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℤ
T : Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT✝ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
hT : ∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)
⊢ ∃ T' e, ((Pretriangulated.shortComplexOfDistTriangle T' ⋯).map (homologyFunctor C (ComplexShape.up ℤ) n)).Exact
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₂₃ + a₁ = a

Tactic:
rw [← h₂₃, h]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
x✝ : IsIso g
⊢ f ≫ Arrow.Hom.right h.i ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X

Tactic:
← h.i_w_assoc,

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
x✝ : IsIso g
⊢ Arrow.Hom.left h.i ≫ g ≫ inv g ≫ Arrow.Hom.left h.r = 𝟙 X
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
X Y Z : C
inst✝ : Preadditive C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
rw [comp, comp, comp, Preadditive.add_comp]

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

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ i

pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i

Tactic:
· intro
    exact quasiIsoAt_of_comp_right φ φ' i

Goal state after:
case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ : HomologicalComplex C c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : QuasiIso f
hfg : QuasiIso (f ≫ g)
⊢ QuasiIso g

Tactic:
rwa [← quasiIso_iff_comp_left f g]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ quasiIso C (ComplexShape.up ℤ) = (subcategoryAcyclic C).trW

Tactic:
by
  ext K L f
  exact ((homologyFunctor C (ComplexShape.up ℤ) 0).mem_homologicalKernel_trW_iff f).symm

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
q r : ℤ
hr : q + m = r
hpq : q + -1 + 1 = q
⊢ (↑(inr φ)).v (q + -1) q hpq ≫ (descCochain φ α β h).v q r hr = β.v (q + -1) r ⋯

Tactic:
simp [inr, descCochain, mappingCocone, smul_smul,
    Cochain.rightShift_v _ _ _ _ _ _ hpq _ (add_zero (q + -1)),
    Cochain.leftShift_v (n := n) _ _ _ _ _ r _ (q + -1) (by lia)]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ ((homologyFunctor C 0).shift a).map ((quotientCompQhIso C).inv.app K) ≫
      (homologyFunctor C 0).shiftMap ((ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ))).map Qh) a a'
          h ≫
        ((homologyFunctor C 0).shift a').map ((quotientCompQhIso C).hom.app L) =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L

Tactic:
shiftMap_homologyFunctor_map_Qh ..,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ ((homologyFunctor C 0).shift a).map ((quotientCompQhIso C).inv.app K) ≫
      ((homologyFunctorFactorsh C a).hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ≫
          (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap
              (ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ))) a a' ⋯ ≫
            (homologyFunctorFactorsh C a').inv.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)) ≫
        ((homologyFunctor C 0).shift a').map ((quotientCompQhIso C).hom.app L) =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L
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)ᵒᵖ
⊢ (unopFunctor V c).map ((unopUnitIso V c).hom.app X) ≫ (unopCounitIso V c).hom.app ((unopFunctor V c).obj X) =
    𝟙 ((unopFunctor V c).obj X)

Tactic:
by
    ext
    simp only [comp_f]
    exact Category.comp_id _

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ φ₁.f n = ((((dNext n) fun i j ↦ (h.hom j i).op) + (prevD n) fun i j ↦ (h.hom j i).op) + (φ₂.f n).op).unop

Tactic:
rw [h.comm n]

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (dNext n) h.hom + (prevD n) h.hom + φ₂.f n =
    ((((dNext n) fun i j ↦ (h.hom j i).op) + (prevD n) fun i j ↦ (h.hom j i).op) + (φ₂.f n).op).unop
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ φ₁.f n = ((((dNext n) fun i j ↦ (h.hom j i).unop) + (prevD n) fun i j ↦ (h.hom j i).unop) + (φ₂.f n).unop).op

Tactic:
rw [h.comm n]

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (dNext n) h.hom + (prevD n) h.hom + φ₂.f n =
    ((((dNext n) fun i j ↦ (h.hom j i).unop) + (prevD n) fun i j ↦ (h.hom j i).unop) + (φ₂.f n).unop).op
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
⊢ (K.extend e).d i' j' = 0

Tactic:
obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
  · exact extend.d_none_eq_zero' _ _ _ hj'
  · rw [extend_d_eq K e hi (e.f_eq_of_r_eq_some hj), K.shape, zero_comp, comp_zero]
    intro hij
    obtain rfl := c.next_eq' hij
    exact hi' hij

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

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.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)
this : Epi φ.τ₁
⊢ IsIso ((e.liftExtend (K.restrictionToTruncGE' e) ⋯).f j')

Tactic:
e.isIso_liftExtend_f_iff _ _ hj'

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.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)
this : Epi φ.τ₁
⊢ IsIso ((K.restrictionToTruncGE' e).f j)
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

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✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ (truncLE'Map φ e).f i = (K.truncLE'XIsoCycles e h hi).hom ≫ cyclesMap φ i' ≫ (L.truncLE'XIsoCycles e h hi).inv

Tactic:
by
  apply Quiver.Hom.op_inj
  dsimp [truncLE'Map, truncLE'XIsoCycles]
  rw [assoc, assoc, truncGE'Map_f_eq_opcyclesMap _ e.op (by simpa) h,
    opcyclesOpIso_inv_naturality_assoc, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ ac.desc x₁ x₂ (e₁.f i₁) = x₁ i₁

Tactic:
by
  dsimp [desc]
  rw [ac.desc'_inl _ _ _ i₁ (ac.equiv.injective (by simp)), desc.aux_trans]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ K.IsGE p

Tactic:
rw [isGE_iff]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ ∀ i < p, ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ QuasiIso (truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Tactic:
by
  rw [HomologicalComplex.quasiIso_truncGEMap_iff]
  constructor
  · intro h i hi
    obtain ⟨k, rfl⟩ := Int.le.dest hi
    exact h k _ rfl
  · rintro h i i' rfl
    exact h _ (by dsimp; lia)

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsGE n
a n' : ℤ
h : a + n' = n
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsGE n'

Tactic:
rw [isGE_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsGE n
a n' : ℤ
h : a + n' = n
⊢ ∀ i < n', ExactAt ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : n < i
⊢ (embeddingUpIntGE n).f (i - n).natAbs = i

Tactic:
by
      dsimp
      rw [Int.natAbs_of_nonneg (by lia), add_sub_cancel]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
D : Type u₂
inst✝¹² : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝¹¹ : AddMonoid M
inst✝¹⁰ : HasShift C M
inst✝⁹ : HasShift D M
inst✝⁸ : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst✝⁷ : HasSmallLocalizedShiftedHom W M X Y
inst✝⁶ : HasSmallLocalizedShiftedHom W M X Z
inst✝⁵ : HasSmallLocalizedShiftedHom W M X T
inst✝⁴ : HasSmallLocalizedShiftedHom W M Y Z
inst✝³ : HasSmallLocalizedShiftedHom W M Y T
inst✝² : HasSmallLocalizedShiftedHom W M Z T
inst✝¹ : HasSmallLocalizedShiftedHom W M Z Z
inst✝ : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₂₃ + a₁ = a

Tactic:
rw [← h₂₃, h]

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

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
⊢ Epi ((composableArrows₂ S₁ i).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)

Tactic:
have := hS₁.epi_g

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₁.g
⊢ Epi ((composableArrows₂ S₁ i).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.f =
    0

Tactic:
simp [← cancel_epi (HomologicalComplex.homologyMap S.f i),
        ← HomologicalComplex.homologyMap_comp]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
hx₂' : x₂' ≫ K.d j k = 0
⊢ K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j = K.liftCycles x₂' k hk hx₂' ≫ K.homologyπ j ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d i j

Tactic:
by
  subst hi hk
  exact (K.sc j).liftCycles_comp_homologyπ_eq_iff_up_to_refinements x₂ x₂' hx₂ hx₂'

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

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

Tactic:
rw [CategoryTheory.Functor.map_id, comp_id, IsIso.hom_inv_id_assoc]

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
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext c.pt Y n
⊢ (mk₀ (∑ i, c.π i ≫ c.ι i)).comp x ⋯ = x

Tactic:
IsBilimit.total hc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext c.pt Y n
⊢ (mk₀ (𝟙 c.pt)).comp x ⋯ = x
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: case e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ (shiftMonoidalFunctor C B).map (eqToHom ⋯) = (pullbackShiftIso C φ 0 0 ⋯).inv

Tactic:
apply eqToHom_map

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: case e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ : A
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftMonoidalFunctor C B).map (eqToHom ⋯) = (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv

Tactic:
apply eqToHom_map

Goal state after: