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
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:
by 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:
by 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:
by 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:
by 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:
by dsimp; infer_instance

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

Goal state before:
pp: case pos
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 ⋯ ⋯ ⋯
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
let m₁ : (t.truncGELT a b).obj X ⟶ _ := H.m₁

Goal state after:
case pos
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₁
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
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 Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i✝ : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i✝)
hi✝ : Mono i✝
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
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)
d : ℤ
hd : X.IsStrictlyGE d
inst✝ : Fibration (ObjectProperty.homMk p)
hip : WeakEquivalence (ObjectProperty.homMk i✝) ∨ WeakEquivalence (ObjectProperty.homMk p)
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i✝) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
i : ℤ
hi : autoParam (i < d) isStrictlyGE_iff._auto_1
⊢ 𝟙 ((kernel p).X i) = 0

Tactic:
← cancel_mono ((kernel.ι p).f i)

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 Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i✝ : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i✝)
hi✝ : Mono i✝
p : X ⟶ Y
hp : degreewiseEpiWithInjectiveKernel p
t : A ⟶ X
b : B ⟶ Y
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)
d : ℤ
hd : X.IsStrictlyGE d
inst✝ : Fibration (ObjectProperty.homMk p)
hip : WeakEquivalence (ObjectProperty.homMk i✝) ∨ WeakEquivalence (ObjectProperty.homMk p)
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i✝) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
i : ℤ
hi : autoParam (i < d) isStrictlyGE_iff._auto_1
⊢ 𝟙 ((kernel p).X i) ≫ (kernel.ι p).f i = 0 ≫ (kernel.ι p).f i
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:
by 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 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:
by dsimp; infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : HasInitial C
inst✝² : CategoryWithWeakEquivalences C
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsCofibrant Y
f : X ⟶ Y
⊢ WeakEquivalence (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]
  rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithFibrations C
inst✝³ : HasTerminal C
inst✝² : CategoryWithWeakEquivalences C
X Y : C
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ WeakEquivalence (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]
  rfl

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

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
inst✝⁸ : CategoryWithCofibrations C
inst✝⁷ : HasInitial C
inst✝⁶ : CategoryWithFibrations C
inst✝⁵ : HasTerminal C
inst✝⁴ : CategoryWithWeakEquivalences C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsFibrant X
inst✝¹ : IsCofibrant Y
inst✝ : IsFibrant Y
f : X ⟶ Y
⊢ WeakEquivalence (homMk f) ↔ WeakEquivalence f

Tactic:
simp only [weakEquivalence_iff]
  rfl

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h : (fun f ↦ f.postcomp g) (mk f₀) = (fun f ↦ f.postcomp g) (mk f₁)
⊢ mk f₀ = mk f₁

Tactic:
simp only [postcomp_mk, mk_eq_mk_iff] at h

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
⊢ mk f₀ = mk f₁
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:
by dsimp; infer_instance

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

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
⊢ QuasiIsoAt (π K L n₁) i

Tactic:
quasiIsoAt_iff' _ (i - 1) i (i + 1) (by simp) (by simp)

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁))
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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
this : QuasiIsoAt (π K L n₁) i
⊢ QuasiIsoAt (ι f n₁) i

Tactic:
← quasiIsoAt_iff_comp_right _ (π K L n₁),

Goal state after:
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₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
hf : ∀ i ≤ n₀, QuasiIsoAt f i
i : ℤ
hi : i ≤ n₀
this : QuasiIsoAt (π K L n₁) i
⊢ QuasiIsoAt (ι f n₁ ≫ π K L n₁) i
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h✝ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject Z
left✝ : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
sq : CommSq h.h f P.p (prod.lift f₀ f₁)
⊢ sq.lift ≫ P.p₀ = f₀

Tactic:
have := sq.fac_right =≫ prod.fst
          rwa [Category.assoc, P.p_fst, prod.lift_fst] at this

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
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let G : H ⥤ Hfib := (HoCat.localizerMorphismResolution C).localizedFunctor L Lfibπ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hfib : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lfibπ : HoCat C ⥤ Hfib := (weakEquivalences (HoCat C)).Q
Lfib : FibrantObject C ⥤ Hfib := toHoCat ⋙ Lfibπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hfib ⥤ H := (localizerMorphism C).localizedFunctor Lfib L
eF : ι ⋙ L ≅ Lfib ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lfib L F
eF' : HoCat.toLocalization L ≅ Lfibπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lfibπ F)
G : H ⥤ Hfib := (HoCat.localizerMorphismResolution C).localizedFunctor L Lfibπ
⊢ (localizerMorphism C).IsLocalizedEquivalence
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:
by 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:
by dsimp; infer_instance

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:
by dsimp; infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
S : ShortComplex C
hS : S.ShortExact
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃ ≫
      ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        (shiftFunctor (DerivedCategory D) ↑1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    ⋯.extClass.hom

Tactic:
exact (hS.mapShiftedHom_singleδ' F).trans (hS.map_of_exact F).extClass_hom.symm

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Transport

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A'
eA : A' ≌ A
eC : C' ≌ C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x✝ : A'
⊢ Epi
    ((((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').rightUnitor.inv ≫
          ((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').whiskerLeft eA.unitIso.hom ≫
            ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator ι' (eA.functor ⋙ eA.inverse)).hom ≫
              (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (ι'.associator eA.functor eA.inverse).inv ≫
                (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (whiskerRight e.hom eA.inverse) ≫
                  ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator (eC.functor ⋙ ι) eA.inverse).inv ≫
                    whiskerRight ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator eC.functor ι).inv eA.inverse ≫
                      whiskerRight (whiskerRight (eA.functor.associator (Λ.F ⋙ eC.inverse) eC.functor).hom ι)
                          eA.inverse ≫
                        whiskerRight
                            (whiskerRight
                              (eA.functor.whiskerLeft
                                ((Λ.F.associator eC.inverse eC.functor).hom ≫
                                  Λ.F.whiskerLeft eC.counitIso.hom ≫ Λ.F.rightUnitor.hom))
                              ι)
                            eA.inverse ≫
                          whiskerRight
                              ((eA.functor.associator Λ.F ι).hom ≫
                                eA.functor.whiskerLeft Λ.π ≫ eA.functor.rightUnitor.hom)
                              eA.inverse ≫
                            eA.unitIso.inv).app
      x✝)

Tactic:
by dsimp; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Transport

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A
G : C ⥤ C'
e : G ⋙ ι' ≅ ι
x✝ : A
⊢ Epi (((Λ.F.associator G ι').hom ≫ Λ.F.whiskerLeft e.hom ≫ Λ.π).app x✝)

Tactic:
by dsimp; infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
X' : C
g : X ⟶ X'
⊢ toSingleMk (f ≫ g) h = (toSingleMk f h).comp (ofHom ((singleFunctor C q).map g)) ⋯

Tactic:
apply (toSingleEquiv h).injective
  simp [toSingleEquiv, singleFunctor, singleFunctors, HomologicalComplex.single_map_f_self]

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((π' Λ).app X)).right) ⋯ ≫
      Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((toKaroubi A).map (Λ.π.app X))).right) ⋯ =
    𝟙 (Arrow.mk ((π' Λ).app X))

Tactic:
by
    ext
    · simp [← Functor.map_comp]
    · simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Epi
    { X₁ := syzygies (Projective.π Z), X₂ := over Z, X₃ := Z, f := d (Projective.π Z), g := Projective.π Z,
        zero := ⋯ }.g

Tactic:
by dsimp; infer_instance

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

Goal state before:
pp: case inst
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
k : ℕ
hk : J ^ k ≤ J'.obj
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')

Tactic:
exact ⟨CostructuredArrow.mk (⟨⟨⟨hk⟩⟩⟩ : (idealPowersToSelfLERadical J).obj (op k) ⟶ J')⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ leftDerived (𝟙 F) n = 𝟙 (F.leftDerived n)

Tactic:
dsimp only [leftDerived]
  simp only [leftDerivedToHomotopyCategory_id, Functor.whiskerRight_id']
  rfl

Goal state after: