awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ StructuredArrow.Hom.right
      (((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                  (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
              X₂).map
          (StructuredArrow.homMk ρ.X₁ (W₁ := W₁.arrow) (W₂ := W₂.arrow).hom ⋯) ≫
        CostructuredArrow.hom
          ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
            (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))) =
    StructuredArrow.Hom.right
      (CostructuredArrow.hom
        ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
          (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯)))

Tactic:
simp [← cancel_epi (isoOfHom L W₂ ρ.w.left ρ.hw.1).hom, ← L.map_comp_assoc, fac]

Premises used: CategoryTheory.LocalizerMorphism.RightResolution.w, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.map_comp_assoc, And.left, CategoryTheory.LocalizerMorphism.RightResolution.hw, CategoryTheory.Arrow.Hom.left, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
rw :
  ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ Functor.obj (𝟭 W₂.Localization) X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).rightUnitor.symm.hom g)
⊢ Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
rw [Φ.isRightDerivabilityStructure_iff (Φ.functor ⋙ W₂.Q) W₂.Q (𝟭 _)
    (Functor.rightUnitor _).symm, TwoSquare.guitartExact_iff_isConnected_downwards]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.LocalizerMorphism.functor, CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff, CategoryTheory.Iso.symm, CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
⊢ ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ Functor.obj (𝟭 W₂.Localization) X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).rightUnitor.symm.hom g)

Tactic:
apply Constructor.isConnected

Premises used: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.isConnected
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
rw : Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
⊢ Φ.IsLeftDerivabilityStructure (W₁ := W₁) (W₂ := W₂)

Tactic:
rw [isLeftDerivabilityStructure_iff_op]

Premises used: CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_op
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
f : Arrow.{v_2, u_2} C₂ᵒᵖ
R : Φ.arrow (W₁ := W₁) (W₂ := W₂).LeftResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk f.hom.unop) :=
  Classical.arbitrary
    (Φ.arrow (W₁ := W₁) (W₂ := W₂).LeftResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk f.hom.unop))
⊢ Nonempty
    (Φ.op (W₁ := W₁) (W₂ := W₂).arrow (W₁ := W₁.op) (W₂ := W₂.op).RightResolution (W₁ := W₁.op.arrow) (W₂ :=
      W₂.op.arrow) f)

Tactic:
⟨{
      X₁ := Arrow.mk R.X₁.hom.op
      w := Arrow.homMk R.w.right.op R.w.left.op (Quiver.Hom.unop_inj R.w.w.symm)
      hw := ⟨R.hw.right, R.hw.left⟩ }⟩

Premises used: CategoryTheory.Arrow.Hom.right, Quiver.Hom.op, CategoryTheory.LocalizerMorphism.LeftResolution.w, CategoryTheory.LocalizerMorphism.RightResolution.mk, CategoryTheory.Arrow.Hom.w, Nonempty.intro, Quiver.Hom.unop_inj, And.right, And.left, CategoryTheory.LocalizerMorphism.LeftResolution.hw, And.intro, CategoryTheory.Arrow.Hom.left, Eq.symm, CategoryTheory.Arrow.homMk
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
f : Arrow.{v_2, u_2} C₂ᵒᵖ
R : Φ.arrow (W₁ := W₁) (W₂ := W₂).LeftResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk f.hom.unop) :=
  Classical.arbitrary
    (Φ.arrow (W₁ := W₁) (W₂ := W₂).LeftResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk f.hom.unop))
⊢ Nonempty
    (Φ.op (W₁ := W₁) (W₂ := W₂).arrow (W₁ := W₁.op) (W₂ := W₂.op).RightResolution (W₁ := W₁.op.arrow) (W₂ :=
      W₂.op.arrow) f)

Tactic:
exact ⟨{
      X₁ := Arrow.mk R.X₁.hom.op
      w := Arrow.homMk R.w.right.op R.w.left.op (Quiver.Hom.unop_inj R.w.w.symm)
      hw := ⟨R.hw.right, R.hw.left⟩ }⟩
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).arrow (W₁ := W₁.op) (W₂ := W₂.op).HasRightResolutions (W₁ := W₁.op.arrow) (W₂ :=
    W₂.op.arrow)

Tactic:
have : Φ.op.arrow.HasRightResolutions := fun f ↦ by
    let R : Φ.arrow.LeftResolution (Arrow.mk f.hom.unop) := Classical.arbitrary _
    exact ⟨{
      X₁ := Arrow.mk R.X₁.hom.op
      w := Arrow.homMk R.w.right.op R.w.left.op (Quiver.Hom.unop_inj R.w.w.symm)
      hw := ⟨R.hw.right, R.hw.left⟩ }⟩
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
this :
  Φ.op (W₁ := W₁) (W₂ := W₂).arrow (W₁ := W₁.op) (W₂ := W₂.op).HasRightResolutions (W₁ := W₁.op.arrow) (W₂ :=
    W₂.op.arrow)
⊢ ∀ (X₂ : C₂ᵒᵖ), IsConnected (Φ.op (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.op) (W₂ := W₂.op) X₂)

Tactic:
have (X₂ : C₂ᵒᵖ) : IsConnected (Φ.op.RightResolution X₂) :=
    isConnected_of_equivalent (LeftResolution.opEquivalence Φ X₂.unop)
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
this_1 :
  Φ.op (W₁ := W₁) (W₂ := W₂).arrow (W₁ := W₁.op) (W₂ := W₂.op).HasRightResolutions (W₁ := W₁.op.arrow) (W₂ :=
    W₂.op.arrow)
this : ∀ (X₂ : C₂ᵒᵖ), IsConnected (Φ.op (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.op) (W₂ := W₂.op) X₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
IsRightDerivabilityStructure.mk' _

Premises used: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.LeftResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasLeftResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
inst_5 : Φ.IsLocalizedEquivalence (W₁ := W₁) (W₂ := W₂)
this_1 :
  Φ.op (W₁ := W₁) (W₂ := W₂).arrow (W₁ := W₁.op) (W₂ := W₂.op).HasRightResolutions (W₁ := W₁.op.arrow) (W₂ :=
    W₂.op.arrow)
this : ∀ (X₂ : C₂ᵒᵖ), IsConnected (Φ.op (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.op) (W₂ := W₂.op) X₂)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)

Tactic:
exact IsRightDerivabilityStructure.mk' _

Premises used: CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk'
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
rw : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
⊢ F.HasPointwiseRightDerivedFunctor W₂

Tactic:
rw [hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure Φ F]

Premises used: CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
Functor.hasPointwiseRightDerivedFunctor_of_inverts _ h

Premises used: CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_of_inverts
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_3 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
exact Functor.hasPointwiseRightDerivedFunctor_of_inverts _ h

Premises used: CategoryTheory.Functor.hasPointwiseRightDerivedFunctor_of_inverts
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst_6 : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (W := W₁) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F :=
  Localization.Lifting.iso W₁.Q W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) G
⊢ G.IsRightDerivedFunctor eG.inv W₁

Tactic:
have := Functor.isRightDerivedFunctor_of_inverts W₁ G eG
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst_6 : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (W := W₁) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F :=
  Localization.Lifting.iso W₁.Q W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) G
this : G.IsRightDerivedFunctor eG.inv W₁
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁

Tactic:
have := (Φ.functor ⋙ F).hasPointwiseRightDerivedFunctor_of_inverts h
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst_6 : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (W := W₁) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F :=
  Localization.Lifting.iso W₁.Q W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) G
this_1 : G.IsRightDerivedFunctor eG.inv W₁
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
rw : IsIso (eG.inv.app X₁)
⊢ IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))

Tactic:
rw [← Φ.isIso_iff_of_isRightDerivabilityStructure W₁.Q L₂ F G eG.inv RF α]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.LocalizerMorphism.isIso_iff_of_isRightDerivabilityStructure, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
X₁ : C₁
inst_6 : RF.IsRightDerivedFunctor α W₂
G : W₁.Localization ⥤ H := Localization.lift (W := W₁) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) h W₁.Q
eG : W₁.Q ⋙ G ≅ Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F :=
  Localization.Lifting.iso W₁.Q W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F) G
this_1 : G.IsRightDerivedFunctor eG.inv W₁
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
⊢ IsIso (eG.inv.app X₁)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
⊢ F.HasPointwiseRightDerivedFunctor W₂

Tactic:
have := h.hasPointwiseRightDerivedFunctor
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))

Tactic:
have := h.isIso (F.totalRightDerivedUnit L₂ W₂)
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
⊢ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj

Tactic:
have := Φ.essSurj_of_hasRightResolutions L₂
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
Goal:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} H
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
h : Φ.Derives (W₁ := W₁) (W₂ := W₂) F
inst_4 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
RF : Functor.{v₄, v₃, u₄, u₃} D₂ H
α : F ⟶ L₂ ⋙ RF
hα :
  ∀ (X₁ : C₁),
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this_1 : F.HasPointwiseRightDerivedFunctor W₂
this_2 :
  ∀ (X₁ : C₁) [(F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂],
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (Y :=
      (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
      (NatTrans.app (F.totalRightDerivedUnit L₂ W₂) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
this : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
φ : F.totalRightDerived L₂ W₂ ⟶ RF :=
  (F.totalRightDerived L₂ W₂).rightDerivedDesc (F.totalRightDerivedUnit L₂ W₂) W₂ RF α
⊢ F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α

Tactic:
have hφ : F.totalRightDerivedUnit L₂ W₂ ≫ Functor.whiskerLeft L₂ φ = α :=
    (F.totalRightDerived L₂ W₂).rightDerived_fac (F.totalRightDerivedUnit L₂ W₂) W₂ RF α