awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
refine_1 :
  ∀ (n : X ⟶ G),
    Membership.mem (γ := Subgroup (X ⟶ G)) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X)) n →
      ∀ (g : X ⟶ G), Membership.mem (γ := Subgroup (X ⟶ G)) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X)) (g * n * g⁻¹)
⊢ Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))

Tactic:
constructor
-- 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
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
x : X ⟶ H
z : X ⟶ G
⊢ (monoidHom φ X : (a : X ⟶ H) → X ⟶ G) (lift z x ≫ ψ) =
    HMul.hMul (β := X ⟶ G) z ((monoidHom φ X : (a : X ⟶ H) → X ⟶ G) x : X ⟶ G) * z⁻¹

Tactic:
simp [hψ]
-- 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
hψ : ψ ≫ φ = G ◁ φ ≫ conj G
X : C
x : X ⟶ H
z : X ⟶ G
⊢ Membership.mem (γ := Subgroup (X ⟶ G)) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
    (HMul.hMul (β := X ⟶ G) z ((monoidHom φ X : (a : X ⟶ H) → X ⟶ G) x : X ⟶ G) * z⁻¹)

Tactic:
exact ⟨lift z x ≫ ψ, by simp [hψ]⟩
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
X : C
g : X ⟶ G
h : X ⟶ H
⊢ Membership.mem (γ := Subgroup (X ⟶ G)) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X)) (h ≫ φ)

Tactic:
simp
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
⊢ ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), ∃ (h' : X ⟶ H), h' ≫ φ = g * h ≫ φ * g⁻¹

Tactic:
have (X : C) (g : X ⟶ G) (h : X ⟶ H) : ∃ (h' : X ⟶ H), h' ≫ φ = g * h ≫ φ * g⁻¹ :=
      (hnormal X).conj_mem (h ≫ φ) (by simp) g
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
this : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), ∃ (h' : X ⟶ H), h' ≫ φ = g * h ≫ φ * g⁻¹
refine_2 :
  ∀ (h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H)
    (hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹),
    ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G
⊢ ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
choose h' hh' using this
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
⟨Yoneda.fullyFaithful.preimage ?_, ?_⟩

Premises used: CategoryTheory.Yoneda.fullyFaithful, CategoryTheory.Functor.FullyFaithful.preimage, Exists.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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
refine_2 :
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, v_1 + 1} Cᵒᵖ (Type v_1))
    (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) (Functor.obj yoneda H)
refine_2₁ :
  Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ G)
    (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
        {
          app := fun (X : Cᵒᵖ) ↦
            ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
              h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
          naturality := ⋯ } ≫
      φ)
    (G ◁ φ ≫ conj G)
⊢ ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
refine ⟨Yoneda.fullyFaithful.preimage ?_, ?_⟩
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
refine_2 :
  ∀ (X Y : Cᵒᵖ) (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶ Functor.obj (Functor.obj yoneda H) Y)
      (Functor.map (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) f ≫
        (fun (X : Cᵒᵖ) ↦
            (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
              Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
                Functor.obj (Functor.obj yoneda H) X))
          Y)
      ((fun (X : Cᵒᵖ) ↦
            (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
              Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
                Functor.obj (Functor.obj yoneda H) X))
          X ≫
        Functor.map (Functor.obj yoneda H) f)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, v_1 + 1} Cᵒᵖ (Type v_1))
    (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) (Functor.obj yoneda H)

Tactic:
refine ⟨fun X ↦ ↾fun x ↦ h' _ (x ≫ fst _ _) (x ≫ snd _ _), fun X Y f ↦ ?_⟩
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
X Y : Cᵒᵖ
f : X ⟶ Y
refine_2 :
  ∀ (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X),
    Eq (α := Functor.obj (Functor.obj yoneda H) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) f ≫
            (fun (X : Cᵒᵖ) ↦
                (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                    h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
                  Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
                    Functor.obj (Functor.obj yoneda H) X))
              Y))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((fun (X : Cᵒᵖ) ↦
                (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                    h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
                  Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
                    Functor.obj (Functor.obj yoneda H) X))
              X ≫
            Functor.map (Functor.obj yoneda H) f))
        x)
⊢ Eq (α :=
    Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶ Functor.obj (Functor.obj yoneda H) Y)
    (Functor.map (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) f ≫
      (fun (X : Cᵒᵖ) ↦
          (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
              h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
            Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
              Functor.obj (Functor.obj yoneda H) X))
        Y)
    ((fun (X : Cᵒᵖ) ↦
          (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
              h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
            Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
              Functor.obj (Functor.obj yoneda H) X))
        X ≫
      Functor.map (Functor.obj yoneda H) f)

Tactic:
ext
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
X Y : Cᵒᵖ
f : X ⟶ Y
x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X
⊢ Eq (α := Functor.obj (Functor.obj yoneda H) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) f ≫
          (fun (X : Cᵒᵖ) ↦
              (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                  h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
                Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
                  Functor.obj (Functor.obj yoneda H) X))
            Y))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Cᵒᵖ) ↦
              (↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                  h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H) :
                Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X ⟶
                  Functor.obj (Functor.obj yoneda H) X))
            X ≫
          Functor.map (Functor.obj yoneda H) f))
      x)

Tactic:
simp [← cancel_mono φ, hh', comp_mul, comp_inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.comp_inv
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ G)
    (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
        {
          app := fun (X : Cᵒᵖ) ↦
            ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
              h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
          naturality := ⋯ } ≫
      φ)
    (G ◁ φ ≫ conj G)

Tactic:
yoneda.map_injective ?_

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_injective
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
refine_2 :
  Eq (α :=
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, v_1 + 1} Cᵒᵖ (Type v_1))
      (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) (Functor.obj yoneda G))
    (Functor.map yoneda
      (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
          {
            app := fun (X : Cᵒᵖ) ↦
              ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
            naturality := ⋯ } ≫
        φ))
    (Functor.map yoneda (G ◁ φ ≫ conj G))
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ G)
    (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
        {
          app := fun (X : Cᵒᵖ) ↦
            ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
              h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
          naturality := ⋯ } ≫
      φ)
    (G ◁ φ ≫ conj G)

Tactic:
refine yoneda.map_injective ?_

Premises used: CategoryTheory.yoneda, CategoryTheory.Functor.map_injective
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
refine_2 :
  ∀ (x : Cᵒᵖ) (x_1 : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Functor.map yoneda
              (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
                  {
                    app := fun (X : Cᵒᵖ) ↦
                      ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                        h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
                    naturality := ⋯ :
                    NatTrans.{v_1, v_1, u_1, v_1 + 1} (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H))
                      (Functor.obj yoneda H) } ≫
                φ))
            x))
        x_1 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map yoneda (G ◁ φ ≫ conj G)) x)) x_1
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, v_1 + 1} Cᵒᵖ (Type v_1))
      (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) (Functor.obj yoneda G))
    (Functor.map yoneda
      (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
          {
            app := fun (X : Cᵒᵖ) ↦
              ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
            naturality := ⋯ } ≫
        φ))
    (Functor.map yoneda (G ◁ φ ≫ conj G))

Tactic:
ext
-- 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 φ
hnormal : ∀ (X : C), Subgroup.Normal.{v_1} (G := X ⟶ G) (MonoidHom.range (G := X ⟶ H) (monoidHom φ X))
h' : (X : C) → (g : X ⟶ G) → (h : X ⟶ H) → X ⟶ H
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
x : Cᵒᵖ
x_1 : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map yoneda
            (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
                {
                  app := fun (X : Cᵒᵖ) ↦
                    ↾fun (x : Functor.obj (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) X) ↦
                      h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H),
                  naturality := ⋯ :
                  NatTrans.{v_1, v_1, u_1, v_1 + 1} (Functor.obj yoneda (tensorObj.{v_1, u_1} (𝒞 := inst) G H))
                    (Functor.obj yoneda H) } ≫
              φ))
          x))
      x_1 =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map yoneda (G ◁ φ ≫ conj G)) x))
      x_1

Tactic:
simp [hh', conj, comp_mul, comp_inv]

Premises used: CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.comp_inv, CategoryTheory.GrpObj.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 K : C
inst_2 : GrpObj G
inst_3 : GrpObj H
inst_4 : GrpObj K
φ : H ⟶ G
inst_5 : BraidedCategory.{v_1, u_1} C
inst_6 : IsCommMonObj.{v_1, u_1} G
inst_7 : IsMonHom φ
inst_8 : Mono φ
⊢ Normal φ

Tactic:
simp [isNormalHom_iff, conj_eq_snd_of_isCommMonObj]

Premises used: CategoryTheory.IsMonHom.isNormalHom_iff, CategoryTheory.GrpObj.conj_eq_snd_of_isCommMonObj
-- 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 φ
P : C
p : G ⟶ P
inst_5 : GrpObj P
inst_6 : IsMonHom p
h : IsPullback (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst)) φ (toUnit H) p η
⊢ ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
⟨h.lift (G ◁ φ ≫ conj G) (toUnit _) ?_, ?_⟩

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.GrpObj.conj, CategoryTheory.IsPullback.lift, 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 φ
P : C
p : G ⟶ P
inst_5 : GrpObj P
inst_6 : IsMonHom p
h : IsPullback (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst)) φ (toUnit H) p η
refine_1 :
  (G ◁ φ ≫ conj G) ≫ p =
    CategoryStruct.comp (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst)) (toUnit (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) η
refine_2 : h.lift (G ◁ φ ≫ conj G) (toUnit (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) ⋯ ≫ φ = G ◁ φ ≫ conj G
⊢ ∃ (ψ : tensorObj.{v_1, u_1} (𝒞 := inst) G H ⟶ H), ψ ≫ φ = G ◁ φ ≫ conj G

Tactic:
refine ⟨h.lift (G ◁ φ ≫ conj G) (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 φ
P : C
p : G ⟶ P
inst_5 : GrpObj P
inst_6 : IsMonHom p
h : IsPullback (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst)) φ (toUnit H) p η
⊢ (G ◁ φ ≫ conj G) ≫ p =
    CategoryStruct.comp (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst)) (toUnit (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) η

Tactic:
simp [conj, comp_mul, inv_comp, mul_comp, h.w, comp_inv, ← Hom.one_def]

Premises used: CategoryTheory.MonObj.mul_comp, CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.inv_comp, CategoryTheory.Hom.one_def, CategoryTheory.GrpObj.comp_inv, CategoryTheory.IsPullback.toCommSq, CategoryTheory.GrpObj.conj, CategoryTheory.CommSq.w
-- 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 φ
P : C
p : G ⟶ P
inst_5 : GrpObj P
inst_6 : IsMonHom p
h : IsPullback (Y := tensorUnit.{v_1, u_1} C (𝒞 := inst)) φ (toUnit H) p η
⊢ h.lift (G ◁ φ ≫ conj G) (toUnit (tensorObj.{v_1, u_1} (𝒞 := inst) G H)) ⋯ ≫ φ = G ◁ φ ≫ conj G

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
Y : Over.{v_1, u_1} X
m : Y ⟶ mk (𝟙 X)
⊢ Hom.left m = Hom.left ((fun (Y : Over.{v_1, u_1} X) ↦ (homMk Y.hom ⋯ : Y ⟶ mk (𝟙 X))) Y)

Tactic:
simpa using m.w

Premises used: CategoryTheory.Over.Hom.w
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X R : C
S T : Over.{v_1, u_1} X
f₁ f₂ : R ⟶ (tensorObj (𝒞 := instCategoryOver) S T).left
e₁ : f₁ ≫ pullback.fst S.hom T.hom = f₂ ≫ pullback.fst S.hom T.hom
e₂ : f₁ ≫ pullback.snd S.hom T.hom = f₂ ≫ pullback.snd S.hom T.hom
⊢ f₁ = f₂

Tactic:
pullback.hom_ext e₁ e₂

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
R S : Over.{v_1, u_1} X
⊢ (tensorObj (𝒞 := instCategoryOver) R S).left = Limits.pullback R.hom S.hom

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
R S : Over.{v_1, u_1} X
⊢ (tensorObj (𝒞 := instCategoryOver) R S).hom = pullback.fst R.hom S.hom ≫ R.hom

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
⊢ left.{v_1, u_1} (X := X) ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver)) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := left.{v_1, u_1} (X := X) ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver)) ⟶ X)
    (hom ((𝟙_ (Over.{v_1, u_1} X)) (𝒞 := instCategoryOver))) (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
R S T : Over.{v_1, u_1} X
f : R ⟶ S
g : R ⟶ T
⊢ Eq (α := R.left ⟶ (tensorObj (𝒞 := instCategoryOver) S T).left) (Hom.left (lift f g))
    (pullback.lift (Hom.left f) (Hom.left g) ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.PullbackCone.mk, CategoryTheory.Limits.limit.lift, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
R S : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ R.left) (Hom.left (fst R S)) (pullback.fst R.hom S.hom)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
R S : Over.{v_1, u_1} X
⊢ Eq (α := (tensorObj (𝒞 := instCategoryOver) R S).left ⟶ S.left) (Hom.left (snd R S)) (pullback.snd R.hom S.hom)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.π, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X : C
R : Over.{v_1, u_1} X
⊢ Hom.left (toUnit R) = R.hom

Tactic:
rfl

Premises used: rfl