mathlib-initiative/mathlib-tactics huggingface dataset:
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
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
X : C₁
⊢ IsIso (α₁.app X) ↔ IsIso (α₂.app (Φ.functor.obj X))

Tactic:
by

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.HasPointwiseLeftKanExtension F
inst✝ : w.GuitartExact
⊢ IsIso w.lanBaseChange

Tactic:
by

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

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
h : Φ.Derives F
inst✝ : Φ.IsRightDerivabilityStructure
⊢ F.HasPointwiseRightDerivedFunctor W₂

Tactic:
by

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

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
D₂ : Type u₄
inst✝³ : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝² : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst✝ : RF.IsRightDerivedFunctor α W₂
⊢ IsIso (α.app (Φ.functor.obj X₁))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app (CostructuredArrow.mk φ) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ IsIso (F.map w)

Tactic:
by

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

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
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
this✝¹ : F.HasPointwiseRightDerivedFunctor W₂
this✝ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
⊢ IsIso φ

Tactic:
by

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

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
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
this✝² : F.HasPointwiseRightDerivedFunctor W₂
this✝¹ :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso ((F.totalRightDerivedUnit L₂ W₂).app (Φ.functor.obj X₁))
this✝ : (Φ.functor ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
this : IsIso φ
⊢ F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft (asIso φ).hom = α

Tactic:
by

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

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
D₂ : Type u₄
inst✝² : Category.{v₄, u₄} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
h : Φ.Derives F
inst✝¹ : Φ.IsRightDerivabilityStructure
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
RF : D₂ ⥤ H
α : F ⟶ L₂ ⋙ RF
hα : ∀ (X₁ : C₁), IsIso (α.app (Φ.functor.obj X₁))
⊢ RF.IsRightDerivedFunctor α W₂

Tactic:
by

Goal state after:
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
Y₂ : D₂
⊢ Nonempty (B.LeftResolution Y₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
Y : C
p : (isInjective C).LimitOfShape (Discrete J) Y
this : ∀ (j : J), Injective (p.diag.obj { as := j })
X✝ Y✝ : C
q : X✝ ⟶ Y
i : X✝ ⟶ Y✝
x✝¹ : Mono i
x✝ : Discrete J
j : J
⊢ (i ≫
        p.isLimit.lift
          { pt := Y✝,
            π :=
              Discrete.natTrans fun x ↦
                match x with
                | { as := j } => Injective.factorThru (q ≫ p.π.app { as := j }) i }) ≫
      { pt := Y, π := p.π }.π.app { as := j } =
    q ≫ { pt := Y, π := p.π }.π.app { as := j }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (isInjective C).limitsOfShape (Discrete J) ≤ isInjective C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ IsZero 0

Tactic:
by

Goal state after:
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).GuitartExact

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
⊢ ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app j ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    s.ι.app j

Tactic:
by

Goal state after:
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
⊢ B.IsLeftDerivabilityStructure

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
m : ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).pt ⟶ s.pt
hm : ∀ (j : CostructuredArrow L (L.obj Y)), ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)).ι.app j ≫ m = s.ι.app j
⊢ m = e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
H : Type u₃
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₃, u₃} H
F : C ⥤ H
W : MorphismProperty C
hF : W.IsInvertedBy F
⊢ F.HasPointwiseRightDerivedFunctor W

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
F : C ⥤ H
RF : D ⥤ H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst✝ : RF.IsRightDerivedFunctor α W
⊢ α =
    (Localization.fac F hF L).inv ≫
      L.whiskerLeft ((Localization.lift F hF L).rightDerivedUnique RF (Localization.fac F hF L).inv α W).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
F : C ⥤ H
RF : D ⥤ H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst✝ : RF.IsRightDerivedFunctor α W
⊢ IsIso α

Tactic:
by

Goal state after:
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
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
⊢ W₂
    (R.functor.preimage
      (iso.hom.app (L.functor.objPreimage ρ.X₁) ≫ B.functor.map (L.functor.objObjPreimageIso ρ.X₁).hom ≫ ρ.w))

Tactic:
by

Goal state after:
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
X₂ : C₂
⊢ Nonempty (T.LeftResolution X₂)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : 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} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
inst✝ : w.GuitartExact
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : 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} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
T' : C₁ ⥤ D₁
B' : C₂ ⥤ D₂
α : T ≅ T'
β : B ≅ B'
⊢ (w.whiskerHorizontal α.inv β.hom).GuitartExact ↔ w.GuitartExact

Tactic:
by

Goal state after:
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:
by

Goal state after:
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').GuitartExact

Tactic:
by

Goal state after:
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₂
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst✝¹ : w.GuitartExact
inst✝ : w'.GuitartExact
⊢ (w.hComp' w' eT eB).GuitartExact

Tactic:
by

Goal state after:
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:
by

Goal state after:
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✝² : B₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ₕ w').GuitartExact
⊢ w'.GuitartExact

Tactic:
by

Goal state after:
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₂
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst✝¹ : B₁.EssSurj
inst✝ : w.GuitartExact
h : (w.hComp' w' eT eB).GuitartExact
⊢ w'.GuitartExact

Tactic:
by

Goal state after:
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
⊢ T.IsLeftDerivabilityStructure ↔ B.IsLeftDerivabilityStructure

Tactic:
by

Goal state after:
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:
by

Goal state after:
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.IsRightDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.hom
⊢ B.IsRightDerivabilityStructure

Tactic:
by

Goal state after:
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.hom
⊢ T.IsRightDerivabilityStructure ↔ B.IsRightDerivabilityStructure

Tactic:
by

Goal state after:
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✝⁵ : W₂'.RespectsIso
inst✝⁴ : L.IsInduced
inst✝³ : L.functor.IsEquivalence
inst✝² : R.IsInduced
inst✝¹ : R.functor.IsEquivalence
inst✝ : T.IsLeftDerivabilityStructure
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
⊢ B.IsLeftDerivabilityStructure

Tactic:
by

Goal state after: