awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ 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
have 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
Tactic: rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ 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
have 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
Tactic: rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ 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
have 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
Tactic: rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ 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
have rw₄ : s.snd ≫ snd A A = s.snd ≫ snd A A
Tactic: rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
have 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
Tactic: refine CartesianMonoidalCategory.hom_ext _ _ (CartesianMonoidalCategory.hom_ext _ _ ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ 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
have 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
Tactic: refine CartesianMonoidalCategory.hom_ext _ _ (CartesianMonoidalCategory.hom_ext _ _ ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (hypothesis)
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) ≫ 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
have h : 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 _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (hypothesis)
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 ≫ 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
have this : (m ≫ μ ▷ A) ≫ fst A A = s.fst ≫ fst A A
Tactic: have := hm₁ =≫ fst _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ (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
have 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)) μ
Tactic: simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (hypothesis)
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
⊢ 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)) μ
have 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
Tactic: rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
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
⊢ 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)) μ
have 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)) μ
Tactic: rwa [← assoc s.snd, eq_lift_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ @inv _ _ inst_1 _ _ ≫ f = f ≫ @inv _ _ inst_1 _ _
have suffices : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
  (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f)
Tactic: suffices lift (lift f (ι ≫ f)) f =
      lift (lift f (f ≫ ι)) f by simpa using (this =≫ fst _ _) =≫ snd _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f)
have h₀ : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
Tactic: apply (isPullback B).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
h₀ :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f)
have h₁ : Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
  (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
  (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
Tactic: apply (isPullback B).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
have h₀ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (fst B B) =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
    (fst B B)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
h₀ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
      (fst B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
      (fst B B)
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
have h₁ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (snd B B) =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
    (snd B B)
Tactic: apply CartesianMonoidalCategory.hom_ext