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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsGE (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₃ n

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsLE ((t.triangleLTGE n).obj Y).obj₁ (n - 1)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
⊢ t.IsGE ((t.triangleLTGE n).obj Y).obj₃ n

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
⊢ t.IsGE ((t.triangleLTGE n₁).obj Y).obj₃ n₁

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
⊢ t.IsLE (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h).obj₁ n₀

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
⊢ t.IsGE (Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h).obj₃ n₁

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
inst✝ : t.IsLE X b
⊢ t.IsLE ((t.truncLT a).obj X) b

Tactic:
by
  by_cases h : a ≤ b + 1
  · exact t.isLE_truncLT_obj ..
  · have := (t.isLE_iff_isIso_truncLTι_app (a - 1) a (by lia) X).1 (t.isLE_of_le _ b _ (by lia))
    exact t.isLE_of_iso (show X ≅ _ from (asIso ((t.truncLTι a).app X)).symm) _

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
⊢ t.IsGE ((t.truncGELT a b).obj X) a

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
a b : ℤ
⊢ t.IsLE ((t.truncLTGE a b).obj X) (b - 1)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj T.obj₁)
mem : Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE (Triangle.mk H.m₁ H.m₃ (T.mor₃ ≫ (shiftFunctor C 1).map ((t.truncGEπ n).app T.obj₁))).obj₁ n

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₃ : t.IsGE T.obj₃ n
Z : C
g : T.obj₂ ⟶ Z
k : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj T.obj₁)
mem : Triangle.mk ((t.truncLTι n).app T.obj₁ ≫ T.mor₁) g k ∈ distinguishedTriangles
H : Octahedron ⋯ ⋯ hT mem := someOctahedron ⋯ ⋯ hT mem
⊢ t.IsGE (Triangle.mk H.m₁ H.m₃ (T.mor₃ ≫ (shiftFunctor C 1).map ((t.truncGEπ n).app T.obj₁))).obj₃ n

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsGE X a
⊢ t.IsGE ((t.triangleLTGE b).obj X).obj₃ a

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsLE X b
⊢ t.IsLE ((t.triangleLTGE a).obj X).obj₁ b

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a b : ℤ
⊢ t.IsLE ((t.truncGELT a b).obj X) (b - 1)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a b : ℤ
⊢ t.IsGE ((t.truncLTGE a b).obj X) a

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
⊢ t.IsGE
    (Triangle.mk H.m₁ H.m₃
        ((t.truncGEδLT b).app X ≫ (shiftFunctor C 1).map (((t.truncLT b).whiskerLeft (t.truncGEπ a)).app X))).obj₃
    b

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip✝ : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this : ∀ (n : ℤ), Injective ((kernel p).X n)
⊢ sq.HasLift

Tactic:
have : (kernel p).IsKInjective := by
      obtain ⟨d, hd⟩ := hX
      have : (kernel p).IsStrictlyGE d := by
        rw [isStrictlyGE_iff]
        intro i hi
        rw [IsZero.iff_id_eq_zero, ← cancel_mono ((kernel.ι p).f i)]
        apply (X.isZero_of_isStrictlyGE d i).eq_of_tgt
      exact isKInjective_of_injective _ d

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip✝ : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝¹ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝ : ∀ (n : ℤ), Injective ((kernel p).X n)
this : (kernel p).IsKInjective
⊢ sq.HasLift
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝² : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝¹ : ∀ (n : ℤ), Injective ((kernel p).X n)
this✝ : (kernel p).IsKInjective
h✝ : QuasiIso i
this : { X₁ := A, X₂ := B, X₃ := cokernel i, f := i, g := cokernel.π i, zero := ⋯ }.ShortExact
⊢ QuasiIso { X₁ := A, X₂ := B, X₃ := cokernel i, f := i, g := cokernel.π i, zero := ⋯ }.f

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝³ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝² : ∀ (n : ℤ), Injective ((kernel p).X n)
this✝¹ : (kernel p).IsKInjective
h✝ : QuasiIso p
this✝ : Epi p
this : { X₁ := kernel p, X₂ := X, X₃ := Y, f := kernel.ι p, g := p, zero := ⋯ }.ShortExact
⊢ QuasiIso { X₁ := kernel p, X₂ := X, X₃ := Y, f := kernel.ι p, g := p, zero := ⋯ }.g

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n : ℤ
⊢ degreewiseEpiWithInjectiveKernel (π f n)

Tactic:
intro i
  rw [epiWithInjectiveKernel_iff]
  exact ⟨_, inferInstance, (mappingCocone.inr (α f n)).1.v (i - 1) i (by lia), by simp,
    ⟨{r := (mappingCocone.snd (α f n)).v _ _ (by lia)
      s := (mappingCocone.inl (α f n)).v _ _ (by lia)
      id := (add_comm _ _).trans (by simp [mappingCocone.id_X]) }⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X : FibrantObject C
⊢ IsFibrant ((localizerMorphism C).functor.obj X)

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
hi' : i + 1 < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯,
        g := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.f (i + 1),
        zero := ⋯ }.g

pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯,
        g := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.f (i + 1),
        zero := ⋯ }.g

Tactic:
· have := hf (i + 1) (by lia)
      infer_instance

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯,
        g := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.f (i + 1),
        zero := ⋯ }.g
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
inst✝ : Mono f
n₀ n₁ : ℤ
hf : ∀ i ≤ n₀, QuasiIsoAt f i
hn₁ : n₀ + 1 = n₁
F₁ : (cofFib f).FullSubcategory
h₁ : quasiIsoLE n₀ F₁
h₂ : isIsoLE n₀ F₁
right✝ : Mono (homologyMap F₁.obj.ι n₁)
F₂ : (cofFib F₁.obj.ι).FullSubcategory
h₃ : quasiIsoLE n₁ F₂
h₄ : isIsoLE n₁ F₂
⊢ Mono { mid := F₂.obj.mid, ι := F₂.obj.ι, π := F₂.obj.π ≫ F₁.obj.π, ι_π := ⋯ }.ι

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀ : ℤ
F : CofFibFactorizationQuasiIsoLE f n₀
n₁ : ℤ
hn₁ : n₀ + 1 = n₁
F₁₂ : (cofFib F.obj.obj.ι).FullSubcategory
h₁ : quasiIsoLE n₁ F₁₂
h₂ : isIsoLE n₀ F₁₂
⊢ Mono { mid := F₁₂.obj.mid, ι := F₁₂.obj.ι, π := F₁₂.obj.π ≫ F.obj.obj.π, ι_π := ⋯ }.ι

Tactic:
dsimp; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H✝ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H✝
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H✝
B : C ⥤ H✝
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : S → CostructuredArrowDownwards e.hom g := fun s ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv ↑s ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ s, Nonempty (Z s ⟶ A)
s₀ : S
f₀ : Z s₀ ⟶ A₀
s₁ : S
f₁ : Z s₁ ⟶ A₁
P : Precylinder X₀
hP : T.map P.i₀ = T.map P.i₁
h : (P.map L).LeftHomotopy ↑s₀ ↑s₁
Z' : CostructuredArrowDownwards e.hom g := CostructuredArrowDownwards.mk e.hom g P.I (e₀.inv ≫ T.map P.i₀) h.h ⋯
⊢ (structuredArrowDownwards e.hom Y₀).map (StructuredArrow.homMk P.i₀ ⋯) ≫ CostructuredArrow.hom Z' =
    CostructuredArrow.hom (Z s₀)

Tactic:
simp [Z, Z', dsimp% h.h₀]

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

Goal state before:
pp: case hP₂
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
W : MorphismProperty C
inst✝ : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk g.hom.op
Y₁✝ Y₂✝ : Cᵒᵖ
w : Y₁✝ ⟶ Y₂✝
hw : W.op w
φ : L.op.obj (op Y) ⟶ L.op.obj Y₂✝
hφ : P (CostructuredArrow.mk (StructuredArrow.mk φ).hom.unop)
⊢ P (CostructuredArrow.mk (StructuredArrow.mk (φ ≫ (isoOfHom L.op W.op w hw).inv)).hom.unop)

Tactic:
| hP₂ w hw φ hφ =>

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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
inst✝ : EnoughInjectives C
K : FibrantObject (Plus C)
n : ℤ
⊢ isInjective C (((FibrantObject.ι ⋙ ι C).obj K).X n)

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.EulerCharSigns
i j : ι
h : c.Rel i j
⊢ c.χ i = -c.χ j

Tactic:
by simp [c.χ_next h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
⊢ (Function.support fun x ↦ ↑(Module.finrank R ↑(X x))) = Function.support fun i ↦ Module.finrank R ↑(X i)

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
i : ι
⊢ (i ∈ Function.support fun x ↦ ↑(Module.finrank R ↑(X x))) ↔ i ∈ Function.support fun i ↦ Module.finrank R ↑(X i)
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
⊢ { f := fun i ↦ (C.X i).map (𝟙 t), comm' := ⋯ } =
    𝟙 { X := fun i ↦ (C.X i).obj t, d := fun i j ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }

Tactic:
ext i

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ { f := fun i ↦ (C.X i).map (𝟙 t), comm' := ⋯ }.f i =
    (𝟙 { X := fun i ↦ (C.X i).obj t, d := fun i j ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }).f i
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
⊢ { f := fun i ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ } =
    { f := fun i ↦ (C.X i).map h₁, comm' := ⋯ } ≫ { f := fun i ↦ (C.X i).map h₂, comm' := ⋯ }

Tactic:
ext i

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ { f := fun i ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ }.f i =
    ({ f := fun i ↦ (C.X i).map h₁, comm' := ⋯ } ≫ { f := fun i ↦ (C.X i).map h₂, comm' := ⋯ }).f i