awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
h :
  Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (X := Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) (Y :=
              Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
              (CategoryStruct.comp (Y := (𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) (↟(Finsupp.lapply PUnit.unit))
                  (↟(Finsupp.lsingle PUnit.unit)) :
                Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
                  (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))) :
            (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u) →ₗ[R]
              (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u)) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
        (freeMk PUnit.unit) :
      (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) (𝟙 (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
        (freeMk PUnit.unit) :
      (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
      (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))))
    (CategoryStruct.comp (Y := (𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) (↟(Finsupp.lapply PUnit.unit))
        (↟(Finsupp.lsingle PUnit.unit)) :
      Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
        (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))))
    (𝟙 (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) :
      Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
        (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))))

Tactic:
ext ⟨⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
h :
  Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    ((Hom.hom (↟(Finsupp.lsingle PUnit.unit)) :
          (a : (↑(𝟙_ (ModuleCat R)) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
        (((Hom.hom (↟(Finsupp.lapply PUnit.unit)) :
              (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u) →ₗ[R]
                (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
            (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑(𝟙_ (ModuleCat R)) : Type u))
          (Finsupp.single PUnit.unit 1)) :
      (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    (Finsupp.single PUnit.unit 1 : (𝟙_ (Type u)) (𝒞 := types) →₀ R)
⊢ Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (X := Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) (Y :=
              Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
              (CategoryStruct.comp (Y := (𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) (↟(Finsupp.lapply PUnit.unit))
                  (↟(Finsupp.lsingle PUnit.unit)) :
                Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
                  (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))) :
            (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u) →ₗ[R]
              (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u)) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
        (freeMk PUnit.unit) :
      (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) (𝟙 (Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
        (freeMk PUnit.unit) :
      (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))

Tactic:
dsimp [freeMk]

Premises used: ModuleCat.freeMk
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
h :
  Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    (Finsupp.single PUnit.unit ((Finsupp.single PUnit.unit 1 : (a : 𝟙_ (Type u)) → R) PUnit.unit) :
      (𝟙_ (Type u)) (𝒞 := types) →₀ (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (Finsupp.single PUnit.unit 1 : (𝟙_ (Type u)) (𝒞 := types) →₀ R)
⊢ Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    ((Hom.hom (↟(Finsupp.lsingle PUnit.unit)) :
          (a : (↑(𝟙_ (ModuleCat R)) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
        (((Hom.hom (↟(Finsupp.lapply PUnit.unit)) :
              (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u) →ₗ[R]
                (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
            (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑(𝟙_ (ModuleCat R)) : Type u))
          (Finsupp.single PUnit.unit 1)) :
      (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    (Finsupp.single PUnit.unit 1 : (𝟙_ (Type u)) (𝒞 := types) →₀ R)

Tactic:
erw [Finsupp.lapply_apply, Finsupp.lsingle_apply]

Premises used: Finsupp.lapply_apply, Finsupp.lsingle_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
h h₁ :
  Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u)) (Finsupp.single PUnit.unit 1)
    (Finsupp.single PUnit.unit 1)
⊢ Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    (Finsupp.single PUnit.unit ((Finsupp.single PUnit.unit 1 : (a : 𝟙_ (Type u)) → R) PUnit.unit) :
      (𝟙_ (Type u)) (𝒞 := types) →₀ (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (Finsupp.single PUnit.unit 1 : (𝟙_ (Type u)) (𝒞 := types) →₀ R)

Tactic:
rw [Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (Iso.hom (εIso R)) :
        (a : (↑(𝟙_ (ModuleCat R)) : Type u)) → (↑((free R).obj (𝟙_ (Type u))) : Type u))
      1)
    (freeMk PUnit.unit)

Tactic:
rfl

Premises used: ModuleCat.freeMk, rfl, Finsupp.single
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
x : PUnit.{u + 1}
dsimp :
  Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (X := Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) (Y := (𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))
              (↟(Finsupp.lapply PUnit.unit)) :
            (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u) →ₗ[R]
              (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑(𝟙_ (ModuleCat R)) : Type u))
        (Finsupp.single x 1) :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (1 : (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
⊢ Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (Iso.inv (εIso R)) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑(𝟙_ (ModuleCat R)) : Type u))
        (freeMk x) :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (1 : (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))

Tactic:
dsimp [εIso, freeMk]

Premises used: ModuleCat.freeMk, ModuleCat.FreeMonoidal.εIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
x : PUnit.{u + 1}
erw :
  Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    ((Finsupp.single x 1 : (a : 𝟙_ (Type u)) → R) PUnit.unit : R)
    (1 : (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
⊢ Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (X := Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) (Y := (𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))
              (↟(Finsupp.lapply PUnit.unit)) :
            (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u) →ₗ[R]
              (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
          (a : (↑((free R).obj (𝟙_ (Type u))) : Type u)) → (↑(𝟙_ (ModuleCat R)) : Type u))
        (Finsupp.single x 1) :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (1 : (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))

Tactic:
erw [Finsupp.lapply_apply]

Premises used: Finsupp.lapply_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
x : PUnit.{u + 1}
rw rw₁ : Eq.{u + 1} (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) 1 1
⊢ Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    ((Finsupp.single x 1 : (a : 𝟙_ (Type u)) → R) PUnit.unit : R)
    (1 : (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))

Tactic:
rw [Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y : Type u
x : X
y : Y
erw :
  Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u))
    (Finsupp.single (x, y) (HMul.hMul (α := R) 1 1)) (Finsupp.single (x, y) 1)
⊢ Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) (Y :=
            Functor.obj (free R) (tensorObj (𝒞 := types) X Y))
            (↟(↑(finsuppTensorFinsupp' R X Y) :
                TensorProduct R (↑((free R).obj X) : Type u) (↑((free R).obj Y) : Type u) →ₗ[R] X ⊗ Y →₀ R)) :
          (a : (↑((free R).obj X ⊗ (free R).obj Y) : Type u)) → (↑((free R).obj (X ⊗ Y)) : Type u))
        (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) :
      (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u))
    (Finsupp.single (x, y) 1 : X × Y →₀ R)

Tactic:
erw [finsuppTensorFinsupp'_single_tmul_single]

Premises used: finsuppTensorFinsupp'_single_tmul_single
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y : Type u
x : X
y : Y
rw rw₁ :
  Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u)) (Finsupp.single (x, y) 1)
    (Finsupp.single (x, y) 1)
⊢ Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u))
    (Finsupp.single (x, y) (HMul.hMul (α := R) 1 1)) (Finsupp.single (x, y) 1)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y : Type u
z : tensorObj (𝒞 := types) X Y
dsimp :
  Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    (((↑(LinearEquiv.symm (finsuppTensorFinsupp' R X Y)) :
            (X ⊗ Y →₀ R) →ₗ[R] TensorProduct R (↑((free R).obj X) : Type u) (↑((free R).obj Y) : Type u)) :
          (a : (↑((free R).obj (X ⊗ Y)) : Type u)) → (↑((free R).obj X ⊗ (free R).obj Y) : Type u))
        (Finsupp.single z 1) :
      (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    (Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1 :
      TensorProduct R (↑(Functor.obj (free R) X) : Type u) (↑(Functor.obj (free R) Y) : Type u))
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (Iso.inv (μIso R X Y)) :
          (a : (↑((free R).obj (X ⊗ Y)) : Type u)) → (↑((free R).obj X ⊗ (free R).obj Y) : Type u))
        (freeMk z) :
      (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    (freeMk z.1 ⊗ₜ[R] freeMk z.2 :
      TensorProduct R (↑(Functor.obj (free R) X) : Type u) (↑(Functor.obj (free R) Y) : Type u))

Tactic:
dsimp [μIso, freeMk]

Premises used: ModuleCat.freeMk, ModuleCat.FreeMonoidal.μIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y : Type u
z : tensorObj (𝒞 := types) X Y
erw erw₁ :
  Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    (Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1) (Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    (((↑(LinearEquiv.symm (finsuppTensorFinsupp' R X Y)) :
            (X ⊗ Y →₀ R) →ₗ[R] TensorProduct R (↑((free R).obj X) : Type u) (↑((free R).obj Y) : Type u)) :
          (a : (↑((free R).obj (X ⊗ Y)) : Type u)) → (↑((free R).obj X ⊗ (free R).obj Y) : Type u))
        (Finsupp.single z 1) :
      (↑(tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) : Type u))
    (Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1 :
      TensorProduct R (↑(Functor.obj (free R) X) : Type u) (↑(Functor.obj (free R) Y) : Type u))

Tactic:
erw [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Premises used: finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y : Type u
f : X ⟶ Y
X' : Type u
rw :
  Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) X X'))
      (Functor.obj (free R) (tensorObj (𝒞 := types) Y X')))
    (Iso.inv (μIso R X X') ≫ CategoryTheory.Functor.map (free R) f ▷ Functor.obj (free R) X' ≫ Iso.hom (μIso R Y X'))
    (Iso.inv (μIso R X X') ≫ Iso.hom (μIso R X X') ≫ CategoryTheory.Functor.map (free R) (f ▷ X'))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) X'))
      (Functor.obj (free R) (tensorObj (𝒞 := types) Y X')))
    (CategoryTheory.Functor.map (free R) f ▷ Functor.obj (free R) X' ≫ Iso.hom (μIso R Y X'))
    (Iso.hom (μIso R X X') ≫ CategoryTheory.Functor.map (free R) (f ▷ X'))

Tactic:
rw [← cancel_epi (μIso R X X').inv]

Premises used: ModuleCat.FreeMonoidal.μIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y : Type u
f : X ⟶ Y
X' : Type u
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) X X'))
      (Functor.obj (free R) (tensorObj (𝒞 := types) Y X')))
    (Iso.inv (μIso R X X') ≫ CategoryTheory.Functor.map (free R) f ▷ Functor.obj (free R) X' ≫ Iso.hom (μIso R Y X'))
    (Iso.inv (μIso R X X') ≫ Iso.hom (μIso R X X') ≫ CategoryTheory.Functor.map (free R) (f ▷ X'))

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y X' : Type u
f : X ⟶ Y
rw :
  Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) X' X))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X' Y)))
    (Iso.inv (μIso R X' X) ≫ Functor.obj (free R) X' ◁ CategoryTheory.Functor.map (free R) f ≫ Iso.hom (μIso R X' Y))
    (Iso.inv (μIso R X' X) ≫ Iso.hom (μIso R X' X) ≫ CategoryTheory.Functor.map (free R) (X' ◁ f))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X') (Functor.obj (free R) X))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X' Y)))
    (Functor.obj (free R) X' ◁ CategoryTheory.Functor.map (free R) f ≫ Iso.hom (μIso R X' Y))
    (Iso.hom (μIso R X' X) ≫ CategoryTheory.Functor.map (free R) (X' ◁ f))

Tactic:
rw [← cancel_epi (μIso R X' X).inv]

Premises used: ModuleCat.FreeMonoidal.μIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y X' : Type u
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) X' X))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X' Y)))
    (Iso.inv (μIso R X' X) ≫ Functor.obj (free R) X' ◁ CategoryTheory.Functor.map (free R) f ≫ Iso.hom (μIso R X' Y))
    (Iso.inv (μIso R X' X) ≫ Iso.hom (μIso R X' X) ≫ CategoryTheory.Functor.map (free R) (X' ◁ f))

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y Z : Type u
rw :
  Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))))
    (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
      Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
          Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z)))
    (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
      Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
          Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z)))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (tensorObj (𝒞 := moduleCategory R)
        (tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) (Functor.obj (free R) Z))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))))
    (Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
      Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
      Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z)))

Tactic:
rw [← cancel_epi ((μIso R X Y).inv ▷ _), ← cancel_epi (μIso R _ _).inv]

Premises used: ModuleCat.FreeMonoidal.μIso, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X Y Z : Type u
h :
  ∀ (z : Z) (x : X) (y : Y),
    Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
                Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
                  Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
                    Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
                      CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z))) :
            (a : (↑((free R).obj ((X ⊗ Y) ⊗ Z)) : Type u)) → (↑((free R).obj (X ⊗ Y ⊗ Z)) : Type u))
          (freeMk ((x, y), z)) :
        (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
                Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
                  Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
                    Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z))) :
            (a : (↑((free R).obj ((X ⊗ Y) ⊗ Z)) : Type u)) → (↑((free R).obj (X ⊗ Y ⊗ Z)) : Type u))
          (freeMk ((x, y), z)) :
        (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))) : Type u))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))))
    (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
      Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
          Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z)))
    (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
      Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
          Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z)))

Tactic:
ext ⟨⟨x, y⟩, z⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X : Type u
rw :
  Eq (α := Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) X) (Functor.obj (free R) X)) (𝟙 (Functor.obj (free R) X))
    (Iso.inv (λ_ (Functor.obj (free R) X)) ≫
      Iso.hom (εIso R) ▷ Functor.obj (free R) X ≫
        Iso.hom (μIso R ((𝟙_ (Type u)) (𝒞 := types)) X) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (λ_ X)))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) (Functor.obj (free R) X))
      (Functor.obj (free R) X))
    (Iso.hom (λ_ (Functor.obj (free R) X)))
    (Iso.hom (εIso R) ▷ Functor.obj (free R) X ≫
      Iso.hom (μIso R ((𝟙_ (Type u)) (𝒞 := types)) X) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (λ_ X)))

Tactic:
rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X : Type u
⊢ Eq (α := Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) X) (Functor.obj (free R) X)) (𝟙 (Functor.obj (free R) X))
    (Iso.inv (λ_ (Functor.obj (free R) X)) ≫
      Iso.hom (εIso R) ▷ Functor.obj (free R) X ≫
        Iso.hom (μIso R ((𝟙_ (Type u)) (𝒞 := types)) X) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (λ_ X)))

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
X : Type u
rw :
  Eq (α := Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) X) (Functor.obj (free R) X)) (𝟙 (Functor.obj (free R) X))
    (Iso.inv (ρ_ (Functor.obj (free R) X)) ≫
      Functor.obj (free R) X ◁ Iso.hom (εIso R) ≫
        Iso.hom (μIso R X ((𝟙_ (Type u)) (𝒞 := types))) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (ρ_ X)))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))
      (Functor.obj (free R) X))
    (Iso.hom (ρ_ (Functor.obj (free R) X)))
    (Functor.obj (free R) X ◁ Iso.hom (εIso R) ≫
      Iso.hom (μIso R X ((𝟙_ (Type u)) (𝒞 := types))) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (ρ_ X)))

Tactic:
rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv