mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y Z : limit (F ⋙ objects)
f : limit (homDiagram X Y)
g : limit (homDiagram Y Z)
j j' : J
h : j ⟶ j'
⊢ (hom ((homDiagram X Z).map h)) ((hom (limit.π (homDiagram X Y) j)) f ≫ (hom (limit.π (homDiagram Y Z) j)) g) =
    (hom (limit.π (homDiagram X Y) j')) f ≫ (hom (limit.π (homDiagram Y Z) j')) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ Types.Limit.mk (homDiagram X✝ Y✝)
      (fun j ↦
        (hom (limit.π (homDiagram X✝ X✝) j))
            (Types.Limit.mk (homDiagram X✝ X✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) X✝)) ⋯) ≫
          (hom (limit.π (homDiagram X✝ Y✝) j)) x✝)
      ⋯ =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X✝ Y✝ : limit (F ⋙ objects)
x✝ : limit (homDiagram X✝ Y✝)
⊢ Types.Limit.mk (homDiagram X✝ Y✝)
      (fun j ↦
        (hom (limit.π (homDiagram X✝ Y✝) j)) x✝ ≫
          (hom (limit.π (homDiagram Y✝ Y✝) j))
            (Types.Limit.mk (homDiagram Y✝ Y✝) (fun x ↦ 𝟙 ((hom (limit.π (F ⋙ objects) x)) Y✝)) ⋯))
      ⋯ =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
W✝ X✝ Y✝ Z✝ : limit (F ⋙ objects)
x✝² : limit (homDiagram W✝ X✝)
x✝¹ : limit (homDiagram X✝ Y✝)
x✝ : limit (homDiagram Y✝ Z✝)
⊢ Types.Limit.mk (homDiagram W✝ Z✝)
      (fun j ↦
        (hom (limit.π (homDiagram W✝ Y✝) j))
            (Types.Limit.mk (homDiagram W✝ Y✝)
              (fun j ↦ (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹) ⋯) ≫
          (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝)
      ⋯ =
    Types.Limit.mk (homDiagram W✝ Z✝)
      (fun j ↦
        (hom (limit.π (homDiagram W✝ X✝) j)) x✝² ≫
          (hom (limit.π (homDiagram X✝ Z✝) j))
            (Types.Limit.mk (homDiagram X✝ Z✝)
              (fun j ↦ (hom (limit.π (homDiagram X✝ Y✝) j)) x✝¹ ≫ (hom (limit.π (homDiagram Y✝ Z✝) j)) x✝) ⋯))
      ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans (L.colimitIsoColimitGrothendieck (L ⋙ G))
              (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).symm)
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun x ↦ Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x)) ⋯)))
          (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
            (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)))
        (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))))
      (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)))
    ((𝟭 T).colimitIsoColimitGrothendieck G).symm
x✝ : Grothendieck (R ⋙ functor L)
⊢ colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).hom ≫
        (L.colimitIsoColimitGrothendieck (L ⋙ G)).inv ≫ colimit.pre G L =
    colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (HasColimit.isoOfNatIso (NatIso.ofComponents (fun x ↦ Iso.refl (G.obj (L.obj (left x.fiber)))) ⋯)).hom ≫
        (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
              (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)).hom ≫
          (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))).hom ≫
            (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)).hom ≫
              ((𝟭 T).colimitIsoColimitGrothendieck G).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
