mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ ∀ (X : W.Localization), G₁.obj X = G₂.obj X

Tactic:
rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_4
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ v₁₃ ≫ u₁₂ = v₁₃ ≫ u₁₂

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
this : Localization.Construction.lift W.Q ⋯ = 𝟭 W.Localization
⊢ (𝟭 W.Localization).IsEquivalence

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
this : Localization.Construction.lift W.Q ⋯ = 𝟭 W.Localization
⊢ (𝟭 W.Localization).IsEquivalence
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
hX : W (𝟙 X)
⊢ 𝟙 (L.obj X) = 𝟙 (L.obj X)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
F : D ⥤ E
⊢ L ⋙ F = L ⋙ F

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case mpr.cons
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map g.toPath)

Tactic:
]

Goal state after:
case mpr.cons
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map g.toPath)
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) ≫
      𝟙 (((Construction.WhiskeringLeftEquivalence.functor W E).obj (Construction.lift L ⋯ ⋙ Y✝)).obj.obj x✝) =
    𝟙 (((Construction.WhiskeringLeftEquivalence.functor W E).obj (Construction.lift L ⋯ ⋙ X✝)).obj.obj x✝) ≫
      ((whiskeringLeftFunctor L W E).map τ).hom.app x✝

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) ≫
      𝟙 (((Construction.WhiskeringLeftEquivalence.functor W E).obj (Construction.lift L ⋯ ⋙ Y✝)).obj.obj x✝) =
    𝟙 (((Construction.WhiskeringLeftEquivalence.functor W E).obj (Construction.lift L ⋯ ⋙ X✝)).obj.obj x✝) ≫
      ((whiskeringLeftFunctor L W E).map τ).hom.app x✝
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) = ((whiskeringLeftFunctor L W E).map τ).hom.app x✝

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) = ((whiskeringLeftFunctor L W E).map τ).hom.app x✝
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ B.functor.map (L.map (T.unitIso.hom.app X)) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ B.functor.map (L.map (T.unitIso.hom.app X))

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ B.functor.map (L.map (T.unitIso.hom.app X)) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ B.functor.map (L.map (T.unitIso.hom.app X))
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X)

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X)
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Full

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Full
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map ((iso T.symm.functor R L B.symm.functor).inv.app (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map ((iso T.symm.functor R L B.symm.functor).inv.app (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.symm.inverse.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map ((iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    (iso T L.symm.inverse R.symm.inverse B).hom.app X

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map ((iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    (iso T L.symm.inverse R.symm.inverse B).hom.app X
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
this : L.EssSurj
Y : D
⊢ τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (L.objObjPreimageIso Y).hom =
    τ'.app (L.obj (L.objPreimage Y)) ≫ F₂.map (L.objObjPreimageIso Y).hom

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (iso T L.functor R.functor B).hom.app X

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map
          (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
            R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
        R.counitIso.hom.app (B.obj (L.functor.obj X)) =
    (iso T L.functor R.functor B).hom.app X
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
⊢ L₂.IsLocalization W

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
⊢ L₂.IsLocalization W
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : W.Q.obj X.as.obj = X
⊢ (𝟙 W.Q ◫ τ₂).app X.as.obj = (𝟙 W.Q ◫ τ₂).app X.as.obj

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ : W.FunctorsInverting D
τ : X✝ ⟶ Y✝
⊢ X✝.obj = X✝.obj

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{v_4, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{v_4, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ : W.FunctorsInverting D
τ : X✝ ⟶ Y✝
⊢ Y✝.obj = Y✝.obj

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯ = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)

Tactic:
]

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯ = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)