awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
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))
rw₂ 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))
⊢ IsIso (α₁.app 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]

Premises used: CategoryTheory.isIso_comp_right_iff, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison_fac_app, CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
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))
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
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
⊢ 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:
dsimp [equivalence, Equivalence.mk]

Premises used: CategoryTheory.Localization.equivalence, CategoryTheory.Equivalence.mk
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
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
⊢ 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:
rw [liftNatTrans_app]

Premises used: CategoryTheory.Localization.liftNatTrans_app
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
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
⊢ 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:
dsimp [Lifting.iso]

Premises used: CategoryTheory.Localization.Lifting.iso
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
w 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
⊢ 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:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
⊢ G'.IsEquivalence

Tactic:
(equivalence L₁ W₁ L₂ W₂ G G' F F' α β).isEquivalence_functor

Premises used: CategoryTheory.Equivalence.isEquivalence_functor, CategoryTheory.Localization.equivalence
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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
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)
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)

Tactic:
obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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
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:
((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.Localization.inverts, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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
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:
exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, Iff.mp, CategoryTheory.Localization.inverts, CategoryTheory.Functor.mapArrow, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₁
⊢ 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')
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₁
h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
⊢ L₂ ⋙ lift (W := W₁) (E.functor ⋙ W₂.Q) h L₁ ≅ W₂.Q

Tactic:
calc
              L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
              _ ≅ _ := isoWhiskerRight E.counitIso.symm _
              _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    Functor.associator _ _ _
              _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫
                      isoWhiskerRight iso _)
              _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q :=
                    isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁)
              _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
              _ ≅ 𝟭 C₂ ⋙ W₂.Q := isoWhiskerRight E.counitIso _
              _ ≅ W₂.Q := leftUnitor _

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Functor.associator, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Localization.lift, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Localization.fac, CategoryTheory.Equivalence.counitIso, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₁
h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q)
⊢ L₂.IsLocalization W₂

Tactic:
exact
    { inverts := hW₂
      isEquivalence :=
        Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂)
          (E.functor ⋙ W₂.Q) (Localization.lift (E.functor ⋙ W₂.Q) h L₁) (by
            calc
              L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
              _ ≅ _ := isoWhiskerRight E.counitIso.symm _
              _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    Functor.associator _ _ _
              _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫
                      isoWhiskerRight iso _)
              _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q :=
                    isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁)
              _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
              _ ≅ 𝟭 C₂ ⋙ W₂.Q := isoWhiskerRight E.counitIso _
              _ ≅ W₂.Q := leftUnitor _)
          (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _) ≪≫ iso) }
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
⊢ (E.functor ⋙ L₂).IsLocalization W₁

Tactic:
haveI : (E.functor ⋙ L₂).IsLocalization W₁ :=
    of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
this : (E.functor ⋙ L₂).IsLocalization W₁
⊢ L₂.IsLocalization W₂

Tactic:
of_equivalence_source (E.functor ⋙ L₂) W₁ L₂ W₂ E hW₁ hW₂ (Iso.refl _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.IsLocalization.of_equivalence_source
-- Module: Mathlib.CategoryTheory.Localization.Equivalence
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₂
this : (E.functor ⋙ L₂).IsLocalization W₁
⊢ L₂.IsLocalization W₂

Tactic:
exact of_equivalence_source (E.functor ⋙ L₂) W₁ L₂ W₂ E hW₁ hW₂ (Iso.refl _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.IsLocalization.of_equivalence_source
-- Module: Mathlib.CategoryTheory.Localization.FiniteProducts
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
J : Type
inst_3 : HasProductsOfShape.{0, u₁, v₁} J C
inst_4 : W.IsStableUnderProductsOfShape J
⊢ MorphismProperty.IsInvertedBy (C := Functor.{0, v₁, 0, u₁} (Discrete J) C) (W.functorCategory (Discrete J)) (lim ⋙ L)

Tactic:
fun _ _ f hf => Localization.inverts L W _ (MorphismProperty.limMap f hf)

Premises used: CategoryTheory.Limits.lim, CategoryTheory.MorphismProperty.IsInvertedBy, CategoryTheory.MorphismProperty.limMap, CategoryTheory.Functor.map, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.FiniteProducts
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
J : Type
inst_3 : HasProductsOfShape.{0, u₁, v₁} J C
inst_4 : W.IsStableUnderProductsOfShape J
inst_5 : W.ContainsIdentities
inst_6 : Finite J
⊢ obj (whiskeringRight (Discrete J) C D) L ⋙ limitFunctor L W J ≅ lim ⋙ L

Tactic:
apply Localization.fac

Premises used: CategoryTheory.Localization.fac
-- Module: Mathlib.CategoryTheory.Localization.FiniteProducts
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
J : Type
inst_3 : HasProductsOfShape.{0, u₁, v₁} J C
inst_4 : W.IsStableUnderProductsOfShape J
inst_5 : W.ContainsIdentities
inst_6 : Finite J
F : Functor.{0, v₁, 0, u₁} (Discrete J) C
⊢ Eq (α :=
    obj (limitFunctor L W J ⋙ const (Discrete J)) (F ⋙ L) ⟶ obj (𝟭 (Functor.{0, v₂, 0, u₂} (Discrete J) D)) (F ⋙ L))
    (NatTrans.app (Adjunction.counit (adj L W J)) (F ⋙ L))
    (map (const (Discrete J)) (NatTrans.app (Iso.hom (compLimitFunctorIso L W J)) F) ≫
      NatTrans.app (Iso.hom (compConstIso (Discrete J) L)) (obj lim F) ≫
        whiskerRight (NatTrans.app (Adjunction.counit constLimAdj) F) L)

Tactic:
apply constLimAdj.localization_counit_app

Premises used: CategoryTheory.Adjunction.localization_counit_app, CategoryTheory.Limits.constLimAdj
-- Module: Mathlib.CategoryTheory.Localization.FiniteProducts
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
J : Type
inst_3 : HasProductsOfShape.{0, u₁, v₁} J C
inst_4 : W.IsStableUnderProductsOfShape J
inst_5 : W.ContainsIdentities
inst_6 : Finite J
F : Functor.{0, v₁, 0, u₁} (Discrete J) C
⊢ ∀ (j : Discrete J),
    Eq (α :=
      obj.{0, v₂, 0, u₂}
          (obj (const (Discrete J)) (Cone.pt (F := F ⋙ L) (coneOfAdj (L := limitFunctor L W J) (adj L W J) (F ⋙ L))))
          j ⟶
        (F ⋙ L).obj j)
      (NatTrans.app (Cone.π (coneOfAdj (L := limitFunctor L W J) (adj L W J) (F ⋙ L))) j)
      (Iso.hom (Iso.app (compLimitFunctorIso L W J) F) ≫ (L.mapCone (limit.cone F)).π.app j)

Tactic:
simp [adj_counit_app, constLimAdj]

Premises used: CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app, CategoryTheory.Limits.constLimAdj
-- Module: Mathlib.CategoryTheory.Localization.FiniteProducts
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
inst_3 : W.ContainsIdentities
J : Type
inst_4 : Finite J
inst_5 : HasProductsOfShape.{0, u₁, v₁} J C
inst_6 : W.IsStableUnderProductsOfShape J
⊢ HasProductsOfShape.{0, u₂, v₂} J D

Tactic:
hasLimitsOfShape_iff_isLeftAdjoint_const.2
    (HasProductsOfShapeAux.adj L W J).isLeftAdjoint

Premises used: Iff.mpr, CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const, CategoryTheory.Localization.HasProductsOfShapeAux.adj, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Localization.FiniteProducts
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_2 : L.IsLocalization W
inst_3 : W.ContainsIdentities
inst_4 : HasFiniteProducts.{v₁, u₁} C
inst_5 : W.IsStableUnderFiniteProducts
⊢ HasFiniteProducts.{v₂, u₂} D

Tactic:
⟨fun _ => hasProductsOfShape L W _⟩

Premises used: CategoryTheory.Limits.HasFiniteProducts.mk, CategoryTheory.Localization.hasProductsOfShape, Fin