mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.fst = c.inl.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.snd = c.inr.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.unop.inl = c.fst.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.unop.inr = c.snd.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.inl = c.fst.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.inr = c.snd.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.unop.fst = (Iso.refl c.op.unop.pt).hom ≫ c.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.unop.snd = (Iso.refl c.op.unop.pt).hom ≫ c.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.unop.op.fst = (Iso.refl c.unop.op.pt).hom ≫ c.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.unop.op.snd = (Iso.refl c.unop.op.pt).hom ≫ c.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.unop.inl ≫ (Iso.refl c.op.unop.pt).hom = c.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.op.unop.inr ≫ (Iso.refl c.op.unop.pt).hom = c.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.unop.op.inl ≫ (Iso.refl c.unop.op.pt).hom = c.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ c.unop.op.inr ≫ (Iso.refl c.unop.op.pt).hom = c.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c ≃ IsLimit c.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsColimit c ≃ IsLimit c.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.op g.op ↔ HasPullback f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.unop g.unop ↔ HasPullback f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ HasPushout f.op g.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ HasPushout f.unop g.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.left = (pushout.inl f.op g.op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.right = (pushout.inr f.op g.op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pushout.inl f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.fst f g).op.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.snd f g).op.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (PushoutCocone.op (colimit.cocone (span f.unop g.unop))).π.app WalkingCospan.left = (pushout.inl f.unop g.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (PushoutCocone.op (colimit.cocone (span f.unop g.unop))).π.app WalkingCospan.right = (pushout.inr f.unop g.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pushout.inl f.unop g.unop ≫ (pullbackIsoOpPushout f g).hom.unop).op = (pullback.fst f g).unop.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pushout.inr f.unop g.unop ≫ (pullbackIsoOpPushout f g).hom.unop).op = (pullback.snd f g).unop.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.op g.op ↔ HasPushout f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ HasPullback f.unop g.unop ↔ HasPushout f g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ HasPullback f.op g.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ HasPullback f.unop g.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι.app WalkingSpan.left = (pullback.fst f.op g.op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ (PullbackCone.unop (limit.cone (cospan f.op g.op))).ι.app WalkingSpan.right = (pullback.snd f.op g.op).unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op).unop = (pushout.inl f g).op.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op).unop = (pushout.inr f g).op.unop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ (PullbackCone.op (limit.cone (cospan f.unop g.unop))).ι.app WalkingSpan.left = (pullback.fst f.unop g.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ (PullbackCone.op (limit.cone (cospan f.unop g.unop))).ι.app WalkingSpan.right = (pullback.snd f.unop g.unop).op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoOpPullback f g).inv.unop ≫ pullback.fst f.unop g.unop).op = (pushout.inl f g).unop.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoOpPullback f g).inv.unop ≫ pullback.snd f.unop g.unop).op = (pushout.inr f g).unop.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ g₁.op ≫ i₁.op = i₃.op ≫ f₁.op

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ g₂.op ≫ i₂.op = i₃.op ≫ f₂.op

Tactic:
by

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

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
⊢ ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (β (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (β Y Z).hom ≫ (α_ X Z Y).inv ≫ (β X Z).hom ▷ Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C =
    (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝¹ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    (pushoutIsoOpPullback g₁.op g₂.op).inv ≫
      pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pushoutIsoOpPullback f₁.op f₂.op).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ X).hom ▷ 𝟙_ C =
    (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ g₁.op ≫ i₃.op = i₁.op ≫ f₁.op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C =
    (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫
      (α_ (𝟙_ C) X (𝟙_ C)).hom ≫
        𝟙_ C ◁ (β_ X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ g₂.op ≫ i₃.op = i₂.op ≫ f₂.op

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫
      (α_ (𝟙_ C) X (𝟙_ C)).hom ≫
        𝟙_ C ◁ (β_ X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫
      (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫
        (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫
      (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫
        (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
⊢ (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      ((adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj (X ⊗ Y) ⊗ F.obj Z)).symm
          ((adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
        (adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (adj.homEquiv ((X ⊗ Y) ⊗ Z) (F.obj X ⊗ F.obj Y ⊗ F.obj Z))
      (F.map (α_ X Y Z).hom ≫
        (adj.homEquiv (X ⊗ Y ⊗ Z) (F.obj X ⊗ F.obj (Y ⊗ Z))).symm
            ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
          F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ (β_ X (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).hom ≫ (β_ X (𝟙_ C)).inv =
    (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    (pullbackIsoOpPushout g₁.op g₂.op).inv ≫
      pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pullbackIsoOpPushout f₁.op f₂.op).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).hom ≫ X ◁ (λ_ (𝟙_ C)).hom = (ρ_ X).hom ▷ 𝟙_ C

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝))
      (F.map (λ_ x✝).inv ≫
        (adj.homEquiv (𝟙_ C ⊗ x✝) (F.obj (𝟙_ C) ⊗ F.obj x✝)).symm
            ((adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj (𝟙_ C)) (F.obj x✝)) ≫
          (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G) ▷ F.obj x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cone.op.inl ≫ (Iso.refl p.cone.op.pt).hom = ⋯.cocone.inl

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cone.op.inr ≫ (Iso.refl p.cone.op.pt).hom = ⋯.cocone.inr

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.op.fst = (Iso.refl p.cocone.op.pt).hom ≫ ⋯.cone.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.op.snd = (Iso.refl p.cocone.op.pt).hom ≫ ⋯.cone.snd

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D))
      (F.map (ρ_ x✝).inv ≫
        (adj.homEquiv (x✝ ⊗ 𝟙_ C) (F.obj x✝ ⊗ F.obj (𝟙_ C))).symm
            ((adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫ μ G (F.obj x✝) (F.obj (𝟙_ C))) ≫
          F.obj x✝ ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cone.unop.inl ≫ (Iso.refl p.cone.unop.pt).hom = ⋯.cocone.inl

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cone.unop.inr ≫ (Iso.refl p.cone.unop.pt).hom = ⋯.cocone.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ : C
f✝ : W✝ ⟶ X✝
g✝ : W✝ ⟶ Y✝
h✝ : X✝ ⟶ Z✝
i✝ : Y✝ ⟶ Z✝
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ p.cocone.unop.fst = (Iso.refl p.cocone.unop.pt).hom ≫ ⋯.cone.fst

Tactic:
by

Goal state after: