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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
⊢ Φ.IsRightDerivabilityStructure

Tactic:
by

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

Goal state before:
pp: J₁ J₂ : Type w
e : J₁ ≃ J₂
hJ₁ :
  ∀ {C : J₁ → Type u₁} {D : J₁ → Type u₂} [inst : (j : J₁) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J₁) → Category.{v₂, u₂} (D j)] (L : (j : J₁) → C j ⥤ D j) (W : (j : J₁) → MorphismProperty (C j))
    [∀ (j : J₁), (W j).ContainsIdentities] [∀ (j : J₁), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C₂ : J₂ → Type u₁
D₂ : J₂ → Type u₂
inst✝³ : (j : J₂) → Category.{v₁, u₁} (C₂ j)
inst✝² : (j : J₂) → Category.{v₂, u₂} (D₂ j)
L₂ : (j : J₂) → C₂ j ⥤ D₂ j
W₂ : (j : J₂) → MorphismProperty (C₂ j)
inst✝¹ : ∀ (j : J₂), (W₂ j).ContainsIdentities
inst✝ : ∀ (j : J₂), (L₂ j).IsLocalization (W₂ j)
L₁ : (j : J₁) → C₂ (e j) ⥤ D₂ (e j) := fun j ↦ L₂ (e j)
E : ((j : J₁) → C₂ (e j)) ≌ (i : J₂) → C₂ i := Pi.equivalenceOfEquiv C₂ e
E' : ((j : J₁) → D₂ (e j)) ≌ (i : J₂) → D₂ i := Pi.equivalenceOfEquiv D₂ e
this : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor
X✝ Y✝ : (i : J₁) → C₂ (e i)
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi (fun j ↦ W₂ (e j)) f
i : J₂
⊢ ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y), W₂ j g → W₂ j' ((Pi.eqToEquivalence C₂ h).functor.map g)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
⊢ W.HasLocalization

Tactic:
by

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

Goal state before:
pp: C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
⊢ ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence

Tactic:
by

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

Goal state before:
pp: J : Type w
inst✝⁴ : Fintype J
hJ :
  ∀ {C : J → Type u₁} {D : J → Type u₂} [inst : (j : J) → Category.{v₁, u₁} (C j)]
    [inst_1 : (j : J) → Category.{v₂, u₂} (D j)] (L : (j : J) → C j ⥤ D j) (W : (j : J) → MorphismProperty (C j))
    [∀ (j : J), (W j).ContainsIdentities] [∀ (j : J), (L j).IsLocalization (W j)],
    (Functor.pi L).IsLocalization (MorphismProperty.pi W)
C : Option J → Type u₁
D : Option J → Type u₂
inst✝³ : (j : Option J) → Category.{v₁, u₁} (C j)
inst✝² : (j : Option J) → Category.{v₂, u₂} (D j)
L : (j : Option J) → C j ⥤ D j
W : (j : Option J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : Option J), (W j).ContainsIdentities
inst✝ : ∀ (j : Option J), (L j).IsLocalization (W j)
L₁ : C none × ((i : J) → C (some i)) ⥤ D none × ((i : J) → D (some i)) := (L none).prod (Functor.pi fun j ↦ L (some j))
⊢ (i : Option J) →
    ((Pi.optionEquivalence C).symm.functor ⋙ Functor.pi L) ⋙ Pi.eval D i ≅
      (L₁ ⋙ (Pi.optionEquivalence D).symm.functor) ⋙ Pi.eval D i

Tactic:
by

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

Goal state before:
pp: J : Type w
inst✝⁴ : Finite J
C : J → Type u₁
D : J → Type u₂
inst✝³ : (j : J) → Category.{v₁, u₁} (C j)
inst✝² : (j : J) → Category.{v₂, u₂} (D j)
L : (j : J) → C j ⥤ D j
W : (j : J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : J), (W j).ContainsIdentities
inst✝ : ∀ (j : J), (L j).IsLocalization (W j)
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
by

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

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
E : J → C ≌ Discrete J ⥤ C := piEquivalenceFunctorDiscrete J C
E' : J → D ≌ Discrete J ⥤ D := piEquivalenceFunctorDiscrete J D
L₂ : (Discrete J ⥤ C) ⥤ Discrete J ⥤ D := (whiskeringRight (Discrete J) C D).obj L
L₁ : (J → C) ⥤ (J → D) := Functor.pi fun x ↦ L
⊢ L₂ ⋙ E'.inverse ≅ E.inverse ⋙ L₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (bifunctorComp₁₂ (curriedTensor C) (curriedTensor C)).flip = bifunctorComp₁₂ (curriedTensor C).flip (curriedTensor C)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)).flip =
    (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C).flip).flip.flip₁₃

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
⊢ bifunctorComp₁₂ (curriedTensor C) (curriedTensor C) =
    (bifunctorComp₂₃ (curriedTensor C).flip (curriedTensor C)).flip.flip₂₃

Tactic:
by

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

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : W.ContainsIdentities
inst✝ : L.IsLocalization W
⊢ ((whiskeringRight (Discrete J) C D).obj L).IsLocalization (W.functorCategory (Discrete J))

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 y : F ⊡ G
f : x ⟶ y
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst

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 y : F ⊡ G
f g : x ⟶ y
hₗ : f.fst = g.fst
hᵣ : f.snd = g.snd
⊢ f = g

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 y : F ⊡ G
eₗ : x.fst ≅ y.fst
eᵣ : x.snd ≅ y.snd
w : F.map eₗ.hom ≫ y.iso.hom = x.iso.hom ≫ G.map eᵣ.hom
⊢ F.map eₗ.inv ≫ x.iso.hom = y.iso.hom ≫ G.map eᵣ.inv

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 y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ (inv f).fst = inv f.fst

Tactic:
symm
  apply IsIso.inv_eq_of_hom_inv_id
  simp [← comp_fst]

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 y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ (inv f).fst = inv f.fst

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 y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ (inv f).snd = inv f.snd

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 y : F ⊡ G
f : x ⟶ y
h₁ : IsIso f.fst
h₂ : IsIso f.snd
⊢ F.map (inv f.fst) ≫ x.iso.hom = y.iso.hom ≫ G.map (inv f.snd)

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 y : F ⊡ G
f : x ⟶ y
h₁ : IsIso f.fst
h₂ : IsIso f.snd
⊢ f ≫ { fst := inv f.fst, snd := inv f.snd, w := ⋯ } = 𝟙 x ∧ { fst := inv f.fst, snd := inv f.snd, w := ⋯ } ≫ f = 𝟙 y

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
S S' : CatCommSqOver F G X
eₗ : S.fst ≅ S'.fst
eᵣ : S.snd ≅ S'.snd
w : whiskerRight eₗ.hom F ≫ S'.iso.hom = S.iso.hom ≫ whiskerRight eᵣ.hom G
⊢ whiskerRight eₗ.inv F ≫ S.iso.hom = S'.iso.hom ≫ whiskerRight eᵣ.inv G

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
⊢ ∀ (X_1 : X ⥤ F ⊡ G),
    { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ } =
      𝟙
        { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
          iso :=
            X_1.associator (π₁ F G) F ≪≫
              X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) 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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ {X_1 Y Z : X ⥤ F ⊡ G} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := ⋯ } =
      { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := ⋯ } ≫
        { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), 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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
⊢ ∀ (X_1 : CatCommSqOver F G X),
    { app := fun x ↦ { fst := (𝟙 X_1).fst.app x, snd := (𝟙 X_1).snd.app x, w := ⋯ }, naturality := ⋯ } =
      𝟙
        { obj := fun x ↦ { fst := X_1.fst.obj x, snd := X_1.snd.obj x, iso := X_1.iso.app x },
          map := fun {x y} f ↦ { fst := X_1.fst.map f, snd := X_1.snd.map f, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }

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
⊢ ∀ {X_1 Y Z : CatCommSqOver F G X} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
    { app := fun x ↦ { fst := (f ≫ g).fst.app x, snd := (f ≫ g).snd.app x, w := ⋯ }, naturality := ⋯ } =
      { app := fun x ↦ { fst := f.fst.app x, snd := f.snd.app x, w := ⋯ }, naturality := ⋯ } ≫
        { app := fun x ↦ { fst := g.fst.app x, snd := g.snd.app x, w := ⋯ }, naturality := ⋯ }

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
x✝¹ : X ⥤ F ⊡ G
x✝ : X
⊢ F.map (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).fst).hom ≫
      (((toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).obj x✝¹).obj x✝).iso.hom =
    (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).iso.hom ≫ G.map (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x✝¹).obj x✝).snd).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
⊢ ∀ {X_1 Y : X ⥤ F ⊡ G} (f : X_1 ⟶ Y),
    (𝟭 (X ⥤ F ⊡ G)).map f ≫
        (NatIso.ofComponents
            (fun x ↦
              mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj Y).obj x).snd) ⋯)
            ⋯).hom =
      (NatIso.ofComponents
            (fun x ↦
              mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X_1).obj x).fst) (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj X_1).obj x).snd) ⋯)
            ⋯).hom ≫
        (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X).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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
⊢ ∀ {X_1 Y : X} (f : X_1 ⟶ Y),
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.map f ≫
        (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj Y)).hom =
      (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj X_1)).hom ≫
        ((𝟭 (CatCommSqOver F G X)).obj x✝).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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
⊢ ∀ {X_1 Y : X} (f : X_1 ⟶ Y),
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.map f ≫
        (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj Y)).hom =
      (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj X_1)).hom ≫
        ((𝟭 (CatCommSqOver F G X)).obj x✝).snd.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
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
⊢ whiskerRight
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).fst.obj x))
            ⋯).hom
        F ≫
      ((𝟭 (CatCommSqOver F G X)).obj x✝).iso.hom =
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).iso.hom ≫
      whiskerRight
        (NatIso.ofComponents
            (fun x ↦
              Iso.refl
                (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj x))
            ⋯).hom
        G

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
⊢ ∀ (X_1 : X ⥤ F ⊡ G),
    (toCatCommSqOver F G X).map
          ((NatIso.ofComponents
                  (fun x ↦
                    NatIso.ofComponents
                      (fun x_1 ↦
                        mkIso (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).fst)
                          (Iso.refl (((𝟭 (X ⥤ F ⊡ G)).obj x).obj x_1).snd) ⋯)
                      ⋯)
                  ⋯).hom.app
            X_1) ≫
        (NatIso.ofComponents
                (fun x ↦
                  CatCommSqOver.mkIso
                    (NatIso.ofComponents
                      (fun x_1 ↦
                        Iso.refl
                          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).fst.obj
                            x_1))
                      ⋯)
                    (NatIso.ofComponents
                      (fun x_1 ↦
                        Iso.refl
                          (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x).snd.obj
                            x_1))
                      ⋯)
                    ⋯)
                ⋯).hom.app
          ((toCatCommSqOver F G X).obj X_1) =
      𝟙 ((toCatCommSqOver F G X).obj X_1)

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
x : X
⊢ F.map (e₁.app x).hom ≫ (K.obj x).iso.hom = (J.obj x).iso.hom ≫ G.map (e₂.app x).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
x✝¹ x✝ : X
f : x✝¹ ⟶ x✝
⊢ J.map f ≫ (mkIso (e₁.app x✝) (e₂.app x✝) ⋯).hom = (mkIso (e₁.app x✝¹) (e₂.app x✝¹) ⋯).hom ≫ K.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 : C
⊢ ((braidingNatIso L W ε).hom.app (L'.obj X)).app (L'.obj Y) =
    LaxMonoidal.μ L' X Y ≫ L'.map (β_ X Y).hom ≫ OplaxMonoidal.δ L' Y X

Tactic:
by

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

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
⊢ α = β

Tactic:
by

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

Goal state before:
pp: C : Type u
W X Y Z : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : W ⟶ X) (g : Y ⟶ Z),
    Quotient.map₂ Hom.tensor ⋯ f g =
      Quot.map (fun f ↦ f.whiskerRight Y) ⋯ f ≫ Quot.map (fun f ↦ Hom.whiskerLeft X f) ⋯ g

Tactic:
by

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

Goal state before:
pp: C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Quotient.map₂ Hom.tensor ⋯ f₁ f₂ ≫ Quotient.map₂ Hom.tensor ⋯ g₁ g₂ = Quotient.map₂ Hom.tensor ⋯ (f₁ ≫ g₁) (f₂ ≫ g₂)

Tactic:
by

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

Goal state before:
pp: C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Quotient.map₂ Hom.tensor ⋯ (Quotient.map₂ Hom.tensor ⋯ f₁ f₂) f₃ ≫
        { hom := ⟦Hom.α_hom Y₁ Y₂ Y₃⟧, inv := ⟦Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      { hom := ⟦Hom.α_hom X₁ X₂ X₃⟧, inv := ⟦Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        Quotient.map₂ Hom.tensor ⋯ f₁ (Quotient.map₂ Hom.tensor ⋯ f₂ f₃)

Tactic:
by

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

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : X ⟶ Y),
    Quot.map (fun f ↦ Hom.whiskerLeft unit f) ⋯ f ≫
        { hom := ⟦Hom.l_hom Y⟧, inv := ⟦Hom.l_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      { hom := ⟦Hom.l_hom X⟧, inv := ⟦Hom.l_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f : X ⟶ Y),
    Quot.map (fun f ↦ f.whiskerRight unit) ⋯ f ≫
        { hom := ⟦Hom.ρ_hom Y⟧, inv := ⟦Hom.ρ_inv Y⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      { hom := ⟦Hom.ρ_hom X⟧, inv := ⟦Hom.ρ_inv X⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ 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
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)
    toCatCommSqOver_mapIso_mkNatIso_eq_mkIso._auto_1
⊢ whiskerRight e₁.hom F ≫ ((toCatCommSqOver F G X).obj K).iso.hom =
    ((toCatCommSqOver F G X).obj J).iso.hom ≫ whiskerRight e₂.hom G

Tactic:
by

Goal state after: