mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v, u_1} C
inst✝⁷ : CartesianMonoidalCategory C
inst✝⁶ : Category.{w, u_2} D
inst✝⁵ : CartesianMonoidalCategory D
M N O X Y : C
inst✝⁴ : MonObj M
inst✝³ : MonObj N
inst✝² : MonObj O
inst✝¹ : BraidedCategory C
inst✝ : IsCommMonObj M
f g : X ⟶ M
⊢ f * g = g * f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ 𝟙_ C
g : X ⟶ Y
⊢ lift f g ≫ (λ_ Y).hom = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
M N : Mon C
inst✝ : IsCommMonObj N.X
f : M ⟶ N
n : ℕ
⊢ (f ^ n).hom = f.hom ^ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M N O X✝ Y : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : MonObj O
f : M ⟶ N
inst✝ : IsMonHom f
X : C
⊢ 1 ≫ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v, u_1} C
inst✝⁶ : CartesianMonoidalCategory C
inst✝⁵ : Category.{w, u_2} D
inst✝⁴ : CartesianMonoidalCategory D
M N O X✝ Y : C
inst✝³ : MonObj M
inst✝² : MonObj N
inst✝¹ : MonObj O
f : M ⟶ N
inst✝ : IsMonHom f
X : C
⊢ ∀ (x y : X ⟶ M), (x * y) ≫ f = x ≫ f * y ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X : C
inst✝ : MonObj M
⊢ monoidHom (𝟙 M) X = MonoidHom.id (X ⟶ M)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
M N O X : C
inst✝⁴ : MonObj M
inst✝³ : MonObj N
inst✝² : MonObj O
f : M ⟶ N
g : N ⟶ O
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ monoidHom (f ≫ g) X = (monoidHom g X).comp (monoidHom f X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ Y
g : X ⟶ 𝟙_ C
⊢ lift f g ≫ (ρ_ Y).hom = f

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
x✝ : Z ⟶ X ⊗ Y
⊢ (fun f ↦ lift f.1 f.2) ((fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X✝ Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
⊢ φ.unop ≫ 1 = 1

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
x✝ : (Z ⟶ X) × (Z ⟶ Y)
⊢ (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) ((fun f ↦ lift f.1 f.2) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ (β_ X Y).hom ≫ fst Y X = snd X Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X✝ Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
f₁ f₂ : unop X ⟶ M
⊢ φ.unop ≫ (f₁ * f₂) = φ.unop ≫ f₁ * φ.unop ≫ f₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ (β_ X Y).hom ≫ snd Y X = fst X Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ (β_ X Y).inv ≫ fst X Y = snd Y X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ (β_ X Y).inv ≫ snd X Y = fst Y X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y✝ : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ α.homEquiv'.toFun (f₁ * f₂) = α.homEquiv'.toFun f₁ * α.homEquiv'.toFun f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ ofRepresentableBy M (yonedaMonObj M) (yonedaMonObjRepresentableBy M) = inst✝

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorμ W X Y Z ≫ fst (W ⊗ Y) (X ⊗ Z) = fst W X ⊗ₘ fst Y Z

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMon.obj M ⟶ yonedaMon.obj N
⊢ η ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) = η

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorμ W X Y Z ≫ snd (W ⊗ Y) (X ⊗ Z) = snd W X ⊗ₘ snd Y Z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ fst (W ⊗ X) (Y ⊗ Z) = fst W Y ⊗ₘ fst X Z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
⊢ tensorδ W X Y Z ≫ snd (W ⊗ X) (Y ⊗ Z) = snd W Y ⊗ₘ snd X Z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
⊢ lift (snd X Y) (fst X Y) = (β_ X Y).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (snd W Y ≫ g') (fst W Y ≫ g) = (β_ W Y).hom ≫ (g' ⊗ₘ g)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ (β_ X Y).hom = lift g f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMon.obj M ⟶ yonedaMon.obj N
⊢ μ ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ (β_ Y X).inv = lift g f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMon.obj M ⟶ yonedaMon.obj N
⊢ yonedaMon.map { hom := (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X), isMonHom_hom := ⋯ } = α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
⊢ yonedaMon.essImage = fun F ↦ (F ⋙ forget MonCat).IsRepresentable

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ 1 ≫ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f₁ f₂ : X ⟶ M
g : M ⟶ N
inst✝ : IsMonHom g
⊢ (f₁ * f₂) ≫ g = f₁ ≫ g * f₂ ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v, u_1} C
inst✝³ : CartesianMonoidalCategory C
M N X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
f : X ⟶ M
n : ℕ
g : M ⟶ N
inst✝ : IsMonHom g
⊢ (f ^ n) ≫ g = (f ≫ g) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X Y : C
inst✝ : MonObj M
f : X ⟶ M
n : ℕ
h : Y ⟶ X
⊢ h ≫ f ^ n = (h ≫ f) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
inst✝ : BraidedCategory C
h : IsCommMonObj M
X : C
⊢ ∀ (a b : X ⟶ M), a * b = b * a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
inst✝ : BraidedCategory C
h : ∀ (X : C), IsMulCommutative (X ⟶ M)
⊢ (β_ M M).hom ≫ μ = μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
inst✝ : BraidedCategory C
⊢ IsCommMonObj M ↔ ∀ (X : C), IsMulCommutative (X ⟶ M)

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
e₁ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₁ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₁ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₁ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₁ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).hom ≫ (e₂ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (e₂ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    (α_ X Y Z).inv ≫ (e₂ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (e₂ Y Z).hom ≫ (α_ X Z Y).inv ≫ (e₂ X Z).hom ▷ Y
⊢ { braiding := e₁, braiding_naturality_right := a₁, braiding_naturality_left := b₁, hexagon_forward := c₁,
      hexagon_reverse := d₁ } =
    { braiding := e₂, braiding_naturality_right := a₂, braiding_naturality_left := b₂, hexagon_forward := c₂,
      hexagon_reverse := d₂ }

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ (a b : SymmetricCategory C), a = b

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : IsIso (terminalComparison F)
⊢ PreservesLimit (Functor.empty C) F

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (Functor.empty C) F
⊢ IsIso (terminalComparison F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
⊢ preservesTerminalIso (𝟭 C) = Iso.refl ((𝟭 C).obj (𝟙_ C))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (Functor.empty C) F
inst✝¹ : PreservesLimit (Functor.empty D) G
inst✝ : PreservesLimit (Functor.empty C) (F ⋙ G)
⊢ preservesTerminalIso (F ⋙ G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (fst A B) = fst (F.obj A) (F.obj B)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
A B : C
inst✝ : IsIso (prodComparison F A B)
⊢ inv (prodComparison F A B) ≫ F.map (snd A B) = snd (F.obj A) (F.obj B)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (f ⊗ₘ g) ≫ prodComparison F A' B' = prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : CommBialgCat R
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C : CommBialgCat R
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommBialgCat R
e : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
g : B ⟶ B'
⊢ F.map (A ◁ g) ≫ prodComparison F A B' = prodComparison F A B ≫ F.obj A ◁ F.map g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B : CommBialgCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Bialgebra R X
inst✝³ : CommRing Y
inst✝² : Bialgebra R Y
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X Y Z : Type v
inst✝⁵ : CommRing X
inst✝⁴ : Bialgebra R X
inst✝³ : CommRing Y
inst✝² : Bialgebra R Y
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : CartesianMonoidalCategory D
F : C ⥤ D
A B A' : C
f : A ⟶ A'
⊢ F.map (f ▷ B) ≫ prodComparison F A' B = prodComparison F A B ≫ F.map f ▷ F.obj B

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommBialgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : Bialgebra R X✝
inst✝³ : CommRing Y✝
inst✝² : Bialgebra R Y✝
inst✝¹ : CommRing Z
inst✝ : Bialgebra R Z
X Y : CommBialgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommBialgCat R)).map f)
⊢ IsIso f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
A B A' B' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (f ⊗ₘ g) = (F.map f ⊗ₘ F.map g) ≫ inv (prodComparison F A' B')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ (ofHom (counitAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op = (λ_ (op (of R A))).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
A B B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ inv (prodComparison F A B) ≫ F.map (A ◁ g) = F.obj A ◁ F.map g ≫ inv (prodComparison F A B')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ op (of R A) ◁ (ofHom (counitAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op = (ρ_ (op (of R A))).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
A B A' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
inst✝ : IsIso (prodComparison F A' B)
⊢ inv (prodComparison F A B) ≫ F.map (f ▷ B) = F.map f ▷ F.obj B ≫ inv (prodComparison F A' B)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
⊢ (ofHom (comulAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op =
    (α_ (op (of R A)) (op (of R A)) (op (of R A))).hom ≫
      op (of R A) ◁ (ofHom (comulAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.CommBialgCat

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
⊢ (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))).hom ≫ μ = μ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A B : C
⊢ prodComparison (F ⋙ G) A B = G.map (prodComparison F A B) ≫ prodComparison G (F.obj A) (F.obj B)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: A : Type u_2
B : Type u_3
f : A ≃ B
x : WithConv B
⊢ (WithConv.congr f).symm x = toConv (f.symm x.ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝ : AddMonoid A
⊢ ∀ (x y : WithConv A), (WithConv.equiv A).toFun (x + y) = (WithConv.equiv A).toFun x + (WithConv.equiv A).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝² : AddCommMonoid A
inst✝¹ : Semiring R
inst✝ : Module R A
⊢ ∀ (m : R) (x : WithConv A), (WithConv.addEquiv A).toFun (m • x) = (RingHom.id R) m • (WithConv.addEquiv A).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.WithConv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Semiring R
inst✝² : Module R A
inst✝¹ : AddCommMonoid B
inst✝ : Module R B
f : A ≃ₗ[R] B
x : WithConv B
⊢ (congrLinearEquiv f).symm x = toConv (f.symm x.ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
a : C
𝓡 : Coalgebra.Repr R a ι
f g : WithConv (C →ₗ[R] A)
⊢ (f * g).ofConv a = ∑ i ∈ 𝓡.index, f.ofConv (𝓡.left i) * g.ofConv (𝓡.right i)

Tactic:
by

Goal state after: