awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
rw₁ :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
⊢ Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ F.map (inv f)ᘁ))
have rw₂ : Eq (α :=
  tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    ((𝟙 (F.obj X) ⊗ₘ inv (F.map f)ᘁ) ≫ (F.map f ⊗ₘ 𝟙 (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))))
Tactic: rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id,
              id_tensorHom, tensorHom_id, ← Category.assoc,
              coevaluation_comp_rightAdjointMate, Category.assoc, ← comp_whiskerRight,
              IsIso.inv_hom_id, id_whiskerRight, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
⊢ (tensorObj (𝒞 := Functor.category)
            { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
              map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
              Functor.{u_3, v_1, u_1, u_2} C D }
            F).map
        f ≫
      ε_ (F.obj Y)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          Y) =
    ε_ (F.obj X)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          X) ≫
      Functor.map ((𝟙_ (Functor.{u_3, v_1, u_1, u_2} C D)) (𝒞 := Functor.category)) f
have dsimp : Eq (α :=
  tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
    (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
  (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ≫
    𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ≫
      𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)))
have rw : Eq (α :=
  tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
    (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
  (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
Tactic: rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc,
              id_tensorHom, tensorHom_id,
              rightAdjointMate_comp_evaluation, ← MonoidalCategory.whiskerLeft_comp_assoc,
              IsIso.hom_inv_id, MonoidalCategory.whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
⊢ Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ≫
      𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)))
have rw₁ : Eq (α :=
  tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
    (inv (F.map f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
  (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
Tactic: rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc,
              id_tensorHom, tensorHom_id,
              rightAdjointMate_comp_evaluation, ← MonoidalCategory.whiskerLeft_comp_assoc,
              IsIso.hom_inv_id, MonoidalCategory.whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
rw₁ :
  Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (inv (F.map f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
⊢ Eq (α :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
      tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
      (F.map (inv f)ᘁ ⊗ₘ F.map f) (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
    (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ≫
      𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)))
have rw₂ : Eq (α :=
  tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) (F.obj X) ⟶
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _) (F.obj Y))
    ((𝟙 (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _) ⊗ₘ F.map f) ≫ (inv (F.map f)ᘁ ⊗ₘ 𝟙 (F.obj Y)))
    (ε_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _)))
  (ε_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
Tactic: rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc,
              id_tensorHom, tensorHom_id,
              rightAdjointMate_comp_evaluation, ← MonoidalCategory.whiskerLeft_comp_assoc,
              IsIso.hom_inv_id, MonoidalCategory.whiskerLeft_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
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
⊢ 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
have 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 ≫ μ)) σ)
Tactic: refine ⟨fun h _ a b c ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (hypothesis)
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
⊢ (a + b) * c = a * c + b * c
have 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 ≫ μ)) σ)
Tactic: have := lift (lift a b) c ≫= h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (hypothesis)
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 ≫ μ)) σ)
⊢ (a + b) * c = a * c + b * c
have 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 ≫ μ)) σ)
Tactic: simp only [lift_whiskerRight_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
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 ≫ μ)) σ)
⊢ (a + b) * c = a * c + b * c
have 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) μ))
    σ
Tactic: simp only [Hom.add_def, Hom.mul_def, this, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (hypothesis)
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
⊢ 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 ≫ μ)) σ)
have h₁ : 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 _ _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
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.{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 ≫ μ)) σ)
have 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))
Tactic: convert! h using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Ring (goal)
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))
⊢ 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 ≫ μ)) σ)
have 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)) μ))
Tactic: convert! h using 2