-- 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
refine_1 :
  (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
refine_2 :
  (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
refine_3 :
  m ≫ snd (tensorObj.{v₁, u₁} (𝒞 := inst) A 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)
      (snd (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
⊢ 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:
refine CartesianMonoidalCategory.hom_ext _ _ (CartesianMonoidalCategory.hom_ext _ _ ?_ ?_) ?_

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext