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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (((shiftFunctor₂ C y).obj K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₂ C y).obj K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          (K.totalShift₂Iso y).hom.f (n + x) =
    (x * y).negOnePow •
      (((shiftFunctor₁₂CommIso C x y).hom.app K).f n₁).f n₂ ≫
        ((shiftFunctor₂ C y).obj ((shiftFunctor₁ C x).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫
          (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom.f n ≫
            (K.totalShift₁Iso x).hom.f (n + y) ≫
              ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n

Tactic:
ι_totalShift₂Iso_hom_f_assoc _ y n₁ n₂ n h _ rfl _ rfl,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (((shiftFunctor₂ C y).obj K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₂ C y).obj K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          (K.totalShift₂Iso y).hom.f (n + x) =
    (x * y).negOnePow •
      (((shiftFunctor₁₂CommIso C x y).hom.app K).f n₁).f n₂ ≫
        ((n₁ * y).negOnePow •
            (((shiftFunctor₁ C x).obj K).shiftFunctor₂XXIso n₁ n₂ y (n₂ + y) ⋯).hom ≫
              ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
                (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₁ C x).obj K).total (up ℤ)) y n (n + y) ⋯).inv) ≫
          (K.totalShift₁Iso x).hom.f (n + y) ≫
            ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : HasZeroMorphisms C₂
inst✝³ : Preadditive D
K₁ L₁ : CochainComplex C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
x : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Iso.refl
              ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                        ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
                    K₂).X
                i)).hom ≫
          ((HomologicalComplex₂.shiftFunctor₁ D x).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).d
            i j =
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                    ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
                K₂).d
            i j ≫
          (Iso.refl
              ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                        ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
                    K₂).X
                j)).hom

Tactic:
by
    intros
    ext
    dsimp
    simp only [Linear.comp_units_smul, id_comp, Functor.map_units_smul,
      NatTrans.app_units_zsmul, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
⊢ (CochainComplex.plus C).limitsOfShape J ≤ CochainComplex.plus C

Tactic:
rintro K ⟨p⟩
    obtain ⟨n, hn⟩ : ∃ (n : ℤ), ∀ (j : J), (p.diag.obj j).IsStrictlyGE n := by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩
    refine ⟨n, ?_⟩
    rw [isStrictlyGE_iff]
    intro i hi
    rw [IsZero.iff_id_eq_zero]
    exact (isLimitOfPreserves (HomologicalComplex.eval _ _ i) p.isLimit).hom_ext
      (fun j ↦ (isZero_of_isStrictlyGE (p.diag.obj j) n i).eq_of_tgt _ _)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ Mono ⋯.shortComplex'.f

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ ∀ (P : C) (g_1 : P ⟶ ⋯.shortComplex'.X₁), g_1 ≫ ⋯.shortComplex'.f = 0 → g_1 = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge 1 ((shiftFunctor C n).obj X)
⊢ (t.ge 0).shift n X

Tactic:
exact t.ge_one_le _ hX

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

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ (h.extend e).ofExtend = h

Tactic:
by
  ext i j
  simp [ofExtend_hom, h.extend_hom_eq e rfl rfl]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
⊢ t.plus ≤ t.plus.shift n

Tactic:
by
        rintro X ⟨i, _⟩
        exact ⟨i - n, t.isGE_shift _ i _ _ (by omega)⟩

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝³ : HasPushout f g
inst✝² : (trivialCofibrations C).IsStableUnderCobaseChange
inst✝¹ : Cofibration g
inst✝ : WeakEquivalence g
⊢ WeakEquivalence (pushout.inl f g)

Tactic:
by
  rw [weakEquivalence_iff]
  exact (MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g)
    (mem_trivialCofibrations g)).2

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁶ : HasBinaryProduct A A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : HasTerminal C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (fibrations C).IsStableUnderBaseChange
inst✝¹ : IsFibrant A
inst✝ : P.IsGood
⊢ Fibration P.p₀

Tactic:
by
  rw [← P.p_fst]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
h : LeftHomotopyRel f g
Z : C
p : Y ⟶ Z
⊢ LeftHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
obtain ⟨P, ⟨h⟩⟩ := h
  exact (h.postcomp p).leftHomotopyRel

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f₀ f₁ f₂ : X ⟶ Y
inst✝ : IsFibrant Y
h' : RightHomotopyRel f₁ f₂
P : PathObject Y
h : P.RightHomotopy f₀ f₁
⊢ RightHomotopyRel f₀ f₂

Tactic:
obtain ⟨P', _, ⟨h'⟩⟩ := h'.exists_good_pathObject

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f₀ f₁ f₂ : X ⟶ Y
inst✝ : IsFibrant Y
h'✝ : RightHomotopyRel f₁ f₂
P : PathObject Y
h : P.RightHomotopy f₀ f₁
P' : PathObject Y
left✝ : P'.IsGood
h' : P'.RightHomotopy f₁ f₂
⊢ RightHomotopyRel f₀ f₂
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝ : A.IsVerdierLeftLocalizing B
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hX : B.op X✝
hY : A.op Y✝
⊢ ∃ Z a b, A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ :=
      IsVerdierLeftLocalizing.fac f.unop hY hX
    exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : ℤ
h : a + 1 = b
⊢ (t.truncLEIsoTruncLT a b h).inv ≫ t.truncLEι a = t.truncLTι b

Tactic:
by
  subst h
  dsimp [truncLEIsoTruncLT, truncLEι, truncLE]
  rw [Category.id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a : ℤ
x✝ : C
⊢ ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x✝ ≫ (t.truncGEδLE a (a + 1) ⋯).app x✝) ≫
      (shiftFunctor C 1).map (𝟙 ((t.truncLE a).obj x✝)) =
    (t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x✝ ≫ (t.truncGEδLE a (a + 1) ⋯).app x✝

Tactic:
simp only [Functor.map_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z

Tactic:
refine ⟨⟨Z, hZ.1⟩, A.homMk a, A.homMk (b ≫ (A.ι.commShiftIso 1).inv.app _), ?_, hZ.2⟩

Goal state after:
case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)) ∈ Pretriangulated.distinguishedTriangles
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ (ι.obj ((singleFunctor C n).obj X)).IsGE n

Tactic:
change DerivedCategory.TStructure.t.IsGE ((DerivedCategory.singleFunctor C n).obj X) n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
⊢ t.IsGE ((DerivedCategory.singleFunctor C n).obj X) n
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} D₁
inst✝¹⁰ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : IsTriangulated C
inst✝³ : A.IsTriangulated
inst✝² : B.IsTriangulated
inst✝¹ : B.IsClosedUnderIsomorphisms
inst✝ : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
⊢ (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse ≤
    (B.op.inverseImage A.op.ι).trW.isoClosure.inverseImage A.opEquivalence.symm.functor

Tactic:
intro _ _ f hf

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} D₁
inst✝¹⁰ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : IsTriangulated C
inst✝³ : A.IsTriangulated
inst✝² : B.IsTriangulated
inst✝¹ : B.IsClosedUnderIsomorphisms
inst✝ : A.IsVerdierLeftLocalizing B
L₁ : A.FullSubcategory ⥤ (B.inverseImage A.ι).trW.Localization := (B.inverseImage A.ι).trW.Q
L₂ : C ⥤ B.trW.Localization := B.trW.Q
F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
  (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
  {
    iso :=
      A.opEquivalence.functor.isoWhiskerLeft
        (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm) }
this : L₂.op.IsLocalization B.op.trW
X✝ Y✝ : A.FullSubcategoryᵒᵖ
f : X✝ ⟶ Y✝
hf : (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse f
⊢ (B.op.inverseImage A.op.ι).trW.isoClosure.inverseImage A.opEquivalence.symm.functor f
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case refine_1
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₁
hf : IsIso ((t.truncGE n₁).map g)
⊢ ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀

Tactic:
refine ⟨_, (t.truncLTι n₁).app Y, inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y,
      isomorphic_distinguished _ (t.triangleLTGE_distinguished n₁ Y) _ ?_,
      by subst hn; infer_instance⟩
    exact Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
      (asIso ((t.truncGE n₁).map g)) (by simp) (by simp) (by simp))

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
⊢ (homRel C).FactorsThroughLocalization (weakEquivalences (FibrantObject C))

Tactic:
rintro X Y f g h
  obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_cylinder
  let L := (weakEquivalences (FibrantObject C)).Q
  rw [areEqualizedByLocalization_iff L]
  suffices L.map (homMk P.i₀) = L.map (homMk P.i₁) by
    simp only [show f = homMk P.i₀ ≫ homMk h.h by cat_disch,
      show g = homMk P.i₁ ≫ homMk h.h by cat_disch, Functor.map_comp, this]
  have := Localization.inverts L (weakEquivalences _) (homMk P.π) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)
  simp [← cancel_mono (L.map (homMk P.π)), ← L.map_comp]

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✝¹ x✝ : FibrantObject C
f : x✝¹ ⟶ x✝
⊢ (f ≫ { hom := iResolutionObj (ι.obj x✝) }).hom =
    ({ hom := iResolutionObj (ι.obj x✝¹) } ≫ homMk (resolutionMap (ι.map f))).hom

Tactic:
exact (HoCat.resolutionMap_fac f.hom).symm

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))

Tactic:
apply hα

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))

Tactic:
apply hα

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
⊢ IsIso α ↔ ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))

Tactic:
constructor
  · intros
    infer_instance
  · intro hα
    have : ∀ (X₂ : D₂), IsIso (α.app X₂) := fun X₂ => by
      have := Φ.essSurj_of_hasLeftResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα
    exact NatIso.isIso_of_isIso_app α

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
⊢ Φ.IsLeftDerivabilityStructure ↔ Φ.op.IsRightDerivabilityStructure

Tactic:
have eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv :=
    TwoSquare.guitartExact_op_iff _

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := NatIso.op e.symm
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.IsLeftDerivabilityStructure ↔ Φ.op.IsRightDerivabilityStructure
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 ⋯
⊢ Zigzag A₀ A₁

Tactic:
calc
    Zigzag A₀ (Z s₀) := .of_inv f₀
    Zigzag (Z s₀) Z' := .of_hom <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₀) (by simp [Z, Z', dsimp% h.h₀])
    Zigzag Z' (Z s₁) := .of_inv <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₁) (by simp [Z, Z', dsimp% h.h₁])
    Zigzag (Z s₁) A₁ := .of_hom f₁

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₃, u₃} C₃
inst✝⁵ : Category.{v₄, u₄} C₄
inst✝⁴ : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝³ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝² : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F : C₂ ⥤ D
inst✝¹ : R.HasPointwiseLeftKanExtension F
inst✝ : w.GuitartExact
⊢ IsIso (w.lanBaseChange.app F)

Tactic:
by
  rw [isIso_lanBaseChange_app_iff]
  let hF := isPointwiseLeftKanExtensionOfIsLeftKanExtension (F := F) _ (R.lanUnit.app F)
  exact (hF.compTwoSquare w).isLeftKanExtension

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

Goal state before:
pp: case refine_1
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (CochainComplex.Plus.quasiIso C).IsInvertedBy (quotient C ⋙ L)

Tactic:
intro _ _ f hf

Goal state after:
case refine_1
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
X✝ Y✝ : CochainComplex.Plus C
f : X✝ ⟶ Y✝
hf : CochainComplex.Plus.quasiIso C f
⊢ IsIso ((quotient C ⋙ L).map f)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_3
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ quasiIso C ≤ (CochainComplex.Plus.quasiIso C).map (quotient C)

Tactic:
· rintro K L f hf
    obtain ⟨K, rfl⟩ := Plus.quotient_obj_surjective K
    obtain ⟨L, rfl⟩ := Plus.quotient_obj_surjective L
    obtain ⟨f, rfl⟩ := (Plus.quotient C).map_surjective f
    apply MorphismProperty.map_mem_map
    simpa [quasiIso, quotient_map_mem_quasiIso_iff] using! hf

Goal state after: