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
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₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x y : CatCommSqOver F G X
f : x ⟶ y
⊢ ((transform X).obj (ψ.comp ψ')).map f ≫
      (mkIso (y.fst.associator ψ.left ψ'.left).symm (y.snd.associator ψ.right ψ'.right).symm ⋯).hom =
    (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯).hom ≫
      ((transform X).obj ψ ⋙ (transform X).obj ψ').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₁
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₁
φ φ' : CatCospanTransform F₁ G₁ F₂ G₂
α : φ ⟶ φ'
⊢ (transform X).map (ψ ◁ α) =
    (transformObjComp X ψ φ).hom ≫
      ((transform X).obj ψ).whiskerLeft ((transform X).map α) ≫ (transformObjComp X ψ φ').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
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₁
α : ψ ⟶ ψ'
φ : CatCospanTransform F₁ G₁ F₂ G₂
⊢ (transform X).map (α ▷ φ) =
    (transformObjComp X ψ φ).hom ≫
      whiskerRight ((transform X).map α) ((transform X).obj φ) ≫ (transformObjComp X ψ' φ).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
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₂
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₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
⊢ (transform X).map (α_ ψ φ τ).hom =
    (transformObjComp X (ψ.comp φ) τ).hom ≫
      whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
        (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
          ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫ (transformObjComp X ψ (φ.comp τ)).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
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₁
⊢ (transform X).map (λ_ ψ).hom =
    (transformObjComp X (CatCospanTransform.id F G) ψ).hom ≫
      whiskerRight (transformObjId X F G).hom ((transform X).obj ψ) ≫ ((transform X).obj ψ).leftUnitor.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
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₁
⊢ (transform X).map (ρ_ ψ).hom =
    (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)).hom ≫
      ((transform X).obj ψ).whiskerLeft (transformObjId X F₁ G₁).hom ≫ ((transform X).obj ψ).rightUnitor.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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
⊢ ∀ (X_1 : CatCommSqOver F G Y),
    { fst := U.whiskerLeft (𝟙 X_1).fst, snd := U.whiskerLeft (𝟙 X_1).snd, w := ⋯ } =
      𝟙
        { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
          iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
⊢ ∀ {X_1 Y_1 Z : CatCommSqOver F G Y} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { fst := U.whiskerLeft (f ≫ g).fst, snd := U.whiskerLeft (f ≫ g).snd, w := ⋯ } =
      { fst := U.whiskerLeft f.fst, snd := U.whiskerLeft f.snd, w := ⋯ } ≫
        { fst := U.whiskerLeft g.fst, snd := U.whiskerLeft g.snd, w := ⋯ }

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
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
⊢ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (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₂ ≫ (e₁.inv ⊗ₘ 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 : Type u₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
⊢ ∀ (X_1 : X ⥤ Y),
    { app := fun x ↦ { fst := whiskerRight (𝟙 X_1) x.fst, snd := whiskerRight (𝟙 X_1) x.snd, w := ⋯ },
        naturality := ⋯ } =
      𝟙
        {
          obj := fun S ↦
            { fst := X_1 ⋙ S.fst, snd := X_1 ⋙ S.snd,
              iso := X_1.associator S.fst F ≪≫ X_1.isoWhiskerLeft S.iso ≪≫ (X_1.associator S.snd G).symm },
          map := fun {S S'} φ ↦ { fst := X_1.whiskerLeft φ.fst, snd := X_1.whiskerLeft φ.snd, w := ⋯ }, map_id := ⋯,
          map_comp := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
I : C
inst✝ : ChosenPullbacksAlong (𝟙 I)
⊢ pushforward (𝟙 I) = 𝟭 (Over I)

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
⊢ ∀ {X_1 Y_1 Z : X ⥤ Y} (f : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z),
    { app := fun x ↦ { fst := whiskerRight (f ≫ g) x.fst, snd := whiskerRight (f ≫ g) x.snd, w := ⋯ },
        naturality := ⋯ } =
      { app := fun x ↦ { fst := whiskerRight f x.fst, snd := whiskerRight f x.snd, w := ⋯ }, naturality := ⋯ } ≫
        { app := fun x ↦ { fst := whiskerRight g x.fst, snd := whiskerRight g x.snd, w := ⋯ }, naturality := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).unit ≫ (pullback (𝟙 I)).whiskerLeft (pushforwardId I).hom =
    (pullbackPushforwardAdj (𝟙 I)).unit

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ Functor.whiskerRight (pushforwardId I).hom (pullback (𝟙 I)) ≫ (pullbackPushforwardAdj (𝟙 I)).counit =
    (pullbackPushforwardAdj (𝟙 I)).counit

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁴ : ChosenPullbacksAlong f
inst✝³ : ChosenPullbacksAlong g
inst✝² : ChosenPullbacksAlong (f ≫ g)
inst✝¹ : ExponentiableMorphism f
inst✝ : ExponentiableMorphism g
⊢ pushforward (f ≫ g) = pushforward f ⋙ pushforward 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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U : X ⥤ Y
V W : Y ⥤ Z
α : V ⟶ W
⊢ (precompose F G).map (U.whiskerLeft α) =
    (precomposeObjComp F G U V).hom ≫
      whiskerRight ((precompose F G).map α) ((precompose F G).obj U) ≫ (precomposeObjComp F G U W).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ (pullbackPushforwardAdj (f ≫ g)).unit ≫ (pullback (f ≫ g)).whiskerLeft (pushforwardComp f g).hom =
    (pullbackPushforwardAdj (f ≫ g)).unit

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₄
Y : Type u₅
Z : Type u₆
inst✝² : Category.{v₄, u₄} X
inst✝¹ : Category.{v₅, u₅} Y
inst✝ : Category.{v₆, u₆} Z
U V : X ⥤ Y
α : U ⟶ V
W : Y ⥤ Z
⊢ (precompose F G).map (whiskerRight α W) =
    (precomposeObjComp F G U W).hom ≫
      ((precompose F G).obj W).whiskerLeft ((precompose F G).map α) ≫ (precomposeObjComp F G V W).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁵ : ChosenPullbacksAlong f
inst✝⁴ : ChosenPullbacksAlong g
inst✝³ : ChosenPullbacksAlong (f ≫ g)
inst✝² : ExponentiableMorphism f
inst✝¹ : ExponentiableMorphism g
inst✝ : ExponentiableMorphism (f ≫ g)
⊢ Functor.whiskerRight (pushforwardComp f g).hom (pullback (f ≫ g)) ≫ (pullbackPushforwardAdj (f ≫ g)).counit =
    (pullbackPushforwardAdj (f ≫ g)).counit

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₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
⊢ (precompose F G).map (U.associator V W).hom =
    (precomposeObjComp F G (U ⋙ V) W).hom ≫
      ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
        (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
          whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫ (precomposeObjComp F G U (V ⋙ W)).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 : Type u₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
⊢ (precompose F G).map U.leftUnitor.hom =
    (precomposeObjComp F G (𝟭 X) U).hom ≫
      ((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom ≫ ((precompose F G).obj U).rightUnitor.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₄
Y : Type u₅
inst✝¹ : Category.{v₄, u₄} X
inst✝ : Category.{v₅, u₅} Y
U : X ⥤ Y
⊢ (precompose F G).map U.rightUnitor.hom =
    (precomposeObjComp F G U (𝟭 Y)).hom ≫
      whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U) ≫ ((precompose F G).obj U).leftUnitor.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
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₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
x y : CatCommSqOver F G Y
f : x ⟶ y
⊢ ((precompose F G).obj U ⋙ (transform X).obj ψ).map f ≫
      (mkIso (U.associator y.fst ψ.left) (U.associator y.snd ψ.right) ⋯).hom =
    (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯).hom ≫
      ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).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₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U V : X ⥤ Y
α : U ⟶ V
⊢ whiskerRight ((precompose F G).map α) ((transform X).obj ψ) ≫
      (CatCommSq.iso ((precompose F G).obj V) ((transform Y).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj V)).hom =
    (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj U)).hom ≫
      ((transform Y).obj ψ).whiskerLeft ((precompose F₁ G₁).map α)

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₁
ψ : CatCospanTransform F G F₁ G₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
⊢ (CatCommSq.iso ((precompose F G).obj (𝟭 X)) ((transform X).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj (𝟭 X))).hom ≫
      ((transform X).obj ψ).whiskerLeft (precomposeObjId F₁ G₁ X).hom =
    whiskerRight (precomposeObjId F G X).hom ((transform X).obj ψ) ≫
      ((transform X).obj ψ).leftUnitor.hom ≫ ((transform X).obj ψ).rightUnitor.inv

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
⊢ F.CoreMonoidal

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 Y : C
⊢ μ F (L.obj X) (L.obj Y) =
    ((Lifting.iso L W G F).hom.app X ⊗ₘ (Lifting.iso L W G F).hom.app Y) ≫
      μ G X Y ≫ (Lifting.iso L W G F).inv.app (X ⊗ Y) ≫ F.map (δ L X Y)

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
⊢ NatTrans.IsMonoidal (Lifting.iso L W G F).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
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₇
Y : Type u₈
Z : Type u₉
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
V : Y ⥤ Z
⊢ (CatCommSq.iso ((precompose F G).obj (U ⋙ V)) ((transform Z).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj (U ⋙ V))).hom ≫
      ((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom =
    whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ) ≫
      (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom ≫
        ((precompose F G).obj V).whiskerLeft
            (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
                ((precompose F₁ G₁).obj U)).hom ≫
          (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv ≫
            whiskerRight
                (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ)
                    ((precompose F₁ G₁).obj V)).hom
                ((precompose F₁ G₁).obj U) ≫
              (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V) ((precompose F₁ G₁).obj U)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
I : C
inst✝ : Closed I
A : C
⊢ toUnit A ≫ curryRightUnitorHom I = curry (fst I A)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
I : C
inst✝¹ : Closed I
inst✝ : ChosenPullbacksAlong (curryRightUnitorHom I)
X✝ Y✝ : Over I
u : X✝ ⟶ Y✝
⊢ (ihom I).map X✝.hom ≫ 𝟙 ((ihom I).obj I) = (ihom I).map (Hom.left u) ≫ (ihom I).map Y✝.hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
I : C
inst✝¹ : Closed I
inst✝ : ChosenPullbacksAlong (curryRightUnitorHom I)
X✝ Y✝ : Over I
u : X✝ ⟶ Y✝
⊢ curryRightUnitorHom I ≫ 𝟙 ((ihom I).obj I) = 𝟙 (𝟙_ C) ≫ curryRightUnitorHom I

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ curry ((β_ I A).hom ≫ Hom.left u) ≫ (ihom I).map X.hom = toUnit A ≫ curryRightUnitorHom I

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
X : Over I
A : C
v : A ⟶ (sections I).obj X
v₂ : A ⟶ (ihom I).obj X.left := v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curryRightUnitorHom I)
⊢ toUnit A ≫ curryRightUnitorHom I = v₂ ≫ (ihom I).map 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
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₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
x y : CatCommSqOver F G Y
f : x ⟶ y
⊢ ((transform Y).obj ψ ⋙ (precompose F₁ G₁).obj U).map f ≫
      (mkIso (U.associator y.fst ψ.left).symm (U.associator y.snd ψ.right).symm ⋯).hom =
    (mkIso (U.associator x.fst ψ.left).symm (U.associator x.snd ψ.right).symm ⋯).hom ≫
      ((precompose F G).obj U ⋙ (transform X).obj ψ).map f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalCategory D
F₁ F₂ : C ⥤ D
f : F₁ ⟶ F₂
X₁ : C
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((curriedTensorPre F₁).obj X₁).map f_1 ≫ (f.app X₁ ⊗ₘ f.app Y) =
      (f.app X₁ ⊗ₘ f.app X) ≫ ((curriedTensorPre F₂).obj X₁).map f_1

Tactic:
by

Goal state after: