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
A : C
inst_2 : GrpObj A
refine :
  ∀
    (s :
      PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        μ μ),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
          ((fun
                (s :
                  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
              (lift
                  (lift (s.snd ≫ fst A A)
                    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                  (s.fst ≫ snd A A) :
                s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
            s)
          (μ ▷ A))
        (fst A A) =
      s.fst ≫ fst A A
⊢ ∀
    (s :
      PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        μ μ),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (μ ▷ A) =
      s.fst

Tactic:
refine fun s => CartesianMonoidalCategory.hom_ext _ _ ?_ (by simp)

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
simp :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
      μ =
    s.fst ≫ fst A A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (μ ▷ A))
      (fst A A) =
    s.fst ≫ fst A A

Tactic:
simp only [lift_whiskerRight, lift_fst]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight, CategoryTheory.CartesianMonoidalCategory.lift_fst
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A) (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _)) μ)
        (s.fst ≫ fst A A))
      μ =
    s.fst ≫ fst A A
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A) ((s.snd ≫ fst A A) ≫ @inv _ _ inst_1 _ _)) μ)
        (s.fst ≫ fst A A))
      μ =
    s.fst ≫ fst A A
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit s.pt) η) (s.fst ≫ fst A A)) μ =
    s.fst ≫ fst A A
rw₃ rw₄ : s.fst ≫ fst A A = s.fst ≫ fst A A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
      μ =
    s.fst ≫ fst A A

Tactic:
rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.MonObj.lift_comp_one_left, CategoryTheory.GrpObj.lift_comp_inv_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s ≫
        Iso.hom (α_ A A A) ≫ A ◁ μ)
      (fst A A) =
    s.snd ≫ fst A A

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
refine :
  ∀
    (s :
      PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        μ μ),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        ((fun
                (s :
                  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
              (lift
                  (lift (s.snd ≫ fst A A)
                    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                  (s.fst ≫ snd A A) :
                s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
            s ≫
          Iso.hom (α_ A A A) ≫ A ◁ μ)
        (snd A A) =
      s.snd ≫ snd A A
⊢ ∀
    (s :
      PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        μ μ),
    (fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s ≫
        Iso.hom (α_ A A A) ≫ A ◁ μ =
      s.snd

Tactic:
refine fun s => CartesianMonoidalCategory.hom_ext _ _ (by simp) ?_

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
simp :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ)
        (s.fst ≫ snd A A))
      μ =
    s.snd ≫ snd A A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s ≫
        Iso.hom (α_ A A A) ≫ A ◁ μ)
      (snd A A) =
    s.snd ≫ snd A A

Tactic:
simp only [lift_lift_associator_hom_assoc, lift_whiskerLeft, lift_snd]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A) ((s.fst ≫ snd A A) ≫ @inv _ _ inst_1 _ _)) μ
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ)
        (s.fst ≫ snd A A))
      μ =
    s.snd ≫ snd A A
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (s.fst ≫ fst A A) (s.fst ≫ snd A A)) μ))
      μ =
    s.snd ≫ snd A A
rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift ((s.snd ≫ fst A A) ≫ @inv _ _ inst_1 _ _)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (s.fst ≫ fst A A) (s.fst ≫ snd A A)) μ))
      μ =
    s.snd ≫ snd A A
rw₄ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (s.fst ≫ fst A A) (s.fst ≫ snd A A)) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (s.snd ≫ fst A A) (s.snd ≫ snd A A)) μ
rw₅ :
  s.fst ≫ μ = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (s.snd ≫ fst A A) (s.snd ≫ snd A A)) μ
rw₆ : s.fst ≫ μ = s.snd ≫ μ
rw₇ rw₈ : s.snd ≫ μ = s.snd ≫ μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ @inv _ _ inst_1 _ _)) μ

Tactic:
rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq,
          lift_comp_fst_snd, lift_comp_fst_snd, s.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.GrpObj.lift_inv_left_eq, CategoryTheory.GrpObj.eq_lift_inv_right, CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd, CategoryTheory.Limits.PullbackCone.snd
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ @inv _ _ inst_1 _ _)) μ

Tactic:
have : lift (s.snd ≫ fst _ _ ≫ ι) (s.fst ≫ fst _ _) ≫ μ =
          lift (s.snd ≫ snd _ _) (s.fst ≫ snd _ _ ≫ ι) ≫ μ := by
        rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq,
          lift_comp_fst_snd, lift_comp_fst_snd, s.condition]
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ @inv _ _ inst_1 _ _)) μ
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ @inv _ _ inst_1 _ _)) μ)
        (s.fst ≫ snd A A))
      μ =
    s.snd ≫ snd A A
rw₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.fst ≫ snd A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ snd A A)) μ))
      μ =
    s.snd ≫ snd A A
rw₂ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A)
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift ((s.fst ≫ snd A A) ≫ @inv _ _ inst_1 _ _) (s.fst ≫ snd A A)) μ))
      μ =
    s.snd ≫ snd A A
rw₃ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ snd A A) (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit s.pt) η)) μ =
    s.snd ≫ snd A A
rw₄ rw₅ : s.snd ≫ snd A A = s.snd ≫ snd A A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
          (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ)
        (s.fst ≫ snd A A))
      μ =
    s.snd ≫ snd A A

Tactic:
rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonObj.lift_comp_one_right, CategoryTheory.MonObj.lift_lift_assoc, CategoryTheory.GrpObj.lift_comp_inv_left
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
⊢ m =
    (fun
          (s :
            PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
        (lift
            (lift (s.snd ≫ fst A A)
              (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
            (s.fst ≫ snd A A) :
          s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
      s

Tactic:
CartesianMonoidalCategory.hom_ext _ _ (CartesianMonoidalCategory.hom_ext _ _ ?_ ?_) ?_

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
⊢ (m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫ fst A A =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
      fst A A

Tactic:
simpa using hm₂ =≫ fst _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
⊢ m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ fst A A = s.snd ≫ fst A A

Tactic:
simpa using hm₂ =≫ fst _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
⊢ m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ fst A A = s.snd ≫ fst A A

Tactic:
have h : m ≫ fst _ _ ≫ fst _ _ = s.snd ≫ fst _ _ := by simpa using hm₂ =≫ fst _ _
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
h : m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ fst A A = s.snd ≫ fst A A
⊢ (m ≫ μ ▷ A) ≫ fst A A = s.fst ≫ fst A A

Tactic:
have := hm₁ =≫ fst _ _
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
h : m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ fst A A = s.snd ≫ fst A A
this : (m ≫ μ ▷ A) ≫ fst A A = s.fst ≫ fst A A
refine_2 :
  ∀ (this : m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ μ = s.fst ≫ fst A A),
    m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ snd A A =
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
        (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ
⊢ (m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫ snd A A =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
        ((fun
              (s :
                PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
            (lift
                (lift (s.snd ≫ fst A A)
                  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                    (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
                (s.fst ≫ snd A A) :
              s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
          s)
        (fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A) ≫
      snd A A

Tactic:
simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.CartesianMonoidalCategory.lift_fst, CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
h : m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ fst A A = s.snd ≫ fst A A
this : m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ μ = s.fst ≫ fst A A
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A) (m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ snd A A)) μ =
    s.fst ≫ fst A A

Tactic:
rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
h : m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ fst A A = s.snd ≫ fst A A
this :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A) (m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ snd A A)) μ =
    s.fst ≫ fst A A
refine_2 :
  m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ snd A A =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift ((s.snd ≫ fst A A) ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A) (m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ snd A A)) μ =
    s.fst ≫ fst A A
⊢ m ≫ fst (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A ≫ snd A A =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
      (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ

Tactic:
rwa [← assoc s.snd, eq_lift_inv_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.snd, CategoryTheory.GrpObj.eq_lift_inv_left