mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯) ≫
      (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)).hom =
    (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)).hom

Tactic:
ext

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ StructuredArrow.Hom.right
      ((w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯) ≫
        (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)).hom) =
    StructuredArrow.Hom.right (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)).hom
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)).hom ≫
      (w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) =
    (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)).hom

Tactic:
ext

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ ((StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)).hom ≫
        (w.costructuredArrowRightwards X₃).map (CostructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯)).left =
    (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)).hom.left
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ (w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯) =
    CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
        (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯)

Tactic:
ext

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ StructuredArrow.Hom.right
      ((w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) ≫
        CostructuredArrow.hom
          (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
            (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯)) =
    StructuredArrow.Hom.right
      (CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯))
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ X₂' : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
g' : R.obj X₂' ⟶ B.obj X₃
γ : X₂' ⟶ X₂
hγ : R.map γ ≫ g = g'
A A' : w.CostructuredArrowDownwards g
φ : A ⟶ A'
⊢ (w.structuredArrowDownwards X₂').map (StructuredArrow.homMk (StructuredArrow.Hom.right φ.left) ⋯) ≫
      CostructuredArrow.hom
        (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A').right (γ ≫ (CostructuredArrow.left A').hom)
          (StructuredArrow.Hom.right (CostructuredArrow.hom A')) ⋯) =
    CostructuredArrow.hom
      (CostructuredArrowDownwards.mk w g' (CostructuredArrow.left A).right (γ ≫ (CostructuredArrow.left A).hom)
        (StructuredArrow.Hom.right (CostructuredArrow.hom A)) ⋯)

Tactic:
ext
    dsimp
    rw [← CostructuredArrow.w φ, structuredArrowDownwards_map]
    rfl

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
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.IsLeftDerivabilityStructure ↔ Φ.op.IsRightDerivabilityStructure

Tactic:
constructor

Goal state after:
case mp
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 := ⋯
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := ⋯
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := ⋯
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.IsLeftDerivabilityStructure → Φ.op.IsRightDerivabilityStructure

case mpr
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 := ⋯
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := ⋯
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := ⋯
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.op.IsRightDerivabilityStructure → Φ.IsLeftDerivabilityStructure
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α

case mpr
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W
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
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop := ⋯
⊢ ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))

Tactic:
intro Y₁ Y₂ w hw φ hφ
    convert! hP₂ w hw (homEquiv W W.Q L φ) hφ
    simp [homEquiv_comp, homEquiv_isoOfHom_inv]

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
⊢ F.HasPointwiseRightDerivedFunctor W₂ ↔ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
constructor

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
⊢ F.HasPointwiseRightDerivedFunctor W₂ → (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁

case mpr
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁ → F.HasPointwiseRightDerivedFunctor W₂
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsLeftDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
this✝ : B.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
iso' : CatCommSq T.functor L.functor R.functor B.functor := { iso := iso }
this : CatCommSq T.functor (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F :=
  CatCommSq.vComp L.functor W₁'.Q T.functor B.functor F R.functor W₂'.Q
⊢ TwoSquare.hComp iso.inv e'.inv = (CatCommSq.iso T.functor (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F).inv

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D₁
inst✝⁶ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsLocalizedEquivalence
inst✝³ : R.IsLocalizedEquivalence
inst✝² : R.functor.EssSurj
inst✝¹ : T.IsLeftDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
this✝ : B.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
iso' : CatCommSq T.functor L.functor R.functor B.functor := { iso := iso }
this : CatCommSq T.functor (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F :=
  CatCommSq.vComp L.functor W₁'.Q T.functor B.functor F R.functor W₂'.Q
X✝ : C₁
⊢ (TwoSquare.hComp iso.inv e'.inv).natTrans.app X✝ =
    (TwoSquare.natTrans (CatCommSq.iso T.functor (L.functor ⋙ W₁'.Q) (R.functor ⋙ W₂'.Q) F).inv).app X✝
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} D₁
inst✝³ : Category.{v_5, u_5} D₂
inst✝² : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ (w ≫ₕ w').op = w.op ≫ᵥ w'.op

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} D₁
inst✝³ : Category.{v_5, u_5} D₂
inst✝² : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
X✝ : C₁ᵒᵖ
⊢ (w ≫ₕ w').op.natTrans.app X✝ = (w.op ≫ᵥ w'.op).natTrans.app X✝
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
  (T.functor.associator R.functor W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor.associator B.functor W₂'.Q ≪≫ L.functor.isoWhiskerLeft e' ≪≫ (L.functor.associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
⊢ TwoSquare.hComp iso.inv e'.inv = e.inv

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₁' : MorphismProperty D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
x✝ : B.IsLeftDerivabilityStructure
this : T.HasLeftResolutions
F : W₁'.Localization ⥤ W₂'.Localization := B.localizedFunctor W₁'.Q W₂'.Q
e' : B.functor ⋙ W₂'.Q ≅ W₁'.Q ⋙ F := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
  (T.functor.associator R.functor W₂'.Q).symm ≪≫
    Functor.isoWhiskerRight iso W₂'.Q ≪≫
      L.functor.associator B.functor W₂'.Q ≪≫ L.functor.isoWhiskerLeft e' ≪≫ (L.functor.associator W₁'.Q F).symm
he' : TwoSquare.GuitartExact e'.inv
X✝ : C₁
⊢ (TwoSquare.hComp iso.inv e'.inv).natTrans.app X✝ = (TwoSquare.natTrans e.inv).app X✝
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
⊢ (w ≫ₕ w'.hom).op = w.op ≫ᵥ w''.hom

Tactic:
ext

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
V₃ : C₃ ⥤ D₃
eT : C₂ ≌ C₃
eB : D₂ ≌ D₃
w' : eT.functor ⋙ V₃ ≅ V₂ ⋙ eB.functor
w'' : V₂.op ⋙ eB.op.functor ≅ eT.op.functor ⋙ V₃.op := NatIso.op w'
X✝ : C₁ᵒᵖ
⊢ (w ≫ₕ w'.hom).op.natTrans.app X✝ = (w.op ≫ᵥ w''.hom).natTrans.app X✝
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
⊢ (isomorphisms (Plus (InjectiveObject C))).inverseImage (L C).functor =
    (CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus

Tactic:
ext

Goal state after:
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
X✝ Y✝ : CochainComplex.Plus (InjectiveObject C)
f✝ : X✝ ⟶ Y✝
⊢ (isomorphisms (Plus (InjectiveObject C))).inverseImage (L C).functor f✝ ↔
    (CochainComplex.Plus.quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus f✝
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
⊢ (quasiIso C).inverseImage (R C).functor = CochainComplex.Plus.quasiIso C

Tactic:
ext

Goal state after:
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
X✝ Y✝ : CochainComplex.Plus C
f✝ : X✝ ⟶ Y✝
⊢ (quasiIso C).inverseImage (R C).functor f✝ ↔ CochainComplex.Plus.quasiIso C f✝
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
⊢ (L C).IsLocalizedEquivalence

Tactic:
have :
      ((L C).functor ⋙ 𝟭 (Plus (InjectiveObject C))).IsLocalization
        ((CochainComplex.Plus.quasiIso C).inverseImage
          (InjectiveObject.ι C).mapCochainComplexPlus) :=
    inferInstanceAs ((HomotopyCategory.Plus.quotient (InjectiveObject C)).IsLocalization _)
  exact LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization (L C) (𝟭 _)

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
F : Plus C ⥤ H
inst✝² : HasDerivedCategory C
F' : DerivedCategory.Plus C ⥤ H
α : F ⟶ DerivedCategory.Plus.Qh ⋙ F'
inst✝¹ : F'.IsRightDerivedFunctor α (quasiIso C)
this : ∀ (Y : Plus (InjectiveObject C)), IsIso (α.app ((InjectiveObject.ι C).mapHomotopyCategoryPlus.obj Y))
K : HomologicalComplex C (ComplexShape.up ℤ)
hX : plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
inst✝ :
  ∀ (n : ℤ), Injective ({ obj := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K, property := hX }.obj.as.X n)
⊢ IsFibrant { obj := K, property := ⋯ }

Tactic:
rwa [CochainComplex.Plus.modelCategoryQuillen.isFibrant_iff]

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
⊢ mapExactFunctor F hS.extClass = ⋯.extClass

Tactic:
ext

Goal state after:
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
⊢ (mapExactFunctor F hS.extClass).hom = ⋯.extClass.hom
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

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
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsZero (K.stupidTrunc e) ↔ K.IsStrictlySupportedOutside e

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsZero (K.stupidTrunc e) → K.IsStrictlySupportedOutside e

case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ K.IsStrictlySupportedOutside e → IsZero (K.stupidTrunc e)
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

Goal state before:
pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupported e ∧ (K.stupidTrunc e).IsStrictlySupportedOutside e

Tactic:
constructor

Goal state after:
case mpr.left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupported e

case mpr.right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
h : K.IsStrictlySupportedOutside e
⊢ (K.stupidTrunc e).IsStrictlySupportedOutside e