awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
⊢ Eq (α := unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        (lift
          ((MonCat.Hom.hom (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
              (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
                (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
            (fst M.X M.X))
          ((MonCat.Hom.hom (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
              (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
                (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
            (snd M.X M.X)))
        (fst N.X N.X) :
      unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X) ⊗ₘ
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X))
        (fst N.X N.X) :
      unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)

Tactic:
simp only [lift_fst, tensorHom_fst, lift_snd, tensorHom_snd,
          ← yonedaMon_naturality, Category.comp_id]

Premises used: CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.yonedaMon_naturality, CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.CartesianMonoidalCategory.lift_fst
-- 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
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
⊢ Eq (α := unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        (lift
          ((MonCat.Hom.hom (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
              (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
                (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
            (fst M.X M.X))
          ((MonCat.Hom.hom (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
              (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
                (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
            (snd M.X M.X)))
        (snd N.X N.X) :
      unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X) ⊗ₘ
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X))
        (snd N.X N.X) :
      unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)

Tactic:
simp only [lift_fst, tensorHom_fst, lift_snd, tensorHom_snd,
          ← yonedaMon_naturality, Category.comp_id]

Premises used: CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.yonedaMon_naturality, CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.CartesianMonoidalCategory.lift_fst
-- 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
M N : Mon.{v, u_1} C
α : Functor.obj yonedaMon M ⟶ Functor.obj yonedaMon N
w :
  ∀ (Y : Cᵒᵖ) (f : (↑((Functor.obj yonedaMon M).obj Y) : Type v)),
    Eq (α := (↑((Functor.obj yonedaMon N).obj Y) : Type v))
      (((MonCat.Hom.hom
                (NatTrans.app
                  (Functor.map yonedaMon
                    {
                      hom :=
                        (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                              MonCat.carrier) (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
                            (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) →
                              (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
                          (𝟙 M.X),
                      isMonHom_hom := ⋯ })
                  Y) :
              (↑((Functor.obj yonedaMon M).obj Y) : Type v) →* (↑((Functor.obj yonedaMon N).obj Y) : Type v)) :
            (a : (↑((yonedaMon.obj M).obj Y) : Type v)) → (↑((yonedaMon.obj N).obj Y) : Type v))
          f :
        (↑((Functor.obj yonedaMon N).obj Y) : Type v))
      ((MonCat.Hom.hom (α.app Y) : (a : (↑((yonedaMon.obj M).obj Y) : Type v)) → (↑((yonedaMon.obj N).obj Y) : Type v))
          f :
        (↑((Functor.obj yonedaMon N).obj Y) : Type v))
⊢ Functor.map yonedaMon
      {
        hom :=
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) → (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
            (𝟙 M.X),
        isMonHom_hom := ⋯ } =
    α

Tactic:
ext Y f
-- 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_1 : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Functor.obj yonedaMon M ⟶ Functor.obj yonedaMon N
Y : Cᵒᵖ
f : (↑((Functor.obj yonedaMon M).obj Y) : Type v)
⊢ Eq (α := (↑((Functor.obj yonedaMon N).obj Y) : Type v))
    (((MonCat.Hom.hom
              (NatTrans.app
                (Functor.map yonedaMon
                  {
                    hom :=
                      (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                            MonCat.carrier) (X := (Functor.obj yonedaMon M).obj (op M.X)) (α.app (op M.X)) :
                          (a : (↑((yonedaMon.obj M).obj (op M.X)) : Type v)) →
                            (↑((yonedaMon.obj N).obj (op M.X)) : Type v))
                        (𝟙 M.X),
                    isMonHom_hom := ⋯ })
                Y) :
            (↑((Functor.obj yonedaMon M).obj Y) : Type v) →* (↑((Functor.obj yonedaMon N).obj Y) : Type v)) :
          (a : (↑((yonedaMon.obj M).obj Y) : Type v)) → (↑((yonedaMon.obj N).obj Y) : Type v))
        f :
      (↑((Functor.obj yonedaMon N).obj Y) : Type v))
    ((MonCat.Hom.hom (α.app Y) : (a : (↑((yonedaMon.obj M).obj Y) : Type v)) → (↑((yonedaMon.obj N).obj Y) : Type v))
        f :
      (↑((Functor.obj yonedaMon N).obj Y) : Type v))

Tactic:
simp [← dsimp% yonedaMon_naturality]

Premises used: CategoryTheory.yonedaMon_naturality
-- 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
⊢ Functor.Full (C := Mon.{v, u_1} C) yonedaMon

Tactic:
yonedaMonFullyFaithful.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.yonedaMonFullyFaithful
-- 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
⊢ Functor.Faithful (C := Mon.{v, u_1} C) yonedaMon

Tactic:
yonedaMonFullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.yonedaMonFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
h :
  ∀ (F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat),
    Functor.essImage (C := Mon.{v, u_1} C) yonedaMon F ↔
      (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
            MonCat.carrier)).IsRepresentable
⊢ Eq (α := ObjectProperty (Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat)) (Functor.essImage (C := Mon.{v, u_1} C) yonedaMon)
    fun (F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) ↦
    (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).IsRepresentable

Tactic:
ext F
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
h :
  Functor.essImage (C := Mon.{v, u_1} C) yonedaMon F →
    (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).IsRepresentable
h₁ :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).IsRepresentable →
    Functor.essImage (C := Mon.{v, u_1} C) yonedaMon F
⊢ Functor.essImage (C := Mon.{v, u_1} C) yonedaMon F ↔
    (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).IsRepresentable

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
M : Mon.{v, u_1} C
α : Functor.obj yonedaMon M ≅ F
⊢ (F ⋙
      forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
        MonCat.carrier)).IsRepresentable

Tactic:
⟨M.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩

Premises used: CategoryTheory.Functor.representableByEquiv, CategoryTheory.Functor.IsRepresentable.mk, Nonempty.intro, CategoryTheory.Mon.X, Exists.intro, CategoryTheory.forget, Equiv.symm, CategoryTheory.Functor.isoWhiskerRight, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
M : Mon.{v, u_1} C
α : Functor.obj yonedaMon M ≅ F
⊢ (F ⋙
      forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
        MonCat.carrier)).IsRepresentable

Tactic:
exact ⟨M.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
X : C
e :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
this : MonObj X := ofRepresentableBy X F e
⊢ Functor.essImage (C := Mon.{v, u_1} C) yonedaMon F

Tactic:
⟨Mon.mk X, ⟨yonedaMonObjIsoOfRepresentableBy X F e⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.yonedaMonObjIsoOfRepresentableBy, Exists.intro, CategoryTheory.Mon.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
F : Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat
X : C
e :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
this : MonObj X := ofRepresentableBy X F e
⊢ Functor.essImage (C := Mon.{v, u_1} C) yonedaMon F

Tactic:
exact ⟨Mon.mk X, ⟨yonedaMonObjIsoOfRepresentableBy X F e⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M N X : C
inst_2 : MonObj M
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α := X ⟶ N) (1 ≫ f) 1

Tactic:
simp [Hom.one_def]

Premises used: CategoryTheory.Hom.one_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M N X : C
inst_2 : MonObj M
inst_3 : MonObj N
f₁ f₂ : X ⟶ M
g : M ⟶ N
inst_4 : IsMonHom g
⊢ (f₁ * f₂) ≫ g = f₁ ≫ g * f₂ ≫ g

Tactic:
simp [Hom.mul_def]

Premises used: CategoryTheory.Hom.mul_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M N X : C
inst_2 : MonObj M
inst_3 : MonObj N
f : X ⟶ M
n : ℕ
g : M ⟶ N
inst_4 : IsMonHom g
zero : HPow.hPow (β := ℕ) f 0 ≫ g = HPow.hPow (β := ℕ) (f ≫ g) 0
succ : ∀ (n : ℕ), (f ^ n) ≫ g = (f ≫ g) ^ n → (f ^ (n + 1)) ≫ g = (f ≫ g) ^ (n + 1)
⊢ (f ^ n) ≫ g = (f ≫ g) ^ n

Tactic:
induction n
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M N X : C
inst_2 : MonObj M
inst_3 : MonObj N
f : X ⟶ M
g : M ⟶ N
inst_4 : IsMonHom g
⊢ HPow.hPow (β := ℕ) f 0 ≫ g = HPow.hPow (β := ℕ) (f ≫ g) 0

Tactic:
simp [pow_succ, MonObj.mul_comp, *]

Premises used: pow_succ, CategoryTheory.MonObj.mul_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M N X : C
inst_2 : MonObj M
inst_3 : MonObj N
f : X ⟶ M
g : M ⟶ N
inst_4 : IsMonHom g
n : ℕ
h : (f ^ n) ≫ g = (f ≫ g) ^ n
⊢ (f ^ (n + 1)) ≫ g = (f ≫ g) ^ (n + 1)

Tactic:
simp [pow_succ, MonObj.mul_comp, *]

Premises used: pow_succ, CategoryTheory.MonObj.mul_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M X Y : C
inst_2 : MonObj M
f : X ⟶ Y
⊢ Eq (α := X ⟶ M) (f ≫ 1) 1

Tactic:
((yonedaMon.obj <| .mk M).map f.op).hom.map_one

Premises used: Quiver.Hom.op, Quiver.Hom.unop, MonCat.Hom.hom, CategoryTheory.Functor.map, MonoidHom.map_one, CategoryTheory.yonedaMon, CategoryTheory.Functor.obj, CategoryTheory.Mon.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M X Y : C
inst_2 : MonObj M
f : X ⟶ Y
g₁ g₂ : Y ⟶ M
⊢ f ≫ (g₁ * g₂) = f ≫ g₁ * f ≫ g₂

Tactic:
((yonedaMon.obj <| .mk M).map f.op).hom.map_mul _ _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, MonCat.Hom.hom, CategoryTheory.Functor.map, CategoryTheory.yonedaMon, MonoidHom.map_mul, CategoryTheory.Functor.obj, CategoryTheory.Mon.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M X Y : C
inst_2 : MonObj M
f : X ⟶ M
n : ℕ
h : Y ⟶ X
zero : h ≫ HPow.hPow (β := ℕ) f 0 = HPow.hPow (β := ℕ) (h ≫ f) 0
succ : ∀ (n : ℕ), h ≫ f ^ n = (h ≫ f) ^ n → h ≫ f ^ (n + 1) = (h ≫ f) ^ (n + 1)
⊢ h ≫ f ^ n = (h ≫ f) ^ n

Tactic:
induction n
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M X Y : C
inst_2 : MonObj M
f : X ⟶ M
h : Y ⟶ X
⊢ h ≫ HPow.hPow (β := ℕ) f 0 = HPow.hPow (β := ℕ) (h ≫ f) 0

Tactic:
simp [pow_succ, MonObj.comp_mul, *]

Premises used: pow_succ, CategoryTheory.MonObj.comp_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M X Y : C
inst_2 : MonObj M
f : X ⟶ M
h : Y ⟶ X
n : ℕ
h_1 : h ≫ f ^ n = (h ≫ f) ^ n
⊢ h ≫ f ^ (n + 1) = (h ≫ f) ^ (n + 1)

Tactic:
simp [pow_succ, MonObj.comp_mul, *]

Premises used: pow_succ, CategoryTheory.MonObj.comp_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
rw : Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ M) η (𝟙 (tensorUnit.{v, u_1} C (𝒞 := inst)) ≫ η)
rw₁ rw₂ : Eq.{v + 1} (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ M) η η
⊢ Eq (α := tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ M) η
    (CategoryStruct.comp (Y := tensorUnit.{v, u_1} C (𝒞 := inst)) (toUnit (tensorUnit.{v, u_1} C (𝒞 := inst))) η)

Tactic:
rw [toUnit_unique (toUnit _) (𝟙 _), Category.id_comp]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.CategoryStruct.id, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
rw : μ = 𝟙 (tensorObj.{v, u_1} (𝒞 := inst) M M) ≫ μ
rw₁ rw₂ : Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) μ μ
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) μ
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M M) (lift (fst M M) (snd M M)) μ)

Tactic:
rw [lift_fst_snd, Category.id_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
inst_3 : BraidedCategory.{v, u_1} C
h : IsCommMonObj.{v, u_1} M
X : C
⊢ ∀ (a b : X ⟶ M), a * b = b * a

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
inst_3 : BraidedCategory.{v, u_1} C
h : ∀ (X : C), IsMulCommutative.{v} (X ⟶ M)
⊢ Eq.{v + 1} (α := tensorObj.{v, u_1} (𝒞 := inst) M M ⟶ M) (Iso.hom (β_ M M) ≫ μ) μ

Tactic:
simp [mul_eq_mul, comp_mul, mul_comm]

Premises used: CategoryTheory.MonObj.comp_mul, mul_comm, CategoryTheory.MonObj.mul_eq_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
M : C
inst_2 : MonObj M
inst_3 : BraidedCategory.{v, u_1} C
⊢ IsCommMonObj.{v, u_1} M ↔ ∀ (X : C), IsMulCommutative.{v} (X ⟶ M)

Tactic:
exact ⟨fun h X ↦ ⟨⟨by simp [mul_comm]⟩⟩, fun h ↦ ⟨by simp [mul_eq_mul, comp_mul, mul_comm]⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CartesianMonoidalCategory.{v_1, u_1} C
G H K : C
inst_2 : GrpObj G
inst_3 : GrpObj H
inst_4 : GrpObj K
φ : H ⟶ G
h :
  CategoryStruct.comp (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst))
      (toUnit (tensorObj.{v_1, u_1} (𝒞 := inst) G (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) η =
    G ◁ η ≫ conj G
⊢ ∃ (ψ :
    tensorObj.{v_1, u_1} (𝒞 := inst) G (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ tensorUnit.{v_1, u_1} C (𝒞 := inst)),
    ψ ≫ η = G ◁ η ≫ conj G

Tactic:
use toUnit _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CartesianMonoidalCategory.{v_1, u_1} C
G H K : C
inst_2 : GrpObj G
inst_3 : GrpObj H
inst_4 : GrpObj K
φ : H ⟶ G
⊢ CategoryStruct.comp (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst))
      (toUnit (tensorObj.{v_1, u_1} (𝒞 := inst) G (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) η =
    G ◁ η ≫ conj G

Tactic:
simp [conj, comp_mul, comp_inv, toUnit_unique _ (toUnit _), ← Hom.one_def]

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.MonObj.comp_mul, CategoryTheory.Hom.one_def, CategoryTheory.GrpObj.comp_inv, CategoryTheory.GrpObj.conj, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CartesianMonoidalCategory.{v_1, u_1} C
G H : C
inst_2 : GrpObj G
inst_3 : GrpObj H
φ : H ⟶ G
inst_4 : IsMonHom φ
inst_5 : Mono φ
⊢ Normal φ ↔ ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
⟨fun h ↦ h.exists_comp_eq_conj, fun h ↦ ⟨‹_›, ‹_›, h⟩⟩

Premises used: CategoryTheory.IsMonHom.Normal.mk, Iff.intro, CategoryTheory.IsMonHom.Normal.exists_comp_eq_conj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CartesianMonoidalCategory.{v_1, u_1} C
G H : C
inst_2 : GrpObj G
inst_3 : GrpObj H
φ : H ⟶ G
inst_4 : IsMonHom φ
inst_5 : Mono φ
rw :
  (∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G) ↔
    ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
⊢ Normal φ ↔ ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))

Tactic:
rw [isNormalHom_iff]

Premises used: CategoryTheory.IsMonHom.isNormalHom_iff
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CartesianMonoidalCategory.{v_1, u_1} C
G H : C
inst_2 : GrpObj G
inst_3 : GrpObj H
φ : H ⟶ G
inst_4 : IsMonHom φ
inst_5 : Mono φ
⊢ (∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G) ↔
    ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : CartesianMonoidalCategory.{v_1, u_1} C
G H : C
inst_2 : GrpObj G
inst_3 : GrpObj H
φ : H ⟶ G
inst_4 : IsMonHom φ
inst_5 : Mono φ
refine_1 :
  (∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G) →
    ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
refine_2 :
  (∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))) →
    ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G
⊢ (∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G) ↔
    ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))

Tactic:
refine ⟨?_, ?_⟩