awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
f g : Z ⟶ X
a : { a : (Z ⟶ M) × (Z ⟶ X) // a.2 = f ∧ a.1 • a.2 = g }
⊢ (↑a : (Z ⟶ M) × (Z ⟶ X)).1 • f = g

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
f g : Z ⟶ X
a : { b : Z ⟶ M // b • f = g }
⊢ ((↑a : Z ⟶ M), f).2 = f ∧ ((↑a : Z ⟶ M), f).1 • ((↑a : Z ⟶ M), f).2 = g

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
H :
  ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)
h :
  ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X),
    Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f
Z : C
f g : Z ⟶ X
⊢ (∃! a : (Z ⟶ M) × (Z ⟶ X), a.2 = f ∧ a.1 • a.2 = g) ↔ ∃! m : Z ⟶ M, m • f = g

Tactic:
exact Equiv.existsUnique_subtype_congr ⟨fun a ↦ ⟨a.val.fst, by grind⟩,
    fun a ↦ ⟨⟨a.val, f⟩, by grind⟩, by cat_disch, by cat_disch⟩

Premises used: Equiv.existsUnique_subtype_congr, Equiv.mk, Subtype.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
D : Type u_1
inst : Category.{v_1, u_1} D
inst_1 : SemiCartesianMonoidalCategory.{v_1, u_1} D
M : D
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} D (𝒞 := inst)) (tensorUnit.{v_1, u_1} D (𝒞 := inst)) ⟶ M)
    (μ ≫ η) ((η ⊗ₘ η) ≫ μ)

Tactic:
simp [toUnit_unique (ρ_ (𝟙_ D)).hom (λ_ (𝟙_ D)).hom]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
D : Type u_1
inst : Category.{v_1, u_1} D
inst_1 : SemiCartesianMonoidalCategory.{v_1, u_1} D
M : D
inst_2 : MonObj M
⊢ Mono.{v_1, u_1} (C := D) (X := tensorUnit.{v_1, u_1} D (𝒞 := inst)) (Y := M) η

Tactic:
Limits.IsTerminal.mono_from isTerminalTensorUnit _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, CategoryTheory.Limits.IsTerminal.mono_from
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
D : Type u_1
inst : Category.{v_1, u_1} D
inst_1 : SemiCartesianMonoidalCategory.{v_1, u_1} D
M N : Mon.{v_1, u_1} D
⊢ Eq (α := M.X ⟶ N.X) (Hom.hom 0) (CategoryStruct.comp (Y := tensorUnit.{v_1, u_1} D (𝒞 := inst)) (toUnit M.X) η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f g h : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (μ ▷ B ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)

Tactic:
have := lift (lift f g) h ≫= mul_assoc B
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f g h : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (μ ▷ B ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B) (lift (lift f g) h)
      (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
        CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) B B) B)
          (lift (lift f g) h) (Iso.hom (α_ B B B) ≫ B ◁ μ ≫ μ)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
        CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorObj.{v, u_1} (𝒞 := inst) B B))
          (lift f (lift g h)) (B ◁ μ ≫ μ)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
        CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
          (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
        (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f g) μ) h) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B)
      (lift f (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift g h) μ)) μ

Tactic:
rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc, CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc, CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
g : A ⟶ B
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) B) (lift f g)
      (η ▷ B ≫ μ) =
    lift f g ≫ Iso.hom (λ_ B)

Tactic:
have := lift f g ≫= one_mul B
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
g : A ⟶ B
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) B) (lift f g)
      (η ▷ B ≫ μ) =
    lift f g ≫ Iso.hom (λ_ B)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = lift f g ≫ Iso.hom (λ_ B)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift (f ≫ η) g) μ = g

Tactic:
rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc, CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f : A ⟶ B
g : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f g)
      (B ◁ η ≫ μ) =
    lift f g ≫ Iso.hom (ρ_ B)

Tactic:
have := lift f g ≫= mul_one B
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
A B : C
inst_2 : MonObj B
f : A ⟶ B
g : A ⟶ tensorUnit.{v, u_1} C (𝒞 := inst)
this :
  CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B (tensorUnit.{v, u_1} C (𝒞 := inst))) (lift f g)
      (B ◁ η ≫ μ) =
    lift f g ≫ Iso.hom (ρ_ B)
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = lift f g ≫ Iso.hom (ρ_ B)),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f),
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f
⊢ CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) B B) (lift f (g ≫ η)) μ = f

Tactic:
rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom, CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
inst_8 : IsCommMonObj.{v, u_1} M
⊢ Eq.{v + 1} (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ M)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) η μ) η

Tactic:
simp [toUnit_unique (ρ_ (𝟙_ C)).hom (λ_ (𝟙_ C)).hom]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonoidalCategoryStruct.tensorUnit, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M : Mon.{v, u_1} C
f : M ⟶ (𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory)
w :
  f.hom =
    Hom.hom
      ((fun (M : Mon.{v, u_1} C) ↦
          ({ hom := toUnit M.X, isMonHom_hom := ⋯ } : M.Hom ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory))))
        M)
⊢ f =
    (fun (M : Mon.{v, u_1} C) ↦
        ({ hom := toUnit M.X, isMonHom_hom := ⋯ } : M.Hom ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory))))
      M

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M : Mon.{v, u_1} C
f : M ⟶ (𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory)
⊢ f.hom =
    Hom.hom
      ((fun (M : Mon.{v, u_1} C) ↦
          ({ hom := toUnit M.X, isMonHom_hom := ⋯ } : M.Hom ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory))))
        M)

Tactic:
toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M : Mon.{v, u_1} C
f : M ⟶ (𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory)
⊢ f.hom =
    Hom.hom
      ((fun (M : Mon.{v, u_1} C) ↦
          ({ hom := toUnit M.X, isMonHom_hom := ⋯ } : M.Hom ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory))))
        M)

Tactic:
exact toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
w :
  Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ M.X) (Hom.hom { hom := fst M.X N.X, isMonHom_hom := ⋯ })
    (Hom.hom
      (M ◁
          IsTerminal.from
            (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) N ≫
        Iso.hom (ρ_ M)))
⊢ Eq (α := tensorObj (𝒞 := instCategory) M N ⟶ M) { hom := fst M.X N.X, isMonHom_hom := ⋯ }
    (M ◁
        IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
          N ≫
      Iso.hom (ρ_ M))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
w :
  Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) M.X N.X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M.X (tensorUnit.{v, u_1} C (𝒞 := inst)))
    (M.X ◁ IsTerminal.from isTerminalTensorUnit N.X)
    (M.X ◁
      Hom.hom
        (IsTerminal.from
          (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) N))
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ M.X) (Hom.hom { hom := fst M.X N.X, isMonHom_hom := ⋯ })
    (Hom.hom
      (M ◁
          IsTerminal.from
            (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) N ≫
        Iso.hom (ρ_ M)))

Tactic:
simp [fst_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) M.X N.X ⟶ tensorObj.{v, u_1} (𝒞 := inst) M.X (tensorUnit.{v, u_1} C (𝒞 := inst)))
    (M.X ◁ IsTerminal.from isTerminalTensorUnit N.X)
    (M.X ◁
      Hom.hom
        (IsTerminal.from
          (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) N))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
w :
  Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ N.X) (Hom.hom { hom := snd M.X N.X, isMonHom_hom := ⋯ })
    (Hom.hom
      (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
            M ▷
          N ≫
        Iso.hom (λ_ N)))
⊢ Eq (α := tensorObj (𝒞 := instCategory) M N ⟶ N) { hom := snd M.X N.X, isMonHom_hom := ⋯ }
    (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
          M ▷
        N ≫
      Iso.hom (λ_ N))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
w :
  Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) M.X N.X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) N.X)
    (IsTerminal.from isTerminalTensorUnit M.X ▷ N.X)
    (Hom.hom
        (IsTerminal.from
          (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) M) ▷
      N.X)
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ N.X) (Hom.hom { hom := snd M.X N.X, isMonHom_hom := ⋯ })
    (Hom.hom
      (IsTerminal.from (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯)
            M ▷
          N ≫
        Iso.hom (λ_ N)))

Tactic:
simp [snd_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
inst_7 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u_1} (𝒞 := inst) M.X N.X ⟶ tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) N.X)
    (IsTerminal.from isTerminalTensorUnit M.X ▷ N.X)
    (Hom.hom
        (IsTerminal.from
          (IsTerminal.ofUniqueHom (fun (M : Mon.{v, u_1} C) ↦ { hom := toUnit M.X, isMonHom_hom := ⋯ }) ⋯) M) ▷
      N.X)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N₁ N₂ : Mon.{v, u_1} C
f : M ⟶ N₁
g : M ⟶ N₂
⊢ Eq (α := M.X ⟶ (tensorObj (𝒞 := instCategory) N₁ N₂).X) (Hom.hom (lift f g)) (lift f.hom g.hom)

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ M.X) (Hom.hom (fst M N)) (fst M.X N.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M N : Mon.{v, u_1} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) M N).X ⟶ N.X) (Hom.hom (snd M N)) (snd M.X N.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} M.X
⊢ Eq.{v + 1} (α := X.{v, u_1} ((𝟙_ (Mon.{v, u_1} C)) (𝒞 := instCategory)) ⟶ M.X) (Hom.hom η) η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : BraidedCategory.{v, u_1} C
M : Mon.{v, u_1} C
inst_3 : IsCommMonObj.{v, u_1} M.X
⊢ Eq.{v + 1} (α := (tensorObj (𝒞 := instCategory) M M).X ⟶ M.X) (Hom.hom μ) μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
F : Functor.{v, w, u_1, w + 1} Cᵒᵖ MonCat
α :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
⊢ HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) : Type w)) (β :=
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
              (Y := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X)))
              (F.map (Quiver.Hom.op (fst (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) :
            (a : (↑(F.obj (op (𝟙_ C))) : Type w)) → (↑(F.obj (op (𝟙_ C ⊗ X))) : Type w))
          1 :
        (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) : Type w))
      (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X ⟶ X)
                (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
            (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ X))))
          (snd (tensorUnit.{v, u_1} C (𝒞 := inst)) X) :
        ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
          (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X)))) =
    ((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
          Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X ⟶ X)
            (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
              (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
        (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ X))))
      (Iso.hom (λ_ X))

Tactic:
simp [leftUnitor_hom, -op_tensorObj, -op_whiskerRight, -op_tensorUnit]

Premises used: CategoryTheory.op_whiskerRight, CategoryTheory.op_tensorUnit, CategoryTheory.op_tensorObj, CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom