awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 W.Localization

Tactic:
hasFiniteProducts W.Q W

Premises used: CategoryTheory.Localization.hasFiniteProducts, CategoryTheory.MorphismProperty.Q
-- 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
⊢ PreservesFiniteProducts W.Q

Tactic:
preservesFiniteProducts W.Q W

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.preservesFiniteProducts
-- 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
inst_6 : MorphismProperty.HasLocalization.{u_1, v₁, u₁} W
⊢ HasFiniteProducts.{u_1, u₁} (MorphismProperty.Localization'.{u_1, v₁, u₁} W)

Tactic:
hasFiniteProducts W.Q' W

Premises used: CategoryTheory.Localization.hasFiniteProducts, CategoryTheory.MorphismProperty.Q'
-- 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
inst_6 : MorphismProperty.HasLocalization.{u_1, v₁, u₁} W
⊢ PreservesFiniteProducts.{v₁, u_1, u₁, u₁} (D := MorphismProperty.Localization'.{u_1, v₁, u₁} W) W.Q'

Tactic:
preservesFiniteProducts W.Q' W

Premises used: CategoryTheory.Localization.preservesFiniteProducts, CategoryTheory.MorphismProperty.Q'
-- Module: Mathlib.CategoryTheory.Localization.HasLocalization
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : HasLocalization.{w, v, u} W
⊢ Functor.IsLocalization.{v, u, w, u} (D := Localization'.{w, v, u} W) W.Q' W

Tactic:
HasLocalization.hL

Premises used: CategoryTheory.MorphismProperty.HasLocalization.hL, CategoryTheory.MorphismProperty.Q', CategoryTheory.MorphismProperty.Localization'
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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
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)
⊢ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ (L₁.map f) = L₂.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map f)

Tactic:
dsimp [homMap]

Premises used: CategoryTheory.LocalizerMorphism.homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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 : C₁
⊢ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))

Tactic:
simpa using Φ.homMap_map L₁ L₂ (𝟙 X)

Premises used: CategoryTheory.LocalizerMorphism.homMap_map, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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 Z : C₁
f : L₁.obj X ⟶ L₁.obj Y
g : L₁.obj Y ⟶ L₁.obj Z
⊢ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ (f ≫ g) =
    Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ f ≫ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ g

Tactic:
simp [homMap]

Premises used: CategoryTheory.LocalizerMorphism.homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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'
change : e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y
⊢ Φ.homMap (W₁ := W₁) (W₂ := W₂) L₁ L₂ f = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
change e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = _

