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) μ μ
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
⊢ 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
have 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
Tactic: rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_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 : 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
⊢ 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
have 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
Tactic: rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_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 : 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
⊢ 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
have rw₃ : s.fst ≫ fst A A = s.fst ≫ fst A A
Tactic: rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_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 : 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)
        μ μ),
    (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
have 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
Tactic: refine fun s => CartesianMonoidalCategory.hom_ext _ _ (by simp) ?_
-- 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) μ μ
⊢ 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
have 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
Tactic: simp only [lift_lift_associator_hom_assoc, lift_whiskerLeft, lift_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 : 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 _ _)) μ
have 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 _ _)) μ
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]
-- 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) μ μ
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 _ _)) μ
⊢ 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 _ _)) μ
have 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
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]
-- 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) μ μ
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
⊢ 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 _ _)) μ
have 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
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]
-- 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) μ μ
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
⊢ 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 _ _)) μ
have 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
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]
-- 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) μ μ
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
⊢ 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 _ _)) μ
have 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)) μ
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]
-- 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) μ μ
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)) μ
⊢ 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 _ _)) μ
have rw₅ : s.fst ≫ μ = CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (s.snd ≫ fst A A) (s.snd ≫ snd A A)) μ
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]
-- 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) μ μ
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)) μ
⊢ 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 _ _)) μ
have rw₆ : s.fst ≫ μ = s.snd ≫ μ
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]
-- 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) μ μ
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 ≫ μ
⊢ 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 _ _)) μ
have rw₇ : s.snd ≫ μ = s.snd ≫ μ
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]
-- 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) μ μ
⊢ 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 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 _ _)) μ
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]
-- 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 _ _)) μ
⊢ 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
      (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
Tactic: rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right]