awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X.{v₁, u₁} ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) η η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, u₁} (V := C)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (X.{v₁, u₁} ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)))
        (X.{v₁, u₁} ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))))
      (X.{v₁, u₁} ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))))
    μ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (tensorObj (𝒞 := instCategory) G H).X) η η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj (𝒞 := instCategory) G H).X (tensorObj (𝒞 := instCategory) G H).X ⟶
      (tensorObj (𝒞 := instCategory) G H).X)
    μ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
f : G ⟶ H
I : Grp.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G I).toMon.X ⟶ (tensorObj (𝒞 := instCategory) H I).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (f ▷ I))) (f.hom.hom ▷ I.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H I : Grp.{v₁, u₁} C
f : H ⟶ I
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ (tensorObj (𝒞 := instCategory) G I).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (G ◁ f))) (G.X ◁ f.hom.hom)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G : Grp.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) G).toMon.X ⟶ G.toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (λ_ G)))) (Iso.hom (λ_ G.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G : Grp.{v₁, u₁} C
⊢ Eq (α := G.toMon.X ⟶ (tensorObj (𝒞 := instCategory) ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) G).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.inv (λ_ G)))) (Iso.inv (λ_ G.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G : Grp.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))).toMon.X ⟶ G.toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (ρ_ G)))) (Iso.hom (ρ_ G.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G : Grp.{v₁, u₁} C
⊢ Eq (α := G.toMon.X ⟶ (tensorObj (𝒞 := instCategory) G ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.inv (ρ_ G)))) (Iso.inv (ρ_ G.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H I : Grp.{v₁, u₁} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) G H) I).toMon.X ⟶
      (tensorObj (𝒞 := instCategory) G (tensorObj (𝒞 := instCategory) H I)).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (α_ G H I)))) (Iso.hom (α_ G.X H.X I.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H I : Grp.{v₁, u₁} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) G (tensorObj (𝒞 := instCategory) H I)).toMon.X ⟶
      (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) G H) I).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.inv (α_ G H I)))) (Iso.inv (α_ G.X H.X I.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ X₁ Y₁ X₂ Y₂ : Grp.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
h :
  Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).toMon.X ⟶ (tensorObj (𝒞 := instCategory) Y₁ Y₂).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (f ⊗ₘ g))) (Hom.hom (InducedCategory.Hom.hom (f ▷ X₂ ≫ Y₁ ◁ g)))
⊢ Eq (α := tensorObj (𝒞 := instCategory) X₁ X₂ ⟶ tensorObj (𝒞 := instCategory) Y₁ Y₂) (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ X₁ Y₁ X₂ Y₂ : Grp.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).toMon.X ⟶ (tensorObj (𝒞 := instCategory) Y₁ Y₂).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (f ⊗ₘ g))) (Hom.hom (InducedCategory.Hom.hom (f ▷ X₂ ≫ Y₁ ◁ g)))

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ x x_1 : Grp.{v₁, u₁} C
h :
  Eq (α :=
    (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)))
            x_1).toMon.X ⟶
      (tensorObj (𝒞 := instCategory) x x_1).toMon.X)
    (Hom.hom
      (InducedCategory.Hom.hom (Iso.hom (α_ x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) x_1) ≫ x ◁ Iso.hom (λ_ x_1))))
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (ρ_ x) ▷ x_1)))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) x_1 ⟶
      tensorObj (𝒞 := instCategory) x x_1)
    (Iso.hom (α_ x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) x_1) ≫ x ◁ Iso.hom (λ_ x_1)) (Iso.hom (ρ_ x) ▷ x_1)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ x x_1 : Grp.{v₁, u₁} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)))
            x_1).toMon.X ⟶
      (tensorObj (𝒞 := instCategory) x x_1).toMon.X)
    (Hom.hom
      (InducedCategory.Hom.hom (Iso.hom (α_ x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) x_1) ≫ x ◁ Iso.hom (λ_ x_1))))
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (ρ_ x) ▷ x_1)))

Tactic:
triangle _ _

Premises used: CategoryTheory.MonoidalCategory.triangle
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ x x_1 : Grp.{v₁, u₁} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)))
            x_1).toMon.X ⟶
      (tensorObj (𝒞 := instCategory) x x_1).toMon.X)
    (Hom.hom
      (InducedCategory.Hom.hom (Iso.hom (α_ x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) x_1) ≫ x ◁ Iso.hom (λ_ x_1))))
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (ρ_ x) ▷ x_1)))

Tactic:
exact triangle _ _

Premises used: CategoryTheory.MonoidalCategory.triangle
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H H₁ H₂ G : Grp.{v₁, u₁} C
f : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)
h :
  f.hom.hom =
    Hom.hom
      (InducedCategory.Hom.hom
        ((fun (G : Grp.{v₁, u₁} C) ↦ (homMk' (toUnit G.toMon) : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) G))
⊢ f = (fun (G : Grp.{v₁, u₁} C) ↦ (homMk' (toUnit G.toMon) : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) G

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H H₁ H₂ G : Grp.{v₁, u₁} C
f : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)
⊢ f.hom.hom =
    Hom.hom
      (InducedCategory.Hom.hom
        ((fun (G : Grp.{v₁, u₁} C) ↦ (homMk' (toUnit G.toMon) : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) G))

Tactic:
toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H H₁ H₂ G : Grp.{v₁, u₁} C
f : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)
⊢ f.hom.hom =
    Hom.hom
      (InducedCategory.Hom.hom
        ((fun (G : Grp.{v₁, u₁} C) ↦ (homMk' (toUnit G.toMon) : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) G))

Tactic:
exact toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H_1 H₁ H₂ G H : Grp.{v₁, u₁} C
h :
  Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ G.toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (homMk' (fst G.toMon H.toMon))))
    (Hom.hom
      (InducedCategory.Hom.hom
        (G ◁ IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) H ≫
          Iso.hom (ρ_ G))))
⊢ Eq (α := tensorObj (𝒞 := instCategory) G H ⟶ G) (homMk' (fst G.toMon H.toMon))
    (G ◁ IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) H ≫
      Iso.hom (ρ_ G))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H_1 H₁ H₂ G H : Grp.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ G.toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (homMk' (fst G.toMon H.toMon))))
    (Hom.hom
      (InducedCategory.Hom.hom
        (G ◁ IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) H ≫
          Iso.hom (ρ_ G))))

Tactic:
apply fst_def

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H_1 H₁ H₂ G H : Grp.{v₁, u₁} C
h :
  Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ H.toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (homMk' (snd G.toMon H.toMon))))
    (Hom.hom
      (InducedCategory.Hom.hom
        (IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) G ▷ H ≫
          Iso.hom (λ_ H))))
⊢ Eq (α := tensorObj (𝒞 := instCategory) G H ⟶ H) (homMk' (snd G.toMon H.toMon))
    (IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) G ▷ H ≫
      Iso.hom (λ_ H))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H_1 H₁ H₂ G H : Grp.{v₁, u₁} C
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ H.toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (homMk' (snd G.toMon H.toMon))))
    (Hom.hom
      (InducedCategory.Hom.hom
        (IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) G ▷ H ≫
          Iso.hom (λ_ H))))

Tactic:
apply snd_def

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H₁ H₂ : Grp.{v₁, u₁} C
f : G ⟶ H₁
g : G ⟶ H₂
⊢ Eq (α := G.toMon ⟶ (tensorObj (𝒞 := instCategory) H₁ H₂).toMon) (InducedCategory.Hom.hom (lift f g))
    (lift f.hom g.hom)

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ G.toMon.X) (Hom.hom (InducedCategory.Hom.hom (fst G H)))
    (fst G.X H.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ H.toMon.X) (Hom.hom (InducedCategory.Hom.hom (snd G H)))
    (snd G.X H.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
⊢ Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ (tensorObj (𝒞 := instCategory) H G).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.hom (β_ G H)))) (Iso.hom (β_ G.X H.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.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
⊢ Eq (α := (tensorObj (𝒞 := instCategory) H G).toMon.X ⟶ (tensorObj (𝒞 := instCategory) G H).toMon.X)
    (Hom.hom (InducedCategory.Hom.hom (Iso.inv (β_ G H)))) (Iso.inv (β_ G.X H.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : F'.Monoidal
inst_8 : G_1.Monoidal
G : C
inst_9 : GrpObj G
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj G) (F.obj G))
      (lift (F.map (@GrpObj.inv _ _ inst_1 _ _)) (𝟙 (F.obj G))) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (toUnit (F.obj G)) η

Tactic:
simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc,
      Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.Monoidal.toUnit_ε_assoc, CategoryTheory.Functor.Monoidal.lift_μ_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G_1 : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : F'.Monoidal
inst_8 : G_1.Monoidal
G : C
inst_9 : GrpObj G
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj G) (F.obj G))
      (lift (𝟙 (F.obj G)) (F.map (@GrpObj.inv _ _ inst_1 _ _))) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (toUnit (F.obj G)) η

Tactic:
simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc,
      Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.Monoidal.toUnit_ε_assoc, CategoryTheory.Functor.Monoidal.lift_μ_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
G : C
inst_5 : GrpObj G
⊢ Eq (α := F.obj G ⟶ F.obj G) (@GrpObj.inv _ _ inst_3 _ _) (F.map (@GrpObj.inv _ _ inst_1 _ _))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : F'.Monoidal
inst_8 : G.Monoidal
inst_9 : F.Full
inst_10 : F.Faithful
⊢ Full (C := Grp.{v₁, u₁} C) (D := Grp.{v₂, u₂} D) F.mapGrp

Tactic:
((FullyFaithful.ofFullyFaithful F).mapGrp).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Functor.FullyFaithful.mapGrp, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : Grp.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ Grp.X (obj (mapGrp (𝟭 C)) A)) η
    (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : Grp.{v₁, u₁} C
⊢ μ = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X) ≫ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
A : Grp.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₃, u₃} E (𝒞 := inst_4) ⟶ Grp.X (obj (F ⋙ G).mapGrp A)) η
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε (F ⋙ G)) ((F ⋙ G).map η))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
A : Grp.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (Grp.X (obj (F ⋙ G).mapGrp A)) (Grp.X (obj (F ⋙ G).mapGrp A)) ⟶
      Grp.X (obj (F ⋙ G).mapGrp A))
    μ
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ (F ⋙ G) A.X A.X)
      ((F ⋙ G).map μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : F'.Monoidal
inst_8 : G.Monoidal
hF : F.FullyFaithful
X : C
inst_9 : GrpObj (F.obj X)
⊢ F.map
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X)
        (lift (hF.preimage (@GrpObj.inv _ _ inst_3 _ _)) (𝟙 X)) μ) =
    F.map (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)

Tactic:
simp [OplaxMonoidal.η_of_cartesianMonoidalCategory]

Premises used: CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : F'.Monoidal
inst_8 : G.Monoidal
hF : F.FullyFaithful
X : C
inst_9 : GrpObj (F.obj X)
⊢ F.map
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X)
        (lift (𝟙 X) (hF.preimage (@GrpObj.inv _ _ inst_3 _ _))) μ) =
    F.map (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)

Tactic:
simp [OplaxMonoidal.η_of_cartesianMonoidalCategory]

Premises used: CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : Grp.{v₁, u₁} C
e : obj F.mapGrp H ≅ G
⊢ F.essImage G.X

Tactic:
⟨H.X, ⟨(Grp.forget _).mapIso e⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Grp.forget, Exists.intro, CategoryTheory.Functor.mapIso, CategoryTheory.Grp.X
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : Grp.{v₁, u₁} C
e : obj F.mapGrp H ≅ G
⊢ F.essImage G.X

Tactic:
exact ⟨H.X, ⟨(Grp.forget _).mapIso e⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : C
e : F.obj H ≅ G.X
this_1 : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ essImage (C := Grp.{v₁, u₁} C) F.mapGrp G

Tactic:
⟨⟨H⟩, ⟨Grp.mkIso e ?_ ?_⟩⟩

Premises used: CategoryTheory.Grp.mk, CategoryTheory.Grp.mkIso, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : C
e : F.obj H ≅ G.X
this_1 : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
refine_1 : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.X) (η ≫ e.hom) η
refine_2 :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2)
        (Grp.X (obj (C := Grp.{v₁, u₁} C) F.mapGrp { X := H, grp := this : Grp.{v₁, u₁} C }))
        (Grp.X (obj (C := Grp.{v₁, u₁} C) F.mapGrp { X := H, grp := this : Grp.{v₁, u₁} C })) ⟶
      G.X)
    (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)
⊢ essImage (C := Grp.{v₁, u₁} C) F.mapGrp G

Tactic:
refine ⟨⟨H⟩, ⟨Grp.mkIso e ?_ ?_⟩⟩