awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)) ≫
      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:
aesop
-- 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) (X :=
          (𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) (Y := Functor.obj (free R) ((𝟙_ (Type u)) (𝒞 := types)))
          (ε (free 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}
⊢ 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))
            (η (free 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:
apply FreeMonoidal.εIso_inv_freeMk

Premises used: ModuleCat.FreeMonoidal.εIso_inv_freeMk
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
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)) (μ (free R) X Y) :
          (a : (↑((free R).obj X ⊗ (free R).obj Y) : Type u)) → (↑((free R).obj (X ⊗ Y)) : Type u))
        (freeMk x ⊗ₜ[R] freeMk y) :
      (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) : Type u))
    (freeMk (x, y) : (↑(Functor.obj (free R) (X × Y)) : Type u))

Tactic:
apply FreeMonoidal.μIso_hom_freeMk_tmul_freeMk

Premises used: ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
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) (X :=
            Functor.obj (free R) (tensorObj (𝒞 := types) X Y)) (Y :=
            tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) (δ (free 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:
apply FreeMonoidal.μIso_inv_freeMk

Premises used: ModuleCat.FreeMonoidal.μIso_inv_freeMk
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
W X Y Z : Free R C
f : Finsupp.{v, u_1} (W ⟶ X) R
g : Finsupp.{v, u_1} (X ⟶ Y) R
h : Finsupp.{v, u_1} (Y ⟶ Z) R
⊢ Eq (α := Finsupp.{v, u_1} (W ⟶ Z) R)
    (sum (f.sum fun (f' : W ⟶ X) (s : R) ↦ g.sum fun (g' : X ⟶ Y) (t : R) ↦ single (f' ≫ g') (s * t))
      fun (f' : W ⟶ Y) (s : R) ↦ h.sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    (f.sum fun (f' : W ⟶ X) (s : R) ↦
      sum (g.sum fun (f' : X ⟶ Y) (s : R) ↦ h.sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
        fun (g' : X ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))

Tactic:
simp [sum_sum_index, add_mul, mul_add, Category.assoc, mul_assoc]

Premises used: add_mul, CategoryTheory.Category.assoc, mul_assoc, mul_add, Finsupp.sum_sum_index
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
h_zero :
  ∀ (a : X ⟶ Y), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (0 * t)) 0
h_add :
  ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b₁ * t))
        (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b₂ * t))
⊢ ((f + f').sum fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t)) =
    HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R)
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
      (sum f' fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))

Tactic:
rw [Finsupp.sum_add_index']

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (0 * t)) 0

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R),
    (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') ((b₁ + b₂) * t)) =
      HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b₁ * t))
        (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b₂ * t))

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
rw :
  Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R)
    (sum f fun (f' : X ⟶ Y) (s : R) ↦ (g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    (sum f fun (a : X ⟶ Y) (b : R) ↦
      HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t))
        (sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t)))
⊢ (sum f fun (f' : X ⟶ Y) (s : R) ↦ (g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t)) =
    HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R)
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))

Tactic:
rw [← Finsupp.sum_add]

Premises used: Finsupp.sum_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
e_g :
  Eq (α := (X ⟶ Y) → R → Finsupp.{v, u_1} (X ⟶ Z) R)
    (fun (f' : X ⟶ Y) (s : R) ↦ (g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    fun (a : X ⟶ Y) (b : R) ↦
    HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t))
      (sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t))
⊢ Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R)
    (sum f fun (f' : X ⟶ Y) (s : R) ↦ (g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    (sum f fun (a : X ⟶ Y) (b : R) ↦
      HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t))
        (sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t)))

Tactic:
congr
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
e_g :
  ∀ (r : X ⟶ Y) (h : R) (a : X ⟶ Z),
    Eq.{u_1 + 1} (α := R) (((g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (r ≫ g') (h * t) : (a : X ⟶ Z) → R) a : R)
      ((HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (r ≫ g') (h * t))
              (sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (r ≫ g') (h * t)) :
            (a : X ⟶ Z) → R)
          a :
        R)
⊢ Eq (α := (X ⟶ Y) → R → Finsupp.{v, u_1} (X ⟶ Z) R)
    (fun (f' : X ⟶ Y) (s : R) ↦ (g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    fun (a : X ⟶ Y) (b : R) ↦
    HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t))
      (sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (a ≫ g') (b * t))

Tactic:
ext r h
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a : X ⟶ Z
e_g : ∀ (a : Y ⟶ Z), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (r ≫ a) (h * 0)) 0
e_g₁ :
  ∀ (a : Y ⟶ Z) (b₁ b₂ : R),
    single (r ≫ a) (h * (b₁ + b₂)) =
      HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (r ≫ a) (h * b₁)) (single (r ≫ a) (h * b₂))
⊢ Eq.{u_1 + 1} (α := R) (((g + g').sum fun (g' : Y ⟶ Z) (t : R) ↦ single (r ≫ g') (h * t) : (a : X ⟶ Z) → R) a : R)
    ((HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (r ≫ g') (h * t))
            (sum g' fun (g' : Y ⟶ Z) (t : R) ↦ single (r ≫ g') (h * t)) :
          (a : X ⟶ Z) → R)
        a :
      R)

Tactic:
rw [Finsupp.sum_add_index']

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (r ≫ a) (h * 0)) 0

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
r : X ⟶ Y
h : R
a : X ⟶ Z
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R),
    single (r ≫ a) (h * (b₁ + b₂)) =
      HAdd.hAdd (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (r ≫ a) (h * b₁)) (single (r ≫ a) (h * b₂))

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
rw :
  (sum f fun (i : X ⟶ Y) (a : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (i ≫ g') (r * a * t)) =
    HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
rw₁ : ∀ (i : X ⟶ Y), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (i ≫ g') (0 * t)) 0
⊢ ((r • f).sum fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t)) =
    HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))

Tactic:
rw [Finsupp.sum_smul_index]

Premises used: Finsupp.sum_smul_index
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (sum f fun (i : X ⟶ Y) (a : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (i ≫ g') (r * a * t)) =
    HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))

Tactic:
simp [Finsupp.smul_sum, mul_assoc]

Premises used: mul_assoc, Finsupp.smul_sum
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (i : X ⟶ Y), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (i ≫ g') (0 * t)) 0

Tactic:
simp [Finsupp.smul_sum, mul_assoc]

Premises used: mul_assoc, Finsupp.smul_sum
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
simp_rw :
  Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R)
    (sum f fun (f' : X ⟶ Y) (s : R) ↦ (r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    (sum f fun (a : X ⟶ Y) (b : R) ↦
      sum g fun (a_1 : Y ⟶ Z) (b_1 : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (a ≫ a_1) (b * b_1)))
⊢ (sum f fun (f' : X ⟶ Y) (s : R) ↦ (r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t)) =
    HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r
      (sum f fun (f' : X ⟶ Y) (s : R) ↦ sum g fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))

Tactic:
simp_rw [Finsupp.smul_sum]

Premises used: Finsupp.smul_sum
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
e_g :
  Eq (α := (X ⟶ Y) → R → Finsupp.{v, u_1} (X ⟶ Z) R)
    (fun (f' : X ⟶ Y) (s : R) ↦ (r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    fun (a : X ⟶ Y) (b : R) ↦
    sum g fun (a_1 : Y ⟶ Z) (b_1 : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (a ≫ a_1) (b * b_1))
⊢ Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R)
    (sum f fun (f' : X ⟶ Y) (s : R) ↦ (r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    (sum f fun (a : X ⟶ Y) (b : R) ↦
      sum g fun (a_1 : Y ⟶ Z) (b_1 : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (a ≫ a_1) (b * b_1)))

Tactic:
congr
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
e_g :
  ∀ (h : X ⟶ Y) (s : R) (a : X ⟶ Z),
    Eq.{u_1 + 1} (α := R) (((r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (h ≫ g') (s * t) : (a : X ⟶ Z) → R) a : R)
      ((sum g fun (a : Y ⟶ Z) (b : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (h ≫ a) (s * b)) :
            (a : X ⟶ Z) → R)
          a :
        R)
⊢ Eq (α := (X ⟶ Y) → R → Finsupp.{v, u_1} (X ⟶ Z) R)
    (fun (f' : X ⟶ Y) (s : R) ↦ (r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (f' ≫ g') (s * t))
    fun (a : X ⟶ Y) (b : R) ↦
    sum g fun (a_1 : Y ⟶ Z) (b_1 : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (a ≫ a_1) (b * b_1))

Tactic:
ext h s
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a : X ⟶ Z
e_g :
  Eq.{u_1 + 1} (α := R) ((sum g fun (i : Y ⟶ Z) (a : R) ↦ single (h ≫ i) (s * (r * a)) : (a : X ⟶ Z) → R) a : R)
    ((sum g fun (a : Y ⟶ Z) (b : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (h ≫ a) (s * b)) :
          (a : X ⟶ Z) → R)
        a :
      R)
e_g₁ : ∀ (i : Y ⟶ Z), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (h ≫ i) (s * 0)) 0
⊢ Eq.{u_1 + 1} (α := R) (((r • g).sum fun (g' : Y ⟶ Z) (t : R) ↦ single (h ≫ g') (s * t) : (a : X ⟶ Z) → R) a : R)
    ((sum g fun (a : Y ⟶ Z) (b : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (h ≫ a) (s * b)) :
          (a : X ⟶ Z) → R)
        a :
      R)

Tactic:
rw [Finsupp.sum_smul_index]

Premises used: Finsupp.sum_smul_index
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a : X ⟶ Z
⊢ Eq.{u_1 + 1} (α := R) ((sum g fun (i : Y ⟶ Z) (a : R) ↦ single (h ≫ i) (s * (r * a)) : (a : X ⟶ Z) → R) a : R)
    ((sum g fun (a : Y ⟶ Z) (b : R) ↦ HSMul.hSMul (β := Finsupp.{v, u_1} (X ⟶ Z) R) r (single (h ≫ a) (s * b)) :
          (a : X ⟶ Z) → R)
        a :
      R)

Tactic:
simp [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (h ≫ i) (s * 0)) 0

Tactic:
simp [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
r s : R
⊢ Eq (α := Finsupp.{v, u_1} (of R X ⟶ of R Z) R)
    (sum (single f r) fun (f' : of R X ⟶ Y) (s_1 : R) ↦
      sum (single g s) fun (g' : Y ⟶ of R Z) (t : R) ↦ single (f' ≫ g') (s_1 * t))
    (single (f ≫ g) (r * s))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
rw : Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single (f ≫ g) (HMul.hMul (α := R) 1 1))
rw₁ rw₂ : Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single (f ≫ g) 1)
⊢ Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single f 1 ≫ single g 1)

Tactic:
rw [single_comp_single, one_mul]

Premises used: CategoryTheory.Free.single_comp_single, one_mul
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
⊢ ∀ (X : Free R C),
    Eq.{v + 1} (α := F.obj X ⟶ F.obj X) (sum (single (𝟙 X) 1) fun (f' : X ⟶ X) (r : R) ↦ r • F.map f') (𝟙 (F.obj X))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
X Y Z : Free R C
g : Y ⟶ Z
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (0 ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum 0 fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₁ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₁.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₂ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₂.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
add :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (HAdd.hAdd (α := X ⟶ Z) (f₁ ≫ g) (f₂ ≫ g)) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) ((f₁ + f₂).sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum ((f₁ + f₂) ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) ((f₁ + f₂).sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
rw [add_comp]

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₁ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₁.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₂ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₂.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
add :
  HAdd.hAdd (α := F.obj X ⟶ F.obj Z) (sum (f₁ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (sum (f₂ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f') =
    HAdd.hAdd (α := F.obj X ⟶ F.obj Y) (f₁.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
        (f₂.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') ≫
      sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'
add₁ : ∀ (a : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
add₂ : ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
add₃ : ∀ (a : X ⟶ Z), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
add₄ : ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (HAdd.hAdd (α := X ⟶ Z) (f₁ ≫ g) (f₂ ≫ g)) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) ((f₁ + f₂).sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
rw [Finsupp.sum_add_index', Finsupp.sum_add_index']

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₁ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₁.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₂ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₂.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
⊢ HAdd.hAdd (α := F.obj X ⟶ F.obj Z) (sum (f₁ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (sum (f₂ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f') =
    HAdd.hAdd (α := F.obj X ⟶ F.obj Y) (f₁.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
        (f₂.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') ≫
      sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'

Tactic:
simp only [w₁, w₂, add_comp]

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
X Y Z : Free R C
g : Y ⟶ Z
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₁ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₁.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (f₂ ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (f₂.sum fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
a : X ⟶ Y
add add₁ : Eq.{v + 1} (α := F.obj X ⟶ F.obj Y) 0 0
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0

Tactic:
rw [zero_smul]

Premises used: zero_smul