awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (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₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ IsIso
    (F₁.rightDerivedDesc α₁ W₁ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂)
      (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
        (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
          whiskerRight
              (Iso.hom
                (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂
                  (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
              F₂ ≫
            (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom))
have rw : (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).IsLeftKanExtension
  (Φ.functor (W₁ := W₁) (W₂ := W₂).whiskerLeft α₂ ≫
    (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ F₂).inv ≫
      whiskerRight
          (Iso.hom
            (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
          F₂ ≫
        (L₁.associator (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂) F₂).hom)
Tactic: rw [← isRightDerivedFunctor_iff_isIso_rightDerivedDesc,
    isRightDerivedFunctor_iff_isLeftKanExtension]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (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₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
X : C₁
⊢ IsIso (α₁.app X) ↔
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
have rw : IsIso (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).obj (L₁.obj X))
    (α₁.app X ≫ NatTrans.app (Φ.rightDerivedFunctorComparison (W₁ := W₁) (W₂ := W₂) L₁ L₂ F F₁ α₁ F₂ α₂) (L₁.obj X)) ↔
  IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
Tactic: rw [← isIso_comp_right_iff (α₁.app X)
    ((Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂).app (L₁.obj X)),
    rightDerivedFunctorComparison_fac_app, isIso_comp_right_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (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₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
X : C₁
rw :
  IsIso (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).obj (L₁.obj X))
      (α₁.app X ≫ NatTrans.app (Φ.rightDerivedFunctorComparison (W₁ := W₁) (W₂ := W₂) L₁ L₂ F F₁ α₁ F₂ α₂) (L₁.obj X)) ↔
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
⊢ IsIso (α₁.app X) ↔
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
have rw₁ : IsIso (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).obj (L₁.obj X))
    (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      F₂.map
        (NatTrans.app
          (Iso.hom
            (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
          X)) ↔
  IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
Tactic: rw [← isIso_comp_right_iff (α₁.app X)
    ((Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂).app (L₁.obj X)),
    rightDerivedFunctorComparison_fac_app, isIso_comp_right_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (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₄
D₂ : Type u₅
inst_3 : Category.{v₄, u₄} D₁
inst_4 : Category.{v₅, u₅} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₄, u₁, u₄} C₁ D₁
L₂ : Functor.{v₂, v₅, u₂, u₅} C₂ D₂
inst_5 : L₁.IsLocalization W₁
inst_6 : L₂.IsLocalization W₂
F : Functor.{v₂, v₃, u₂, u₃} C₂ H
F₁ : Functor.{v₄, v₃, u₄, u₃} D₁ H
α₁ : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F ⟶ L₁ ⋙ F₁
F₂ : Functor.{v₅, v₃, u₅, u₃} D₂ H
α₂ : F ⟶ L₂ ⋙ F₂
inst_7 : F₁.IsRightDerivedFunctor α₁ W₁
inst_8 : Φ.IsRightDerivabilityStructure (W₁ := W₁) (W₂ := W₂)
inst_9 : (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst_10 : F₂.IsRightDerivedFunctor α₂ W₂
X : C₁
rw :
  IsIso (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).obj (L₁.obj X))
      (α₁.app X ≫ NatTrans.app (Φ.rightDerivedFunctorComparison (W₁ := W₁) (W₂ := W₂) L₁ L₂ F F₁ α₁ F₂ α₂) (L₁.obj X)) ↔
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
rw₁ :
  IsIso (Y := (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂ ⋙ F₂).obj (L₁.obj X))
      (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
        F₂.map
          (NatTrans.app
            (Iso.hom
              (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
            X)) ↔
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
⊢ IsIso (α₁.app X) ↔
    IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
have rw₂ : IsIso (X := (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ F).obj X) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) ↔
  IsIso (X := F.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X)) (α₂.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))
Tactic: rw [← isIso_comp_right_iff (α₁.app X)
    ((Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂).app (L₁.obj X)),
    rightDerivedFunctorComparison_fac_app, isIso_comp_right_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v_1, v_5, u_1, u_5} C₁ D₂
G' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_6 : Lifting L₁ W₁ G G'
F : Functor.{v_2, v_4, u_2, u_4} C₂ D₁
F' : Functor.{v_5, v_4, u_5, u_4} D₂ D₁
inst_7 : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ Eq (α :=
    ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).inverse ⋙ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).functor).obj (L₂.obj X) ≅
      Functor.obj.{v_5, v_5, u_5, u_5} (𝟭 D₂) (L₂.obj X))
    ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X))
    (Iso.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')) X ≪≫ β.app X)
have w : Eq (α :=
  ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).inverse ⋙ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).functor).obj (L₂.obj X) ⟶
    Functor.obj.{v_5, v_5, u_5, u_5} (𝟭 D₂) (L₂.obj X))
  (Iso.hom ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X)))
  (Iso.hom (Iso.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')) X ≪≫ β.app X))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v_1, v_5, u_1, u_5} C₁ D₂
G' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_6 : Lifting L₁ W₁ G G'
F : Functor.{v_2, v_4, u_2, u_4} C₂ D₁
F' : Functor.{v_5, v_4, u_5, u_4} D₂ D₁
inst_7 : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ Eq (α :=
    ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).inverse ⋙ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).functor).obj (L₂.obj X) ⟶
      Functor.obj.{v_5, v_5, u_5, u_5} (𝟭 D₂) (L₂.obj X))
    (Iso.hom ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X)))
    (Iso.hom (Iso.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')) X ≪≫ β.app X))
have w : NatTrans.app (liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom) (L₂.obj X) =
  G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
Tactic: dsimp [equivalence, Equivalence.mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v_1, v_5, u_1, u_5} C₁ D₂
G' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_6 : Lifting L₁ W₁ G G'
F : Functor.{v_2, v_4, u_2, u_4} C₂ D₁
F' : Functor.{v_5, v_4, u_5, u_4} D₂ D₁
inst_7 : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ NatTrans.app (liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom) (L₂.obj X) =
    G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
have w : NatTrans.app (Iso.hom (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G'))) X ≫
    β.hom.app X ≫ NatTrans.app (Iso.inv (Lifting.iso L₂ W₂ L₂ (𝟭 D₂))) X =
  G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
Tactic: rw [liftNatTrans_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v_1, v_5, u_1, u_5} C₁ D₂
G' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_6 : Lifting L₁ W₁ G G'
F : Functor.{v_2, v_4, u_2, u_4} C₂ D₁
F' : Functor.{v_5, v_4, u_5, u_4} D₂ D₁
inst_7 : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ NatTrans.app (Iso.hom (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G'))) X ≫
      β.hom.app X ≫ NatTrans.app (Iso.inv (Lifting.iso L₂ W₂ L₂ (𝟭 D₂))) X =
    G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
have w : G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X ≫ 𝟙 (L₂.obj X) =
  G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
Tactic: dsimp [Lifting.iso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G : Functor.{v_1, v_5, u_1, u_5} C₁ D₂
G' : Functor.{v_4, v_5, u_4, u_5} D₁ D₂
inst_6 : Lifting L₁ W₁ G G'
F : Functor.{v_2, v_4, u_2, u_4} C₂ D₁
F' : Functor.{v_5, v_4, u_5, u_4} D₂ D₁
inst_7 : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X ≫ 𝟙 (L₂.obj X) =
    G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
have w : G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X = G'.map ((Lifting.iso L₂ W₂ F F').hom.app X) ≫ β.hom.app X
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D
W₁ : MorphismProperty.{v_1, u_1} C₁
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ D
W₂ : MorphismProperty.{v_2, u_2} C₂
E : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst_3 : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
x x_1 : C₁
f : x ⟶ x_1
hf : W₁ f
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)
have obtain : ∀ (w w_1 : C₂) (f' : w ⟶ w_1) (hf' : W₂ f') (e : Arrow.mk f' ≅ Arrow.mk (E.functor.map f)),
  IsIso ((E.functor ⋙ W₂.Q).map f)
Tactic: obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D
W₁ : MorphismProperty.{v_1, u_1} C₁
L₂ : Functor.{v_2, v_3, u_2, u_3} C₂ D
W₂ : MorphismProperty.{v_2, u_2} C₂
E : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst_3 : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
⊢ L₂.IsLocalization W₂
have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
Tactic: have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf => by
    obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
    exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Equivalence (hypothesis)
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_4, u_4} D₁
inst_3 : Category.{v_5, u_5} D₂
L₁ : Functor.{v_1, v_4, u_1, u_4} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_5, u_2, u_5} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
E : Equivalence.{v_1, v_2, u_1, u_2} C₁ C₂
E' : Equivalence.{v_4, v_5, u_4, u_5} D₁ D₂
inst_5 : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
⊢ L₂.IsLocalization W₂
have this : (E.functor ⋙ L₂).IsLocalization W₁
Tactic: haveI : (E.functor ⋙ L₂).IsLocalization W₁ :=
    of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_3, u_3} C₂
inst_2 : Category.{v_5, u_5} D₁
inst_3 : Category.{v_6, u_6} D₂
W₁ : MorphismProperty.{v_2, u_2} C₁
W₂ : MorphismProperty.{v_3, u_3} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_3, v_6, u_3, u_6} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ (L₁.map f) = L₂.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map f)
have dsimp : NatTrans.app
      (Iso.hom (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
      X ≫
    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂).map (L₁.map f) ≫
      NatTrans.app
        (Iso.inv
          (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂)))
        Y =
  L₂.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map f)
Tactic: dsimp [homMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_3, u_3} C₂
inst_2 : Category.{v_5, u_5} D₁
inst_3 : Category.{v_6, u_6} D₂
W₁ : MorphismProperty.{v_2, u_2} C₁
W₂ : MorphismProperty.{v_3, u_3} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_3, v_6, u_3, u_6} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : Functor.{v_5, v_6, u_5, u_6} D₁ D₂ := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G'
⊢ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ f = e.hom.app X ≫ G.map f ≫ e.inv.app Y
have change : e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y
Tactic: change e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_3, u_3} C₂
inst_2 : Category.{v_5, u_5} D₁
inst_3 : Category.{v_6, u_6} D₂
W₁ : MorphismProperty.{v_2, u_2} C₁
W₂ : MorphismProperty.{v_3, u_3} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_3, v_6, u_3, u_6} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : Functor.{v_5, v_6, u_5, u_6} D₁ D₂ := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G'
this : Localization.Lifting L₁ W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) G := Localization.Lifting.mk (W := W₁) e.symm
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) G' G e'.symm
⊢ e = e' ≪≫ L₁.isoWhiskerLeft α
have w : ∀ (x : C₁), e.hom.app x = (e' ≪≫ L₁.isoWhiskerLeft α).hom.app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (hypothesis)
Goal:
C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_3, u_3} C₂
inst_2 : Category.{v_5, u_5} D₁
inst_3 : Category.{v_6, u_6} D₂
W₁ : MorphismProperty.{v_2, u_2} C₁
W₂ : MorphismProperty.{v_3, u_3} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_3, v_6, u_3, u_6} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : L₁.obj X ⟶ L₁.obj Y
G' : Functor.{v_5, v_6, u_5, u_6} D₁ D₂ := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂
e' : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G'
this : Localization.Lifting L₁ W₁ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) G := Localization.Lifting.mk (W := W₁) e.symm
α : G' ≅ G := Localization.liftNatIso L₁ W₁ (L₁ ⋙ G') (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂) G' G e'.symm
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y
have this₁ : e = e' ≪≫ L₁.isoWhiskerLeft α
Tactic: have : e = e' ≪≫ Functor.isoWhiskerLeft _ α := by
    ext
    simp [α, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_3, u_3} C₂
inst_2 : Category.{v_4, u_4} C₃
inst_3 : Category.{v_5, u_5} D₁
inst_4 : Category.{v_6, u_6} D₂
inst_5 : Category.{v_7, u_7} D₃
W₁ : MorphismProperty.{v_2, u_2} C₁
W₂ : MorphismProperty.{v_3, u_3} C₂
W₃ : MorphismProperty.{v_4, u_4} C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_6 : L₁.IsLocalization W₁
L₂ : Functor.{v_3, v_6, u_3, u_6} C₂ D₂
inst_7 : L₂.IsLocalization W₂
L₃ : Functor.{v_4, v_7, u_4, u_7} C₃ D₃
inst_8 : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂ := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂
G' : Functor.{v_6, v_7, u_6, u_7} D₂ D₃ := Ψ.localizedFunctor (W₁ := W₂) (W₂ := W₃) L₂ L₃
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
e' : Ψ.functor (W₁ := W₂) (W₂ := W₃) ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso (Ψ.functor (W₁ := W₂) (W₂ := W₃)) L₂ L₃ G'
⊢ Ψ.homMap (W₁ := W₂) (W₂ := W₃) L₂ L₃ (Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ f) =
    (Φ.comp (W₁ := W₁) (W₂ := W₂) (W₃ := W₃) Ψ).homMap (W₁ := W₁) (W₂ := W₃) L₁ L₃ f
have rw : e'.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
    G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
  (Φ.functor (W₁ := W₁) (W₂ := W₂).associator (Ψ.functor (W₁ := W₂) (W₂ := W₃)) L₃ ≪≫
            Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e' ≪≫
              (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ G').symm ≪≫
                Functor.isoWhiskerRight e G' ≪≫ L₁.associator G G').hom.app
      X ≫
    (G ⋙ G').map f ≫
      (Φ.functor (W₁ := W₁) (W₂ := W₂).associator (Ψ.functor (W₁ := W₂) (W₂ := W₃)) L₃ ≪≫
              Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e' ≪≫
                (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ G').symm ≪≫
                  Functor.isoWhiskerRight e G' ≪≫ L₁.associator G G').inv.app
        Y
Tactic: rw [Φ.homMap_apply L₁ L₂ G e, Ψ.homMap_apply L₂ L₃ G' e',
    (Φ.comp Ψ).homMap_apply L₁ L₃ (G ⋙ G')
      (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e' ≪≫
      (Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight e _ ≪≫
      Functor.associator _ _ _)]