awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
inst_5 : BraidedCategory.{v, u} C
inst_6 : IsCommMonObj.{v, u} G
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) (μ ≫ @GrpObj.inv _ _ inst_1 _ _)
    ((@GrpObj.inv _ _ inst_1 _ _ ⊗ₘ @GrpObj.inv _ _ inst_1 _ _) ≫ μ)

Tactic:
simp [GrpObj.mul_inv_rev]

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
⊢ Eq.{v + 1} (α := G.toMon ⟶ H.toMon) (InducedCategory.Hom.hom 1) 1

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f g : G ⟶ H
⊢ (f * g).hom = f.hom * g.hom

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
⊢ (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℕ
hn : (f ^ n).hom = f.hom ^ n
⊢ (f ^ (n + 1)).hom = f.hom ^ (n + 1)

Tactic:
simp [pow_succ, hn]

Premises used: pow_succ
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℕ
zero : (HPow.hPow (β := ℕ) f 0).hom = HPow.hPow (β := ℕ) f.hom 0
succ : ∀ (n : ℕ) (hn : (f ^ n).hom = f.hom ^ n), (f ^ (n + 1)).hom = f.hom ^ (n + 1)
⊢ (f ^ n).hom = f.hom ^ n

Tactic:
induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, hn]

Premises used: pow_succ
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
⊢ f⁻¹.hom.hom = f.hom.hom⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f g : G ⟶ H
⊢ (f / g).hom.hom = f.hom.hom / g.hom.hom

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, DivInvMonoid.div', rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
n : ℤ
ofNat : ∀ (a : ℕ), (f ^ Int.ofNat a).hom.hom = f.hom.hom ^ Int.ofNat a
negSucc : ∀ (a : ℕ), (f ^ Int.negSucc a).hom.hom = f.hom.hom ^ Int.negSucc a
⊢ (f ^ n).hom.hom = f.hom.hom ^ n

Tactic:
cases n
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
a : ℕ
⊢ (f ^ Int.ofNat a).hom.hom = f.hom.hom ^ Int.ofNat a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
G H : Grp.{v, u} C
inst_3 : IsCommMonObj.{v, u} H.X
f : G ⟶ H
a : ℕ
⊢ (f ^ Int.negSucc a).hom.hom = f.hom.hom ^ Int.negSucc a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
inst_4 : IsCommMonObj.{v, u} G
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) (conj G) (snd G G)

Tactic:
simp [conj]

Premises used: CategoryTheory.GrpObj.conj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
rw :
  (∀ (X : C), IsMulCommutative.{v} (X ⟶ G)) ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
⊢ IsCommMonObj.{v, u} G ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η

Tactic:
rw [isCommMonObj_iff_isMulCommutative]

Premises used: CategoryTheory.isCommMonObj_iff_isMulCommutative
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
⊢ (∀ (X : C), IsMulCommutative.{v} (X ⟶ G)) ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η

Tactic:
⟨fun h ↦ ?_, fun heq X ↦ ⟨⟨fun f g ↦ ?_⟩⟩⟩

Premises used: Iff.intro, IsMulCommutative.mk, Std.Commutative.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
refine_1 :
  ∀ (h : ∀ (X : C), IsMulCommutative.{v} (X ⟶ G)),
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
refine_2 :
  ∀
    (heq :
      GrpObj.commutator G =
        CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η)
    (X : C) (f g : X ⟶ G), f * g = g * f
⊢ (∀ (X : C), IsMulCommutative.{v} (X ⟶ G)) ↔
    GrpObj.commutator G =
      CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η

Tactic:
refine ⟨fun h ↦ ?_, fun heq X ↦ ⟨⟨fun f g ↦ ?_⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
h : ∀ (X : C), IsMulCommutative.{v} (X ⟶ G)
⊢ GrpObj.commutator G =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η

Tactic:
simp [GrpObj.commutator, one_eq_one]

Premises used: CategoryTheory.GrpObj.commutator, CategoryTheory.MonObj.one_eq_one
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
inst_3 : BraidedCategory.{v, u} C
heq :
  GrpObj.commutator G =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit (tensorObj.{v, u} (𝒞 := inst) G G)) η
X : C
f g : X ⟶ G
⊢ f * g = g * f

Tactic:
simpa [one_eq_one, mul_inv_eq_iff_eq_mul] using congr(lift f g ≫ $heq)

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.MonObj.one_eq_one, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
J : Type w
inst_2 : Category.{u_2, w} J
inst_3 : HasLimitsOfShape.{u_2, w, v, u_1} J C
⊢ PreservesLimitsOfShape (C := Mon.{v, u_1} C) J shrinkYonedaMon.{max w v, v, u_1}

Tactic:
have : PreservesLimitsOfShape J (shrinkYonedaMon ⋙ (whiskeringRight _ _ _).obj (forget MonCat)) :=
    (inferInstance : PreservesLimitsOfShape J (Mon.forget C ⋙ shrinkYoneda.{max w v}))
  preservesLimitsOfShape_of_reflects_of_preserves _ ((whiskeringRight _ _ _).obj (forget MonCat))

Premises used: Opposite, inferInstance, MonCat, CategoryTheory.Functor.whiskeringRight, CategoryTheory.shrinkYonedaMon, CategoryTheory.forget, CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
J : Type w
inst_2 : Category.{u_2, w} J
inst_3 : HasLimitsOfShape.{u_2, w, v, u_1} J C
⊢ HasLimitsOfShape J (Grp.{v, u_1} C)

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Grp.forget C)

Premises used: CategoryTheory.Grp.forget, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
Goal:
C : Type u
inst : SemilatticeInf C
inst_1 : OrderTop C
X Y : C
⊢ MonoidalCategoryStruct.tensorObj (𝒞 := Preorder.smallCategory C) X Y = X ⊓ Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
Goal:
C : Type u
inst : SemilatticeInf C
inst_1 : OrderTop C
⊢ (𝟙_ C) (𝒞 := Preorder.smallCategory C) = ⊤

Tactic:
rfl

Premises used: rfl
-- 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
Z : C
m n : Z ⟶ M
x : Z ⟶ X
⊢ (m * n) • x = m • n • x

Tactic:
simp [mul_def, smul_def, ← lift_whiskerRight]

Premises used: CategoryTheory.Hom.smul_def, CategoryTheory.Hom.mul_def, CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight
-- 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
Z : C
x : Z ⟶ X
⊢ HSMul.hSMul (α := Z ⟶ M) 1 x = x

Tactic:
simp [one_def, smul_def, ← lift_whiskerRight]

Premises used: CategoryTheory.Hom.smul_def, CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight, CategoryTheory.Hom.one_def
-- 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
Z Z' : C
g : Z' ⟶ Z
m : Z ⟶ M
x : Z ⟶ X
rw :
  g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) =
    g ≫ m • g ≫ x
rw₁ :
  Eq (α := Z' ⟶ X)
    (g ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x))
      (@smul _ _ _ _ _ _ _ inst_2 _ _))
rw₂ rw₃ :
  Eq (α := Z' ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x))
      (@smul _ _ _ _ _ _ _ inst_2 _ _))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift (g ≫ m) (g ≫ x))
      (@smul _ _ _ _ _ _ _ inst_2 _ _))
⊢ g ≫ (m • x) = g ≫ m • g ≫ x

Tactic:
rw [Hom.smul_def, Hom.smul_def, comp_lift_assoc]

Premises used: CategoryTheory.Hom.smul_def, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc
-- 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
Y : C
inst_4 : ModObj M Y
f : X ⟶ Y
inst_5 : IsModHom M f
Z : C
m : Z ⟶ M
x : Z ⟶ X
⊢ (m • x) ≫ f = m • x ≫ f

Tactic:
simp [Hom.smul_def, Category.assoc, IsModHom.smul_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Hom.smul_def, CategoryTheory.IsModHom.smul_hom
-- 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
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) M X ⟶ X) (leftSMul M X ≫ fst X X) (@smul _ _ _ _ _ _ _ inst_2 _ _)

Tactic:
simp [leftSMul]

Premises used: CategoryTheory.ModObj.leftSMul
-- 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
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) M X ⟶ X) (leftSMul M X ≫ snd X X) (snd M X)

Tactic:
simp [leftSMul]

Premises used: CategoryTheory.ModObj.leftSMul
-- 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
Z : C
x : Z ⟶ X
m : Z ⟶ M
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (fst X X) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (fst X X)
h_snd :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (snd X X) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (snd X X)
⊢ Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift (m • x) x)

Tactic:
ext
-- 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
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (fst X X) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (fst X X)

Tactic:
simp [Hom.smul_def]

Premises used: CategoryTheory.Hom.smul_def
-- 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
Z : C
x : Z ⟶ X
m : Z ⟶ M
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (snd X X) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X) (lift (m • x) x) (snd X X)

Tactic:
simp [Hom.smul_def]

Premises used: CategoryTheory.Hom.smul_def
-- 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
Z : C
x y : Z ⟶ X
m : Z ⟶ M
⊢ Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift y x) ↔ m • x = y

Tactic:
simp [Hom.smul_def, leftSMul, CartesianMonoidalCategory.hom_ext_iff]

Premises used: CategoryTheory.Hom.smul_def, CategoryTheory.ModObj.leftSMul, CategoryTheory.CartesianMonoidalCategory.hom_ext_iff
-- 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
⊢ ∀ (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)

Tactic:
have H (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) :
      lift m x ≫ leftSMul M X = lift (m • x) x := by
    ext <;> simp [Hom.smul_def]
-- 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)
Z : C
f g : Z ⟶ X
m : Z ⟶ M
x : Z ⟶ X
simp :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) = f ∧ x = g ↔
    x = g ∧ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) = f
⊢ Eq (α := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) (lift m x ≫ leftSMul M X) (lift f g) ↔ x = g ∧ m • x = f

Tactic:
simp [← lift_leftSMul_eq_lift_iff, CartesianMonoidalCategory.hom_ext_iff]

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext_iff, CategoryTheory.ModObj.lift_leftSMul_eq_lift_iff
-- 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)
Z : C
f g : Z ⟶ X
m : Z ⟶ M
x : Z ⟶ X
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) = f ∧ x = g ↔
    x = g ∧ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) M X) (lift m x) (@smul _ _ _ _ _ _ _ inst_2 _ _) = f

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)
⊢ ∀ (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

Tactic:
have h (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X) :
      lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f := by
    simp [← lift_leftSMul_eq_lift_iff, CartesianMonoidalCategory.hom_ext_iff]
    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
rw :
  (∀ (T : C),
      Function.Bijective (β := T ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : T ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
        x ≫ leftSMul M X) ↔
    ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
⊢ IsIso.{v, u} (X := tensorObj.{v, u} (𝒞 := inst) M X) (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

Tactic:
rw [isIso_iff_yoneda_map_bijective]

Premises used: CategoryTheory.isIso_iff_yoneda_map_bijective
-- 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
a :
  ∀ (Z : C),
    (Function.Bijective (β := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
        x ≫ leftSMul M X) ↔
      ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
⊢ (∀ (T : C),
      Function.Bijective (β := T ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : T ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
        x ≫ leftSMul M X) ↔
    ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

Tactic:
congr! with Z
-- 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
a :
  (∀ (b : Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X),
      ∃! a : (Z ⟶ M) × (Z ⟶ X),
        ((fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦ x ≫ leftSMul M X) ∘
              (⇑liftEquiv : (a : (Z ⟶ M) × (Z ⟶ X)) → Z ⟶ M ⊗ X))
            a =
          b) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
⊢ (Function.Bijective (β := Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X) fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦
      x ≫ leftSMul M X) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

Tactic:
rw [← Function.Bijective.of_comp_iff _ liftEquiv.bijective, Function.bijective_iff_existsUnique]

Premises used: Equiv.bijective, CategoryTheory.CartesianMonoidalCategory.liftEquiv, Function.Bijective.of_comp_iff, Function.bijective_iff_existsUnique
-- 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
a :
  (∀ (a b : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
⊢ (∀ (b : Z ⟶ tensorObj.{v, u} (𝒞 := inst) X X),
      ∃! a : (Z ⟶ M) × (Z ⟶ X),
        ((fun (x : Z ⟶ tensorObj.{v, u} (𝒞 := inst) M X) ↦ x ≫ leftSMul M X) ∘
              (⇑liftEquiv : (a : (Z ⟶ M) × (Z ⟶ X)) → Z ⟶ M ⊗ X))
            a =
          b) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

Tactic:
simp only [liftEquiv.surjective.forall, liftEquiv_apply, Prod.forall, Function.comp_apply, h]

Premises used: Function.Surjective.forall, CategoryTheory.CartesianMonoidalCategory.liftEquiv, Prod.forall, Function.comp_apply, Equiv.surjective, CategoryTheory.CartesianMonoidalCategory.liftEquiv_apply
-- 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
a :
  (∀ (b a : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y
⊢ (∀ (a b : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

Tactic:
rw [forall_comm]

Premises used: forall_comm
-- 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
a : ∀ (f g : Z ⟶ X), (∃! a : (Z ⟶ M) × (Z ⟶ X), a.2 = f ∧ a.1 • a.2 = g) ↔ ∃! m : Z ⟶ M, m • f = g
⊢ (∀ (b a : Z ⟶ X), ∃! a_1 : (Z ⟶ M) × (Z ⟶ X), a_1.2 = b ∧ a_1.1 • a_1.2 = a) ↔
    ∀ (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

Tactic:
congr! 2 with f g