awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
⊢ Eq (α := (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (Y := M)
            (↟((Finsupp.lift (↑M : Type u) R X : (a : X → (↑M : Type u)) → (X →₀ R) →ₗ[R] (↑M : Type u))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → (↑M : Type u)))) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u))
have erw : HSMul.hSMul (α := R) (β := (↑M : Type u)) 1
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
  (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x
Tactic: erw [Finsupp.lift_apply, Finsupp.sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
erw :
  HSMul.hSMul (α := R) (β := (↑M : Type u)) 1
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x
⊢ Eq (α := (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (Y := M)
            (↟((Finsupp.lift (↑M : Type u) R X : (a : X → (↑M : Type u)) → (X →₀ R) →ₗ[R] (↑M : Type u))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → (↑M : Type u)))) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u))
have erw₁ : HSMul.hSMul (α := R) (β := (↑M : Type u)) 0
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
  0
Tactic: erw [Finsupp.lift_apply, Finsupp.sum_single_index]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
x : Functor.obj (free R) X ⟶ M
⊢ (fun (ψ : X ⟶ (↑M : Type u)) ↦
        (freeDesc
            (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
          Functor.obj (free R) X ⟶ M))
      ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
          (↾fun (x : X) ↦
              (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    carrier) φ :
                  (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                (freeMk x) :
            X ⟶ (↑M : Type u)))
        x) =
    x
have h : ∀ (x_1 : X),
  Eq (α := (↑M : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (Functor.obj (free R) X) M
            ((fun (ψ : X ⟶ (↑M : Type u)) ↦
                (freeDesc
                    (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
                  Functor.obj (free R) X ⟶ M))
              ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
                  (↾fun (x : X) ↦
                      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                            (CC := carrier) φ :
                          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                        (freeMk x) :
                    X ⟶ (↑M : Type u)))
                x)) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x_1) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) x :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x_1) :
      (↑M : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
x : X ⟶ (↑M : Type u)
⊢ (fun (φ : Functor.obj (free R) X ⟶ M) ↦
        (↾fun (x : X) ↦
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  carrier) φ :
                (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
              (freeMk x) :
          X ⟶ (↑M : Type u)))
      ((fun (ψ : X ⟶ (↑M : Type u)) ↦
          (freeDesc
              (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
            Functor.obj (free R) X ⟶ M))
        x) =
    x
have h : ∀ (x_1 : X),
  TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
            (↾fun (x : X) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                      carrier) φ :
                    (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                  (freeMk x) :
              X ⟶ (↑M : Type u)))
          ((fun (ψ : X ⟶ (↑M : Type u)) ↦
              (freeDesc
                  (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
                Functor.obj (free R) X ⟶ M))
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) x).toFun x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g :
  Y ⟶
    Functor.obj
      (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)) M
⊢ Eq (α := Functor.obj (free R) X ⟶ M)
    ((Equiv.symm freeHomEquiv : (a : X ⟶ (forget (ModuleCat R)).obj M) → (free R).obj X ⟶ M) (f ≫ g) :
      Functor.obj (free R) X ⟶ M)
    (CategoryTheory.Functor.map (free R) f ≫
        (Equiv.symm freeHomEquiv : (a : Y ⟶ (forget (ModuleCat R)).obj M) → (free R).obj Y ⟶ M) g :
      Functor.obj (free R) X ⟶ M)
have h : ∀ (x : X),
  Eq (α := (↑M : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (Functor.obj (free R) X) M
            ((Equiv.symm freeHomEquiv : (a : X ⟶ (forget (ModuleCat R)).obj M) → (free R).obj X ⟶ M) (f ≫ g)) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (Y := M)
            (CategoryTheory.Functor.map (free R) f ≫
              (Equiv.symm freeHomEquiv : (a : Y ⟶ (forget (ModuleCat R)).obj M) → (free R).obj Y ⟶ M) g) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))
      ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))
    (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit)) (𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))
have hf : Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
  ((Hom.hom (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit)) : (a : R) → (↑(𝟙_ (ModuleCat R)) : Type u))
      1 :
    (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
  (((Hom.hom (𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) :
          (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
            (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
        (a : R) → (↑(𝟙_ (ModuleCat R)) : Type u))
      1 :
    (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
⊢ 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))))
have 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))
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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)
              (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))
have 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)
Tactic: dsimp [freeMk]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing 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)
have 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)
Tactic: erw [Finsupp.lapply_apply, Finsupp.lsingle_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
⊢ 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)
have h : Eq (α := (↑(Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types))) : Type u)) (Finsupp.single PUnit.unit 1)
  (Finsupp.single PUnit.unit 1)
Tactic: rw [Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
x : PUnit.{u + 1}
⊢ 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))
have 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))
Tactic: dsimp [εIso, freeMk]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
x : PUnit.{u + 1}
⊢ 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))
have 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))
Tactic: erw [Finsupp.lapply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
x : PUnit.{u + 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))
have rw : Eq.{u + 1} (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) 1 1
Tactic: rw [Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y : Type u
x : X
y : Y
⊢ 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)
have 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)
Tactic: erw [finsuppTensorFinsupp'_single_tmul_single]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y : Type u
x : X
y : Y
⊢ 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)
have rw : Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u)) (Finsupp.single (x, y) 1)
  (Finsupp.single (x, y) 1)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y : Type u
z : tensorObj (𝒞 := types) X Y
⊢ 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))
have 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))
Tactic: dsimp [μIso, freeMk]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y : Type u
z : tensorObj (𝒞 := types) X Y
⊢ 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))
have 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)
Tactic: erw [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y : Type u
f : X ⟶ Y
X' : Type u
⊢ 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'))
have 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'))
Tactic: rw [← cancel_epi (μIso R X X').inv]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y X' : Type u
f : X ⟶ Y
⊢ 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))
have 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))
Tactic: rw [← cancel_epi (μIso R X' X).inv]