Premises used: CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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
w : ∀ (x : C₁), e.hom.app x = (e' ≪≫ L₁.isoWhiskerLeft α).hom.app x
⊢ e = e' ≪≫ L₁.isoWhiskerLeft α

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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
x : C₁
⊢ e.hom.app x = (e' ≪≫ L₁.isoWhiskerLeft α).hom.app x

Tactic:
simp [α, this]
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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 α

Tactic:
have : e = e' ≪≫ Functor.isoWhiskerLeft _ α := by
    ext
    simp [α, this]
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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_1 : 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
this : e = e' ≪≫ L₁.isoWhiskerLeft α
⊢ e'.hom.app X ≫ G'.map f ≫ e'.inv.app Y = e.hom.app X ≫ G.map f ≫ e.inv.app Y

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C₁ : Type u_2
D₁ : Type u_5
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_5, u_5} D₁
W₁ : MorphismProperty.{v_2, u_2} C₁
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_2 : L₁.IsLocalization W₁
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
⊢ (id W₁).homMap (W₁ := W₁) (W₂ := W₁) L₁ L₁ f = f

Tactic:
simpa using (id W₁).homMap_apply L₁ L₁ (𝟭 D₁) (Iso.refl _) f

Premises used: CategoryTheory.Functor.id, CategoryTheory.Iso.refl, CategoryTheory.LocalizerMorphism.homMap_apply, CategoryTheory.LocalizerMorphism.id
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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'
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
⊢ Ψ.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

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 _ _ _)]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.LocalizerMorphism.homMap_apply, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.LocalizerMorphism.comp
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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'
dsimp :
  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) =
    (𝟙 (L₃.obj (Ψ.functor (W₁ := W₂) (W₂ := W₃).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))) ≫
        e'.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
          𝟙 (G'.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))) ≫
            G'.map (e.hom.app X) ≫ 𝟙 (G'.obj (G.obj (L₁.obj X)))) ≫
      G'.map (G.map f) ≫
        (((𝟙 (G'.obj (G.obj (L₁.obj Y))) ≫ G'.map (e.inv.app Y)) ≫
              𝟙 (G'.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))) ≫
            e'.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)) ≫
          𝟙 (L₃.obj (Ψ.functor (W₁ := W₂) (W₂ := W₃).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
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'
⊢ 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) =
    (𝟙 (L₃.obj (Ψ.functor (W₁ := W₂) (W₂ := W₃).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))) ≫
        e'.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
          𝟙 (G'.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))) ≫
            G'.map (e.hom.app X) ≫ 𝟙 (G'.obj (G.obj (L₁.obj X)))) ≫
      G'.map (G.map f) ≫
        (((𝟙 (G'.obj (G.obj (L₁.obj Y))) ≫ G'.map (e.inv.app Y)) ≫
              𝟙 (G'.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))) ≫
            e'.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)) ≫
          𝟙 (L₃.obj (Ψ.functor (W₁ := W₂) (W₂ := W₃).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))

Tactic:
simp only [Functor.map_comp, assoc, comp_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
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_1, u_1} C
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
inst_4 : Category.{v_5, u_5} D₁
inst_5 : Category.{v_6, u_6} D₂
inst_6 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_7 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_8 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_9 : L₃.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
rw :
  ((LocalizerMorphism.id W).comp (W₁ := W) (W₂ := W) (W₃ := W) (LocalizerMorphism.id W)).homMap (W₁ := W) (W₂ := W) L₁
      L₁ f =
    f
⊢ (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₁
      ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f) =
    f

Tactic:
rw [LocalizerMorphism.homMap_homMap]

Premises used: CategoryTheory.LocalizerMorphism.homMap_homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
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_1, u_1} C
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
inst_4 : Category.{v_5, u_5} D₁
inst_5 : Category.{v_6, u_6} D₂
inst_6 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_7 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_8 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_9 : L₃.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ ((LocalizerMorphism.id W).comp (W₁ := W) (W₂ := W) (W₃ := W) (LocalizerMorphism.id W)).homMap (W₁ := W) (W₂ := W) L₁
      L₁ f =
    f

Tactic:
apply LocalizerMorphism.id_homMap

Premises used: CategoryTheory.LocalizerMorphism.id_homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
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_1, u_1} C
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
inst_4 : Category.{v_5, u_5} D₁
inst_5 : Category.{v_6, u_6} D₂
inst_6 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_7 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_8 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_9 : L₃.IsLocalization W
X Y Z : C
g : L₂.obj X ⟶ L₂.obj Y
rw :
  ((LocalizerMorphism.id W).comp (W₁ := W) (W₂ := W) (W₃ := W) (LocalizerMorphism.id W)).homMap (W₁ := W) (W₂ := W) L₂
      L₂ g =
    g
⊢ (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂
      ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₁ g) =
    g

Tactic:
rw [LocalizerMorphism.homMap_homMap]

Premises used: CategoryTheory.LocalizerMorphism.homMap_homMap
-- Module: Mathlib.CategoryTheory.Localization.HomEquiv
Goal:
C : Type u_1
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_1, u_1} C
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
inst_4 : Category.{v_5, u_5} D₁
inst_5 : Category.{v_6, u_6} D₂
inst_6 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_7 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_8 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_9 : L₃.IsLocalization W
X Y Z : C
g : L₂.obj X ⟶ L₂.obj Y
⊢ ((LocalizerMorphism.id W).comp (W₁ := W) (W₂ := W) (W₃ := W) (LocalizerMorphism.id W)).homMap (W₁ := W) (W₂ := W) L₂
      L₂ g =
    g

Tactic:
apply LocalizerMorphism.id_homMap

Premises used: CategoryTheory.LocalizerMorphism.id_homMap