⊢ L.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (pre L (𝟭 T) (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
hsT : ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 ((𝟭 (AsSmall T)).obj X)
X : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x
⊢ (𝟭 (AsSmall T)).map (Iso.refl (F''.obj X).left).hom ≫
      ((pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)).obj X).hom =
    (F''.obj X).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
⊢ (CostructuredArrow.toOver L' (R'.obj b)).Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
⊢ L.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
X✝ Y✝ : ↑s.1
f : X✝ ⟶ Y✝
⊢ (hom (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
      X✝ ⟶
    (hom
        (limit.lift (F ⋙ objects) { pt := ↑s.pt, π := { app := fun j ↦ ↾(s.π.app j).toFunctor.obj, naturality := ⋯ } }))
      Y✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
j : J
h : X = Y
⊢ (hom (limit.π (homDiagram X Y) j)) (eqToHom h) = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
⊢ ∀ (X : ↑s.pt), (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.obj X = (s.π.app j).toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
j : J
X Y : ↑s.pt
f : X ⟶ Y
⊢ (limitConeLift F s ≫ (limitCone F).π.app j).toFunctor.map f = eqToHom ⋯ ≫ (s.π.app j).toFunctor.map f ≫ eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ m = limitConeLift F s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ (limit.cone (F ⋙ objects)).pt ≅ (objects.mapCone (HasLimits.limitCone F)).pt

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
J✝ : Type v
inst✝ : Category.{v, v} J✝
F : J✝ ⥤ Cat
⊢ ∀ (j : J✝),
    (limit.cone (F ⋙ objects)).π.app j =
      (Iso.refl (limit.cone (F ⋙ objects)).pt).hom ≫ (objects.mapCone (HasLimits.limitCone F)).π.app j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ f ≫ Δ = Δ ≫ (f ⊗ₘ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ ε = toUnit A

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : ComonObj A
⊢ Δ = lift (𝟙 A) (𝟙 A)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F₁ F₂ : W₁.Localization × W₂.Localization ⥤ E
h : W₁.Q.prod W₂.Q ⋙ F₁ = W₁.Q.prod W₂.Q ⋙ F₂
⊢ F₁ = F₂

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} D₁
inst✝² : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
inst✝ : W₂.ContainsIdentities
hF : (W₁.prod W₂).IsInvertedBy F
x✝¹ x✝ : C₁
f₁ : x✝¹ ⟶ x✝
hf₁ : W₁ f₁
⊢ IsIso ((curry.obj F).map f₁)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
X✝ Y✝ : C₂
f₂ : X✝ ⟶ Y✝
hf₂ : W₂ f₂
X₁ : W₁.Localization
⊢ IsIso (((prodLift₁ F hF).flip.map f₂).app X₁)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₁.Localization × W₂.Localization ⥤ E

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₁.Q.prod W₂.Q ⋙ prodLift F hF = F

Tactic:
by

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} D₁
inst✝⁴ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
⊢ (L₁.prod L₂).IsLocalization (W₁.prod W₂)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
inst✝¹⁰ : Category.{v_1, u_1} C₁
inst✝⁹ : Category.{v_2, u_2} C₂
inst✝⁸ : Category.{v_3, u_3} D₁
inst✝⁷ : Category.{v_4, u_4} D₂
inst✝⁶ : Category.{v_5, u_5} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
⊢ ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) =
    ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫
      (τ.app X₁).app X₂ ≫ ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
inst✝⁷ : Category.{v_5, u_5} E
inst✝⁶ : Category.{v_6, u_6} E'
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv).app
            (L₁.obj X₁)).app
        (L₂.obj X₂) =
      ((𝟙 F₁').app (L₁.obj X₁)).app (L₂.obj X₂)

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
E : Type u_5
E' : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D₁
inst✝⁸ : Category.{v_4, u_4} D₂
inst✝⁷ : Category.{v_5, u_5} E
inst✝⁶ : Category.{v_6, u_6} E'
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
inst✝³ : W₁.ContainsIdentities
inst✝² : W₂.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ E
inst✝¹ : Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'
inst✝ : Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂),
    ((lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv ≫ lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom).app
            (L₁.obj X₁)).app
        (L₂.obj X₂) =
      ((𝟙 F₂').app (L₁.obj X₁)).app (L₂.obj X₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Widesubcategory

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₂} D
F : C → D
P : MorphismProperty D
inst✝ : P.IsMultiplicative
X Y : InducedWideCategory D F P
f g : X ⟶ Y
eq : (wideInducedFunctor F P).map f = (wideInducedFunctor F P).map g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Widesubcategory

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : SymmetricCategory C
inst✝ : P.IsStableUnderBraiding
c c' : WideSubcategory P
⊢ (β_ c c').hom ≫ (β_ c' c).hom = 𝟙 (c ⊗ c')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
inst✝³ : P.IsStableUnderBraiding
c : WideSubcategory P
inst✝² : ComonObj c.obj
inst✝¹ : IsCommComonObj c.obj
inst✝ : P.IsStableUnderComonoid c.obj
⊢ Δ ≫ (β_ c c).hom = Δ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X : Dial C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
Y : Over X
⊢ (mapPullbackAdj (𝟙 X)).unit.app Y ≫ (pullbackId X).hom.app ((map (𝟙 X)).obj Y) = (mapPullbackAdj (𝟙 X)).unit.app Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
⊢ (mapPullbackAdj (𝟙 X)).unit ≫ (map (𝟙 X)).whiskerLeft (pullbackId X).hom = (mapPullbackAdj (𝟙 X)).unit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : ChosenPullbacksAlong (𝟙 X)
⊢ Functor.whiskerRight (pullbackId X).hom (map (𝟙 X)) ≫ (mapPullbackAdj (𝟙 X)).counit = (mapPullbackAdj (𝟙 X)).counit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ (mapPullbackAdj (f ≫ g)).unit ≫ (map (f ≫ g)).whiskerLeft (pullbackComp f g).hom = (mapPullbackAdj (f ≫ g)).unit

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : ChosenPullbacksAlong f
inst✝¹ : ChosenPullbacksAlong g
inst✝ : ChosenPullbacksAlong (f ≫ g)
⊢ Functor.whiskerRight (pullbackComp f g).hom (map (f ≫ g)) ≫ (mapPullbackAdj (f ≫ g)).counit =
    (mapPullbackAdj (f ≫ g)).counit

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
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_6} D₁
inst✝¹⁰ : Category.{v_5, u_7} D₂
inst✝⁹ : Category.{v_6, u_8} D₃
inst✝⁸ : Category.{v_13, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃

Tactic:
by

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₁₂ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
D₁₂ : Type u_9
D₂₃ : Type u_10
C : Type u_11
D : Type u_12
E : Type u_13
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_6} D₁
inst✝¹⁶ : Category.{v_5, u_7} D₂
inst✝¹⁵ : Category.{v_6, u_8} D₃
inst✝¹⁴ : Category.{v_7, u_4} C₁₂
inst✝¹³ : Category.{v_8, u_5} C₂₃
inst✝¹² : Category.{v_9, u_9} D₁₂
inst✝¹¹ : Category.{v_10, u_10} D₂₃
inst✝¹⁰ : Category.{v_11, u_11} C
inst✝⁹ : Category.{v_12, u_12} D
inst✝⁸ : Category.{v_13, u_13} E
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
L₃ : C₃ ⥤ D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
inst✝⁷ : L₁.IsLocalization W₁
inst✝⁶ : L₂.IsLocalization W₂
inst✝⁵ : L₃.IsLocalization W₃
inst✝⁴ : W₁.ContainsIdentities
inst✝³ : W₂.ContainsIdentities
inst✝² : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E
inst✝¹ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst✝ : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
e : F₁ ≅ F₂
⊢ ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
    (((lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₂ F₁' F₂' e.hom ≫ lift₃NatTrans L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₁ F₂' F₁' e.inv).app
                (L₁.obj X₁)).app
            (L₂.obj X₂)).app
        (L₃.obj X₃) =
      (((𝟙 F₁').app (L₁.obj X₁)).app (L₂.obj X₂)).app (L₃.obj X₃)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
⊢ φ₂ ≫ ((pullback g).obj (Over.mk f)).hom = U.hom

Tactic:
by

Goal state after: