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
M : Mon C
f : M ⟶ 𝟙_ (Mon C)
⊢ f.hom = { hom := toUnit M.X, isMonHom_hom := ⋯ }.hom

Tactic:
;

Goal state after:
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
M : Mon C
f : M ⟶ 𝟙_ (Mon C)
⊢ f.hom = { hom := toUnit M.X, isMonHom_hom := ⋯ }.hom
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
M N : Mon C
⊢ { hom := fst M.X N.X, isMonHom_hom := ⋯ }.hom =
    (M ◁ (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N ≫ (ρ_ M).hom).hom

Tactic:
;

Goal state after:
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
M N : Mon C
⊢ { hom := fst M.X N.X, isMonHom_hom := ⋯ }.hom =
    (M ◁ (IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N ≫ (ρ_ M).hom).hom
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
M N : Mon C
⊢ M.X ◁ isTerminalTensorUnit.from N.X =
    M.X ◁ ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N).hom

Tactic:
;

Goal state after:
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
M N : Mon C
⊢ M.X ◁ isTerminalTensorUnit.from N.X =
    M.X ◁ ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from N).hom
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
M N : Mon C
⊢ { hom := snd M.X N.X, isMonHom_hom := ⋯ }.hom =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M ▷ N ≫ (λ_ N).hom).hom

Tactic:
;

Goal state after:
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
M N : Mon C
⊢ { hom := snd M.X N.X, isMonHom_hom := ⋯ }.hom =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M ▷ N ≫ (λ_ N).hom).hom
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
M N : Mon C
⊢ isTerminalTensorUnit.from M.X ▷ N.X =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M).hom ▷ N.X

Tactic:
;

Goal state after:
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
M N : Mon C
⊢ isTerminalTensorUnit.from M.X ▷ N.X =
    ((IsTerminal.ofUniqueHom (fun M ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯).from M).hom ▷ N.X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ Z₁ Z₂ : C
this : MonoidalCategoryStruct C :=
  { tensorObj := ofChosenFiniteProducts.tensorObj ℬ,
    whiskerLeft := fun X {x x_1} g ↦ ofChosenFiniteProducts.tensorHom ℬ (𝟙 X) g,
    whiskerRight := fun {x x_1} f Y ↦ ofChosenFiniteProducts.tensorHom ℬ f (𝟙 Y),
    tensorHom := fun {X₁ Y₁ X₂ Y₂} ↦ ofChosenFiniteProducts.tensorHom ℬ, tensorUnit := 𝒯.cone.pt,
    associator := BinaryFan.associatorOfLimitCone ℬ,
    leftUnitor := fun X ↦ BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X).isLimit,
    rightUnitor := fun X ↦ BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit }
X Y T✝ : C
f : T✝ ⟶ X
g : T✝ ⟶ Y
m : T✝ ⟶ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).pt
hf : m ≫ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).fst = f
hg : m ≫ (BinaryFan.mk (BinaryFan.fst (ℬ X Y).cone) (BinaryFan.snd (ℬ X Y).cone)).snd = g
⊢ m ≫ BinaryFan.snd (ℬ X Y).cone = ↑(BinaryFan.IsLimit.lift' (ℬ X Y).isLimit f g) ≫ BinaryFan.snd (ℬ X Y).cone

Tactic:
by simpa using hg

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₁ f₂ f₃ : X ⟶ M
⊢ f₁ * f₂ * f₃ = f₁ * (f₂ * f₃)

Tactic:
change lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Goal state after:
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₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (X ◁ toUnit Y ≫ (ρ_ X).hom) ≫ (ρ_ X).inv = fst X Y ≫ (ρ_ X).inv

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (X ◁ toUnit Y ≫ (ρ_ X).hom) ≫ (ρ_ X).inv = fst X Y ≫ (ρ_ X).inv
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (toUnit X ▷ Y ≫ (λ_ Y).hom) ≫ (λ_ Y).inv = snd X Y ≫ (λ_ Y).inv

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
⊢ (toUnit X ▷ Y ≫ (λ_ Y).hom) ≫ (λ_ Y).inv = snd X Y ≫ (λ_ Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

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

Tactic:
by
  rw [← cancel_mono (λ_ Y).inv]; aesop

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
⊢ μ = μ

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ μ = μ
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
⊢ lift (fst M M) (snd M M) ≫ μ = μ

Tactic:
;

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M : C
inst✝ : MonObj M
⊢ lift (fst M M) (snd M M) ≫ μ = μ
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✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ { toBraidedCategory := toBraidedCategory✝¹, symmetry := symmetry✝¹ } =
    { toBraidedCategory := toBraidedCategory✝, symmetry := symmetry✝ }

Tactic:
;

Goal state after:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ { toBraidedCategory := toBraidedCategory✝¹, symmetry := symmetry✝¹ } =
    { toBraidedCategory := toBraidedCategory✝, symmetry := symmetry✝ }
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✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ toBraidedCategory✝¹ = toBraidedCategory✝

Tactic:
;

Goal state after:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ toBraidedCategory✝¹ = toBraidedCategory✝
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
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom ((ofHom (counitAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom (λ_ (op (of R A))).hom.unop) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom ((ofHom (counitAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom (λ_ (op (of R A))).hom.unop) x✝
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
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom (op (of R A) ◁ (ofHom (counitAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom (ρ_ (op (of R A))).hom.unop) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom (op (of R A) ◁ (ofHom (counitAlgHom R A)).op ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom (ρ_ (op (of R A))).hom.unop) x✝
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
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom ((ofHom (comulAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom
        ((α_ (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).unop)
      x✝

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
A : Type u
inst✝¹ : CommRing A
inst✝ : Bialgebra R A
x✝ : ↑(unop (op (of R A)))
⊢ (Hom.hom ((ofHom (comulAlgHom R A)).op ▷ op (of R A) ≫ (ofHom (comulAlgHom R A)).op).unop) x✝ =
    (Hom.hom
        ((α_ (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).unop)
      x✝
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
x✝ : ↑(unop (op (CommAlgCat.of R A)))
⊢ (CommAlgCat.Hom.hom ((β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))).hom ≫ μ).unop) x✝ =
    (CommAlgCat.Hom.hom μ.unop) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
x✝ : ↑(unop (op (CommAlgCat.of R A)))
⊢ (CommAlgCat.Hom.hom ((β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))).hom ≫ μ).unop) x✝ =
    (CommAlgCat.Hom.hom μ.unop) 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)
x✝ : C
⊢ (f * (g + h)).ofConv x✝ = (f * g + f * h).ofConv x✝

Tactic:
;

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)
x✝ : C
⊢ ((f + g) * h).ofConv x✝ = (f * h + g * h).ofConv x✝

Tactic:
;

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)
x✝ : C
⊢ (0 * f).ofConv x✝ = (ofConv 0) x✝

Tactic:
;

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)
x✝ : C
⊢ (f * 0).ofConv x✝ = (ofConv 0) x✝

Tactic:
;

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.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
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower S A A
s : S
f g : WithConv (C →ₗ[R] A)
c : C
⊢ ((s • f) • g).ofConv c = (s • f • g).ofConv c

Tactic:
;

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
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower S A A
s : S
f g : WithConv (C →ₗ[R] A)
c : C
⊢ ((s • f) • g).ofConv c = (s • f • g).ofConv c
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 x✝ : C
⊢ (prodComparisonNatTrans (F ⋙ G) A).app x✝ =
    (Functor.whiskerRight (prodComparisonNatTrans F A) G ≫ F.whiskerLeft (prodComparisonNatTrans G (F.obj A))).app x✝

Tactic:
;

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.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
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass R S A
inst✝ : SMulCommClass S A A
s : S
f g : WithConv (C →ₗ[R] A)
c : C
⊢ (s • f • g).ofConv c = (f • s • g).ofConv c

Tactic:
;

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
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass R S A
inst✝ : SMulCommClass S A A
s : S
f g : WithConv (C →ₗ[R] A)
c : C
⊢ (s • f • g).ofConv c = (f • s • g).ofConv c
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: 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✝

Tactic:
;

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)).ofConv 1 =
    (toConv (toSpanSingleton R A (x * y))).ofConv 1

Tactic:
;

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
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✝

Tactic:
;

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✝
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 A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
x✝ : C
⊢ IsIso (prodComparisonNatTrans F x✝)

Tactic:
;

Goal state after:
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✝
A B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : ∀ (A B : C), IsIso (prodComparison F A B)
x✝ : C
⊢ IsIso (prodComparisonNatTrans F x✝)
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inl ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom f

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inl ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom f
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inr ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom g

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inr ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom g