mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) =
    G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
      lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))

Tactic:
ext

Goal state after:
case h_fst
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
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
        lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))) ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

case h_snd
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
⊢ lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)) ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.map (lift (F.map (fst A B)) (F.map (snd A B))) ≫
        lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))) ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f g h : WithConv (C →ₗ[R] A)
⊢ f * (g + h) = f * g + f * h

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (f * (g + h)).ofConv x✝ = (f * g + f * h).ofConv x✝
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f g h : WithConv (C →ₗ[R] A)
⊢ (f + g) * h = f * h + g * h

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ ((f + g) * h).ofConv x✝ = (f * h + g * h).ofConv x✝
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f : WithConv (C →ₗ[R] A)
⊢ 0 * f = 0

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (0 * f).ofConv x✝ = (ofConv 0) x✝
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f : WithConv (C →ₗ[R] A)
⊢ f * 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
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
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (f * 0).ofConv x✝ = (ofConv 0) x✝
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 : C
⊢ prodComparisonNatTrans (F ⋙ G) A =
    Functor.whiskerRight (prodComparisonNatTrans F A) G ≫ F.whiskerLeft (prodComparisonNatTrans G (F.obj A))

Tactic:
ext

Goal state after:
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 x✝ : C
⊢ (prodComparisonNatTrans (F ⋙ G) A).app x✝ =
    (Functor.whiskerRight (prodComparisonNatTrans F A) G ≫ F.whiskerLeft (prodComparisonNatTrans G (F.obj A))).app x✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A : C
⊢ prodComparisonNatTrans (𝟭 C) A = 𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A x✝ : C
⊢ (prodComparisonNatTrans (𝟭 C) A).app x✝ = (𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)).app x✝
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x y : A
⊢ toConv (toSpanSingleton R A x) * toConv (toSpanSingleton R A y) = toConv (toSpanSingleton R A (x * y))

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
x y : A
⊢ (toConv (toSpanSingleton R A x) * toConv (toSpanSingleton R A y)).ofConv 1 =
    (toConv (toSpanSingleton R A (x * y))).ofConv 1
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
⊢ prodComparisonBifunctorNatTrans (F ⋙ G) =
    Functor.whiskerRight (prodComparisonBifunctorNatTrans F) ((Functor.whiskeringRight C D E).obj G) ≫
      F.whiskerLeft (Functor.whiskerRight (prodComparisonBifunctorNatTrans G) ((Functor.whiskeringLeft C D E).obj F))

Tactic:
ext

Goal state after:
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
x✝¹ x✝ : C
⊢ ((prodComparisonBifunctorNatTrans (F ⋙ G)).app x✝¹).app x✝ =
    ((Functor.whiskerRight (prodComparisonBifunctorNatTrans F) ((Functor.whiskeringRight C D E).obj G) ≫
              F.whiskerLeft
                (Functor.whiskerRight (prodComparisonBifunctorNatTrans G) ((Functor.whiskeringLeft C D E).obj F))).app
          x✝¹).app
      x✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ prodComparisonIso (𝟭 C) A B = Iso.refl ((𝟭 C).obj (A ⊗ B))

Tactic:
ext

Goal state after:
case h_fst
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ (prodComparisonIso (𝟭 C) A B).hom ≫ fst ((𝟭 C).obj A) ((𝟭 C).obj B) =
    (Iso.refl ((𝟭 C).obj (A ⊗ B))).hom ≫ fst ((𝟭 C).obj A) ((𝟭 C).obj B)

case h_snd
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
A B : C
⊢ (prodComparisonIso (𝟭 C) A B).hom ≫ snd ((𝟭 C).obj A) ((𝟭 C).obj B) =
    (Iso.refl ((𝟭 C).obj (A ⊗ B))).hom ≫ snd ((𝟭 C).obj A) ((𝟭 C).obj B)
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
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ prodComparisonIso (F ⋙ G) A B = G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)

Tactic:
ext

Goal state after:
case h_fst
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
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

case h_snd
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
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
⊢ (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
      (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)) =
    (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)

Tactic:
ext

Goal state after:
case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom)).comp
        includeLeft)
      x✝

case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ Z✝ : CommAlgCat R
f✝ : Y✝ ⟶ Z✝
x✝ : ↑Y✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (AlgHom.id R ↑X✝) (Hom.hom f✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑X✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Y✝)).hom))).comp
        includeRight)
      x✝
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
⊢ (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
      (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)) =
    (Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)

Tactic:
ext

Goal state after:
case ha
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑X✝
⊢ (((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
            (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝))).comp
        includeLeft)
      x✝ =
    (((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
            (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom)).comp
        includeLeft)
      x✝

case hb
R : Type u
inst✝ : CommRing R
A B C D X✝ Y✝ : CommAlgCat R
f✝ : X✝ ⟶ Y✝
Z✝ : CommAlgCat R
x✝ : ↑Z✝
⊢ ((AlgHom.restrictScalars R
            ((Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑Y✝ ↑Z✝)).hom).comp
              (Algebra.TensorProduct.map (Hom.hom f✝) (AlgHom.id R ↑Z✝)))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map (AlgHom.id R ↑Z✝) (Hom.hom f✝)).comp
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑X✝ ↑Z✝)).hom))).comp
        includeRight)
      x✝
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ =
    (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ ↑(TensorProduct.assoc R C C C).symm) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (mul' R A ∘ₗ ((f * g).ofConv ⊗ₘ h.ofConv) ∘ₗ δ) x✝ =
    ((mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
        (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ ↑(TensorProduct.assoc R C C C).symm) ∘ₗ lTensor C δ ∘ₗ δ)
      x✝
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✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
constructor

Goal state after:
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✝ : ∀ (A B : C), IsIso (prodComparison F A B)
⊢ autoParam (∀ {K : Discrete WalkingPair ⥤ C}, PreservesLimit K F) PreservesLimitsOfShape.preservesLimit._autoParam
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
⊢ ((↑(assoc R R R ↑T ↑U ↑S)).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
      ↑(assoc R R R ↑S ↑T ↑U) =
    ((Algebra.TensorProduct.map (AlgHom.id R ↑T) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
          ↑(assoc R R R ↑T ↑S ↑U)).comp
      (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom) (AlgHom.id R ↑U))

Tactic:
ext

Goal state after:
case ha.ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑S
⊢ (((((↑(assoc R R R ↑T ↑U ↑S)).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
                ↑(assoc R R R ↑S ↑T ↑U)).comp
            includeLeft).comp
        includeLeft)
      x✝ =
    (((((Algebra.TensorProduct.map (AlgHom.id R ↑T) (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
                    ↑(assoc R R R ↑T ↑S ↑U)).comp
                (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom)
                  (AlgHom.id R ↑U))).comp
            includeLeft).comp
        includeLeft)
      x✝

case ha.hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑T
⊢ ((AlgHom.restrictScalars R
            ((((↑(assoc R R R ↑T ↑U ↑S)).comp
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
                  ↑(assoc R R R ↑S ↑T ↑U)).comp
              includeLeft)).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((((Algebra.TensorProduct.map (AlgHom.id R ↑T)
                          (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
                      ↑(assoc R R R ↑T ↑S ↑U)).comp
                  (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom)
                    (AlgHom.id R ↑U))).comp
              includeLeft)).comp
        includeRight)
      x✝

case hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑U
⊢ ((AlgHom.restrictScalars R
            (((↑(assoc R R R ↑T ↑U ↑S)).comp
                  (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S) (↑T ⊗[R] ↑U))).hom)).comp
              ↑(assoc R R R ↑S ↑T ↑U))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            (((Algebra.TensorProduct.map (AlgHom.id R ↑T)
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)).comp
                  ↑(assoc R R R ↑T ↑S ↑U)).comp
              (Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑T)).hom)
                (AlgHom.id R ↑U)))).comp
        includeRight)
      x✝
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: case e_f
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ mul' R A ∘ₗ rTensor A (mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm = mul' R A ∘ₗ lTensor A (mul' R A)

Tactic:
ext

Goal state after:
case e_f
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x✝² x✝¹ x✝ : A
⊢ ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry (mul' R A ∘ₗ rTensor A (mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm)) x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (mul' R A ∘ₗ lTensor A (mul' R A))) x✝²)) x✝¹) x✝
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
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
x✝¹ : P.FullSubcategory
x✝ : x✝¹ ⟶ 𝟙_ P.FullSubcategory
⊢ x✝ = ObjectProperty.homMk (toUnit x✝¹.obj)

Tactic:
ext

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
x✝¹ : P.FullSubcategory
x✝ : x✝¹ ⟶ 𝟙_ P.FullSubcategory
⊢ x✝.hom = (ObjectProperty.homMk (toUnit x✝¹.obj)).hom
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
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ ObjectProperty.homMk (fst X.obj Y.obj) =
    X ◁ (IsTerminal.ofUniqueHom (fun X ↦ ObjectProperty.homMk (toUnit X.obj)) ⋯).from Y ≫ (ρ_ X).hom

Tactic:
ext

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ (ObjectProperty.homMk (fst X.obj Y.obj)).hom =
    (X ◁ (IsTerminal.ofUniqueHom (fun X ↦ ObjectProperty.homMk (toUnit X.obj)) ⋯).from Y ≫ (ρ_ X).hom).hom
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ (mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ =
    mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
x✝ : C
⊢ ((mul' R A ∘ₗ lTensor A (mul' R A)) ∘ₗ (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ) x✝ =
    (mul' R A ∘ₗ (f.ofConv ⊗ₘ mul' R A ∘ₗ (g.ofConv ⊗ₘ h.ofConv) ∘ₗ δ) ∘ₗ δ) x✝
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
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ ObjectProperty.homMk (snd X.obj Y.obj) =
    (IsTerminal.ofUniqueHom (fun X ↦ ObjectProperty.homMk (toUnit X.obj)) ⋯).from X ▷ Y ≫ (λ_ Y).hom

Tactic:
ext

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ (ObjectProperty.homMk (snd X.obj Y.obj)).hom =
    ((IsTerminal.ofUniqueHom (fun X ↦ ObjectProperty.homMk (toUnit X.obj)) ⋯).from X ▷ Y ≫ (λ_ Y).hom).hom