mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ (toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh) = CatCommSqOver.mkIso e₁ e₂ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  autoParam
    (whiskerRight e₁.hom F ≫
        (K.associator (π₁ F G) F).hom ≫
          K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
      (J.associator (π₁ F G) F).hom ≫
        J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G)
    mkNatIso_eq._auto_1
⊢ whiskerRight e₁.hom F ≫ ((functorEquiv F G X).functor.obj K).iso.hom =
    ((functorEquiv F G X).functor.obj J).iso.hom ≫ whiskerRight e₂.hom G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ (L'.obj X) (L'.obj Y) (L'.obj Z)).hom ≫
      (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Y ⊗ L'.obj Z)).hom ≫
        (α_ (L'.obj Y) (L'.obj Z) (L'.obj X)).hom =
    (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Y)).hom ▷ L'.obj Z ≫
      (α_ (L'.obj Y) (L'.obj X) (L'.obj Z)).hom ≫
        L'.obj Y ◁ (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Z)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ mkNatIso e₁ e₂ coh = (functorEquiv F G X).fullyFaithfulFunctor.preimageIso (CatCommSqOver.mkIso e₁ e₂ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x y : CatCommSqOver F G X
f : x ⟶ y
⊢ whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
      { fst := y.fst ⋙ ψ.left, snd := y.snd ⋙ ψ.right,
            iso :=
              y.fst.associator ψ.left F₁ ≪≫
                y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (y.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight y.iso ψ.base ≪≫
                      y.snd.associator G ψ.base ≪≫
                        y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (y.snd.associator ψ.right G₁).symm }.iso.hom =
    { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
            iso :=
              x.fst.associator ψ.left F₁ ≪≫
                x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (x.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight x.iso ψ.base ≪≫
                      x.snd.associator G ψ.base ≪≫
                        x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (x.snd.associator ψ.right G₁).symm }.iso.hom ≫
      whiskerRight (whiskerRight f.snd ψ.right) G₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X Y : F C
t : X ⟶ Y
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
⊢ motive t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
⊢ ∀ (X_1 : CatCommSqOver F G X),
    { fst := whiskerRight (𝟙 X_1).fst ψ.left, snd := whiskerRight (𝟙 X_1).snd ψ.right, w := ⋯ } =
      𝟙
        { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
          iso :=
            X_1.fst.associator ψ.left F₁ ≪≫
              X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                (X_1.fst.associator F ψ.base).symm ≪≫
                  isoWhiskerRight X_1.iso ψ.base ≪≫
                    X_1.snd.associator G ψ.base ≪≫
                      X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                        (X_1.snd.associator ψ.right G₁).symm }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
⊢ ∀ {X_1 Y Z : CatCommSqOver F G X} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := ⋯ } =
      { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ } ≫
        { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, w := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
x y : X
f : x ⟶ y
⊢ ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                      iso :=
                        S.fst.associator ψ.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (S.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight S.iso ψ.base ≪≫
                                S.snd.associator G ψ.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (S.snd.associator ψ.right G₁).symm },
                  map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).fst.map
        f ≫
      η.left.app (S.fst.obj y) =
    η.left.app (S.fst.obj x) ≫
      ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                      iso :=
                        S.fst.associator ψ'.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (S.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight S.iso ψ'.base ≪≫
                                S.snd.associator G ψ'.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (S.snd.associator ψ'.right G₁).symm },
                  map := fun {x y} f ↦
                    { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).fst.map
        f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
x y : X
f : x ⟶ y
⊢ ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                      iso :=
                        S.fst.associator ψ.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                            (S.fst.associator F ψ.base).symm ≪≫
                              isoWhiskerRight S.iso ψ.base ≪≫
                                S.snd.associator G ψ.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                    (S.snd.associator ψ.right G₁).symm },
                  map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).snd.map
        f ≫
      η.right.app (S.snd.obj y) =
    η.right.app (S.snd.obj x) ≫
      ({
                  obj := fun S ↦
                    { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                      iso :=
                        S.fst.associator ψ'.left F₁ ≪≫
                          S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                            (S.fst.associator F ψ'.base).symm ≪≫
                              isoWhiskerRight S.iso ψ'.base ≪≫
                                S.snd.associator G ψ'.base ≪≫
                                  S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                    (S.snd.associator ψ'.right G₁).symm },
                  map := fun {x y} f ↦
                    { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                  map_id := ⋯, map_comp := ⋯ }.obj
              S).snd.map
        f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ (L'.obj X) (L'.obj Y) (L'.obj Z)).inv ≫
      (((braidingNatIso L W ε).app (L'.obj X ⊗ L'.obj Y)).app (L'.obj Z)).hom ≫
        (α_ (L'.obj Z) (L'.obj X) (L'.obj Y)).inv =
    L'.obj X ◁ (((braidingNatIso L W ε).app (L'.obj Y)).app (L'.obj Z)).hom ≫
      (α_ (L'.obj X) (L'.obj Z) (L'.obj Y)).inv ≫
        (((braidingNatIso L W ε).app (L'.obj X)).app (L'.obj Z)).hom ▷ L'.obj Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
⊢ BraidedCategory (LocalizedMonoidal L W ε)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : SymmetricCategory C
⊢ SymmetricCategory (LocalizedMonoidal L W ε)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
⊢ whiskerRight { app := fun y ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
      ({
                obj := fun S ↦
                  { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                    iso :=
                      S.fst.associator ψ'.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                          (S.fst.associator F ψ'.base).symm ≪≫
                            isoWhiskerRight S.iso ψ'.base ≪≫
                              S.snd.associator G ψ'.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                  (S.snd.associator ψ'.right G₁).symm },
                map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.obj
            S).iso.hom =
    ({
                obj := fun S ↦
                  { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                    iso :=
                      S.fst.associator ψ.left F₁ ≪≫
                        S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                          (S.fst.associator F ψ.base).symm ≪≫
                            isoWhiskerRight S.iso ψ.base ≪≫
                              S.snd.associator G ψ.base ≪≫
                                S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                  (S.snd.associator ψ.right G₁).symm },
                map := fun {x y} f ↦ { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }.obj
            S).iso.hom ≫
      whiskerRight { app := fun y ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Coherence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f : C → D
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (project f✝).map f ▷ (project f✝).obj x✝ ≫ (Iso.refl ((project f✝).obj Y✝ ⊗ (project f✝).obj x✝)).hom =
    (Iso.refl ((project f✝).obj X✝ ⊗ (project f✝).obj x✝)).hom ≫ (project f✝).map (f ▷ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
⊢ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app (L.obj X₂) =
    ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
⊢ ∀ (X_1 : CatCospanTransform F G F₁ G₁),
    {
        app := fun S ↦
          { fst := { app := fun y ↦ (𝟙 X_1).left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ (𝟙 X_1).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } =
      𝟙
        {
          obj := fun S ↦
            { fst := S.fst ⋙ X_1.left, snd := S.snd ⋙ X_1.right,
              iso :=
                S.fst.associator X_1.left F₁ ≪≫
                  S.fst.isoWhiskerLeft (CatCommSq.iso F X_1.left X_1.base F₁).symm ≪≫
                    (S.fst.associator F X_1.base).symm ≪≫
                      isoWhiskerRight S.iso X_1.base ≪≫
                        S.snd.associator G X_1.base ≪≫
                          S.snd.isoWhiskerLeft (CatCommSq.iso G X_1.right X_1.base G₁) ≪≫
                            (S.snd.associator X_1.right G₁).symm },
          map := fun {x y} f ↦ { fst := whiskerRight f.fst X_1.left, snd := whiskerRight f.snd X_1.right, w := ⋯ },
          map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝ : C → D
X✝ Y✝ x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X✝ ⟶ Y✝
⊢ (project f✝).obj x✝ ◁ (project f✝).map f ≫ (Iso.refl ((project f✝).obj x✝ ⊗ (project f✝).obj Y✝)).hom =
    (Iso.refl ((project f✝).obj x✝ ⊗ (project f✝).obj X✝)).hom ≫ (project f✝).map (x✝ ◁ f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
F₁ F₂ : C ⥤ E
F₁' F₂' : D ⥤ E
inst✝² : Lifting L W F₁ F₁'
inst✝¹ : Lifting L W F₂ F₂'
inst✝ : HasZeroMorphisms E
⊢ ∀ (X : C), (liftNatTrans L W F₁ F₂ F₁' F₂' 0).app (L.obj X) = NatTrans.app 0 (L.obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
inst✝² : Preadditive E
F₁ F₂ : C ⥤ E
F₁' F₂' : D ⥤ E
inst✝¹ : Lifting L W F₁ F₁'
inst✝ : Lifting L W F₂ F₂'
τ τ' : F₁ ⟶ F₂
⊢ ∀ (X : C),
    (liftNatTrans L W F₁ F₂ F₁' F₂' (τ + τ')).app (L.obj X) =
      (liftNatTrans L W F₁ F₂ F₁' F₂' τ + liftNatTrans L W F₁ F₂ F₁' F₂' τ').app (L.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
⊢ ∀ {X_1 Y Z : CatCospanTransform F G F₁ G₁} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    {
        app := fun S ↦
          { fst := { app := fun y ↦ (f ≫ g).left.app (S.fst.obj y), naturality := ⋯ },
            snd := { app := fun y ↦ (f ≫ g).right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
        naturality := ⋯ } =
      {
          app := fun S ↦
            { fst := { app := fun y ↦ f.left.app (S.fst.obj y), naturality := ⋯ },
              snd := { app := fun y ↦ f.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
          naturality := ⋯ } ≫
        {
          app := fun S ↦
            { fst := { app := fun y ↦ g.left.app (S.fst.obj y), naturality := ⋯ },
              snd := { app := fun y ↦ g.right.app (S.snd.obj y), naturality := ⋯ }, w := ⋯ },
          naturality := ⋯ }

Tactic:
by

Goal state after: