awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
refine_1 :
  ∀
    (h :
      Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ))
    (x : C) (a b c : x ⟶ R), (a + b) * c = a * c + b * c
refine_2 :
  ∀ (h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c),
    Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ) ↔
    ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
x : C
a b c : x ⟶ R
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
      (σ ▷ R ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)

Tactic:
have := lift (lift a b) c ≫= h
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
x : C
a b c : x ⟶ R
this :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
      (σ ▷ R ≫ μ) =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift a b) σ) c) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)

Tactic:
simp only [lift_whiskerRight_assoc] at this

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
x : C
a b c : x ⟶ R
this :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift a b) σ) c) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
refine_1 :
  CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R) (lift (lift a b) c)
        (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)))
      σ =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift a c) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift b c) μ))
      σ
⊢ (a + b) * c = a * c + b * c

Tactic:
simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Hom.mul_def, CategoryTheory.Hom.add_def
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h : ∀ ⦃X : C⦄ (a b c : X ⟶ R), (a + b) * c = a * c + b * c
⊢ HAdd.hAdd (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
        (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) *
      snd (tensorObj.{v, u} (𝒞 := inst) R R) R =
    HMul.hMul (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
        (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R) +
      HMul.hMul (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
        (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)

Tactic:
replace h := h (fst (R ⊗ R) R ≫ fst _ _) (fst _ _ ≫ snd _ _) (snd _ _)
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)

Tactic:
h
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R) (σ ▷ R)
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
        σ)
      (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
h₂ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
    (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ))
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)

Tactic:
convert! h using 2
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (fst R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (fst R R))
h₂ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (snd R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (snd R R))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
    (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ))
    (lift
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
        (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (fst R R ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (fst R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (fst R R))

Tactic:
simp only [lift_fst]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
    (fst R R ▷ R) (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (fst R R ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (snd R R ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) (snd R R))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      (snd R R))

Tactic:
simp only [lift_snd]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_snd
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
R : C
inst_2 : MonObj R
inst_3 : AddMonObj R
h :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R)
            (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R))
          σ)
        (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
      μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ fst R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
          (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ))
      σ)
h₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ tensorObj.{v, u} (𝒞 := inst) R R)
    (snd R R ▷ R) (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (snd R R ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R)
      (lift (fst (tensorObj.{v, u} (𝒞 := inst) R R) R ≫ snd R R) (snd (tensorObj.{v, u} (𝒞 := inst) R R) R)) μ)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X : C
a b c : X ⟶ R
revert : ∀ {X : C} (a b c : X ⟶ R), a * (b + c) = a * b + a * c
⊢ a * (b + c) = a * b + a * c

Tactic:
revert X a b c
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) R (tensorObj.{v, u} (𝒞 := inst) R R) ⟶ R) (R ◁ σ ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
rw₁ rw₂ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) R (tensorObj.{v, u} (𝒞 := inst) R R) ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ)) σ)
⊢ ∀ {X : C} (a b c : X ⟶ R), a * (b + c) = a * b + a * c

Tactic:
rw [← mul_add_iff, RingObj.mul_add R]

Premises used: CategoryTheory.mul_add_iff, CategoryTheory.RingObj.mul_add
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X : C
a b c : X ⟶ R
revert : ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c
⊢ (a + b) * c = a * c + b * c

Tactic:
revert X a b c
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
rw :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R) (σ ▷ R ≫ μ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
rw₁ rw₂ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) R R) R ⟶ R)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) R R) (lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ)) σ)
⊢ ∀ {X : C} (a b c : X ⟶ R), (a + b) * c = a * c + b * c

Tactic:
rw [← add_mul_iff, RingObj.add_mul R]

Premises used: CategoryTheory.RingObj.add_mul, CategoryTheory.add_mul_iff
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X_1 X : C
a : X ⟶ R
⊢ 0 * a = 0

Tactic:
simpa using add_mul 0 0 a

Premises used: CategoryTheory.Hom.add_mul, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X_1 X : C
a : X ⟶ R
⊢ a * 0 = 0

Tactic:
simpa using mul_add a 0 0

Premises used: OfNat.ofNat, CategoryTheory.Hom.mul_add
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R₁ R₂ : RingObjCat.{v, u} C
f g : R₁ ⟶ R₂
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.RingObjCat.Hom.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R₁ R₂ : CommRingObjCat.{v, u} C
f g : R₁ ⟶ R₂
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: CategoryTheory.CommRingObjCat.Hom.ext