mathlib-initiative/mathlib-tactics huggingface dataset:
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
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (λ_ (F.obj X)).hom = ε ▷ F.obj X ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom

Tactic:
[

Goal state after:
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
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (λ_ (F.obj X)).hom = ε ▷ F.obj X ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
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
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ ε ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom

Tactic:
[

Goal state after:
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
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X : C
⊢ (ρ_ (F.obj X)).hom = F.obj X ◁ ε ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
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 ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (F ⋙ G).map x✝¹ ▷ (F ⋙ G).obj x✝ ≫ μ G (F.obj Y✝) (F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ (F ⋙ G).map (x✝¹ ▷ x✝)

Tactic:
[

Goal state after:
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 ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (F ⋙ G).map x✝¹ ▷ (F ⋙ G).obj x✝ ≫ μ G (F.obj Y✝) (F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ (F ⋙ G).map (x✝¹ ▷ x✝)
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 ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ (F ⋙ G).map (x✝¹ ◁ x✝)

Tactic:
[

Goal state after:
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 ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ (F ⋙ G).map (x✝¹ ◁ x✝)
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 ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ G.obj (F.obj x✝) ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
[

Goal state after:
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 ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ G.obj (F.obj x✝) ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y : SemimoduleCat R
f : X ⟶ Y
Z : SemimoduleCat R
⊢ f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
X Y Z : SemimoduleCat R
f : Y ⟶ Z
⊢ X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
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
h : F.CoreMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (h.μIso x✝¹ X✝).inv ≫ F.obj x✝¹ ◁ F.map x✝ = F.map (x✝¹ ◁ x✝) ≫ (h.μIso x✝¹ Y✝).inv

Tactic:
rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_id, comp_id]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
inst✝ : HasLimit F
j : J
⊢ colimit.ι F.unop j ≫ (colimitUnopIsoOpLimit F).hom = (limit.π F (op j)).unop

Tactic:
simp [colimitUnopIsoOpLimit]

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✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
this : F.map (G.map f) ▷ F.obj (G.obj X') ≫ ?m.200 = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.237
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')

Tactic:
this

Goal state after:
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✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
this :
  F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.237
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.237) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')
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✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
this : F.obj (G.obj X) ◁ F.map (G.map g) ≫ ?m.305 = (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.342
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)

Tactic:
this

Goal state after:
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✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
this :
  F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.342
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ ?m.342) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)
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 X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (X ◁ g ≫ f ▷ Y') ≫ (β_ Y Y').hom = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ f

Tactic:
[

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (X ◁ g ≫ f ▷ Y') ≫ (β_ Y Y').hom = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ f
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono (F.map f)

Tactic:
[

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono (F.map f)
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono f

Tactic:
[

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)

Tactic:
[

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi f

Tactic:
[

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsColimit (span f f) F
inst✝ : Epi (F.map f)
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi f
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).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
(slice_lhs 2 3 => rw [← braiding_naturality_left]); simp only [assoc]

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₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        Y₁ ◁ (α_ Y₂ V₁ V₂).inv ≫ Y₁ ◁ (β_ Y₂ V₁).hom ▷ V₂ ≫ Y₁ ◁ (α_ V₁ Y₂ V₂).hom ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        X₁ ◁ (α_ X₂ U₁ U₂).inv ≫ X₁ ◁ (β_ X₂ U₁).hom ▷ U₂ ≫ X₁ ◁ (α_ U₁ X₂ U₂).hom ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)

Tactic:
[

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫
        Y₁ ◁ (α_ Y₂ V₁ V₂).inv ≫ Y₁ ◁ (β_ Y₂ V₁).hom ▷ V₂ ≫ Y₁ ◁ (α_ V₁ Y₂ V₂).hom ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv =
    ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫
        X₁ ◁ (α_ X₂ U₁ U₂).inv ≫ X₁ ◁ (β_ X₂ U₁).hom ▷ U₂ ≫ X₁ ◁ (α_ U₁ X₂ U₂).hom ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

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

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom

Tactic:
this

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (λ_ X₁).inv ▷ X₂

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv =
    𝟙_ C ◁ (λ_ X₁).inv ▷ X₂
| (λ_ X₁).hom ⊗ₘ (λ_ X₂).hom
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₁ X₂ : C
this :
  (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom
⊢ (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom

Tactic:
this

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ : C
this :
  (ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
    (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom
⊢ (α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫ X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫ X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom ≫ X₁ ◁ (λ_ X₂).hom =
    ((α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
        X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv ≫
          X₁ ◁ (β_ (𝟙_ C) X₂).hom ▷ 𝟙_ C ≫ X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).hom ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).inv) ≫
      (X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (X₁ ⊗ X₂)).hom
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1) → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔
    ∀ {x y : M}, ↑s x y → ↑t x y

Tactic:
[

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1) → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔
    ∀ {x y : M}, ↑s x y → ↑t x y
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ((lift R) f).range = Algebra.adjoin R (Set.range ⇑f)

Tactic:
[

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ((lift R) f).range = Algebra.adjoin R (Set.range ⇑f)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ Algebra.adjoin R (Set.range fun x ↦ ((lift R) f) ((ι R) x)) = Algebra.adjoin R (Set.range ⇑f)

Tactic:
lift_ι_apply

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
⊢ (e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R)).IsRightAdjoint

Tactic:
this

Goal state after:
R✝ : Type u
inst✝² : CommRing R✝
R : Type v
inst✝¹ : CommRing R
inst✝ : Small.{u, v} R
e : AlgCat R ≌ AlgCat (Shrink.{u, v} R) := restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)
this :
  e.inverse ⋙ forget₂ (AlgCat R) (ModuleCat R) =
    forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse
⊢ (forget₂ (AlgCat (Shrink.{u, v} R)) (ModuleCat (Shrink.{u, v} R)) ⋙
      (ModuleCat.restrictScalarsEquivalenceOfRingEquiv (Shrink.ringEquiv R)).inverse).IsRightAdjoint