awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor (hypothesis)
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)
⊢ Φ.op (W₁ := W₁) (W₂ := W₂).IsRightDerivabilityStructure (W₁ := W₁.op) (W₂ := W₂.op)
have this₁ : ∀ (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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (goal)
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₂)
⊢ F.HasPointwiseRightDerivedFunctor W₂
have rw : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
Tactic: rw [hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure Φ F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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
⊢ IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
have this : G.IsRightDerivedFunctor eG.inv W₁
Tactic: have := Functor.isRightDerivedFunctor_of_inverts W₁ G eG
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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₁
⊢ IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
have this₁ : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
Tactic: have := (Φ.functor ⋙ F).hasPointwiseRightDerivedFunctor_of_inverts h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (goal)
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 (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)) (α.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
have rw : IsIso (eG.inv.app X₁)
Tactic: rw [← Φ.isIso_iff_of_isRightDerivabilityStructure W₁.Q L₂ F G eG.inv RF α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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₁))
⊢ RF.IsRightDerivedFunctor α W₂
have this : F.HasPointwiseRightDerivedFunctor W₂
Tactic: have := h.hasPointwiseRightDerivedFunctor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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₂
⊢ RF.IsRightDerivedFunctor α W₂
have 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₁))
Tactic: have := h.isIso (F.totalRightDerivedUnit L₂ W₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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₁))
⊢ RF.IsRightDerivedFunctor α W₂
have this₁ : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).EssSurj
Tactic: have := Φ.essSurj_of_hasRightResolutions L₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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 α
⊢ RF.IsRightDerivedFunctor α W₂
have hφ : 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 α
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (goal)
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 α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
⊢ IsIso φ
have rw : ∀ (X : D₂), IsIso (φ.app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (goal)
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 α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ IsIso (φ.app Y₂)
have rw : IsIso (X :=
  (F.totalRightDerived L₂ W₂).obj
    ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
  (φ.app ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
Tactic: rw [NatTrans.isIso_app_iff_of_iso φ ((Φ.functor ⋙ L₂).objObjPreimageIso Y₂).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (goal)
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 α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ IsIso (X :=
    (F.totalRightDerived L₂ W₂).obj
      ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
    (φ.app ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂)))
have dsimp : IsIso (X :=
  (F.totalRightDerived L₂ W₂).obj
    (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
  (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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 α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
Y₂ : D₂
⊢ IsIso (X :=
    (F.totalRightDerived L₂ W₂).obj
      (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
    (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj ((Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂).objPreimage Y₂))))
have hα₁ : ∀ (X₁ : C₁),
  IsIso (X := (L₂ ⋙ F.totalRightDerived L₂ W₂).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁))
    (φ.app (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁)))
Tactic: simp only [← hφ, NatTrans.comp_app, Functor.whiskerLeft_app, isIso_comp_left_iff] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (hypothesis)
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 α
hφ : F.totalRightDerivedUnit L₂ W₂ ≫ L₂.whiskerLeft φ = α
⊢ RF.IsRightDerivedFunctor α W₂
have this₁ : IsIso φ
Tactic: have : IsIso φ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro Y₂
    rw [NatTrans.isIso_app_iff_of_iso φ ((Φ.functor ⋙ L₂).objObjPreimageIso Y₂).symm]
    dsimp
    simp only [← hφ, NatTrans.comp_app, Functor.whiskerLeft_app, isIso_comp_left_iff] at hα
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (goal)
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_3 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ 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 φ
⊢ RF.IsRightDerivedFunctor α W₂
have rw : (F.totalRightDerived L₂ W₂).IsRightDerivedFunctor (F.totalRightDerivedUnit L₂ W₂) W₂
Tactic: rw [← Functor.isRightDerivedFunctor_iff_of_iso (F.totalRightDerivedUnit L₂ W₂) α W₂
    (asIso φ) (by cat_disch)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (goal)
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₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
⊢ W₂ ≤ W₁.inverseImage ρ
have rw : W₂ ≤ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage ρ
Tactic: rw [hW₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (hypothesis)
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₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage ρ f
have this : Functor.map (𝟭 C₂) f ≫ i.app Y = i.app X ≫ (ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)).map f
Tactic: have := i.naturality f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (goal)
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₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f)
⊢ (W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))).inverseImage ρ f
have simp : W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f))
Tactic: simp only [MorphismProperty.inverseImage_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions (goal)
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₂
ρ : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor (W₁ := W₁) (W₂ := W₂)
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage (Φ.functor (W₁ := W₁) (W₂ := W₂))
inst_2 : W₂.HasTwoOutOfThreeProperty
X Y : C₂
f : X ⟶ Y
hf : W₂ f
this : f ≫ i.app Y = i.app X ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f)
⊢ W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map (ρ.map f))
have rw : W₂ (f ≫ i.app Y)
Tactic: rw [← W₂.precomp_iff _ _ (hi X), ← this]