awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b₁ b₂ : R
⊢ (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
simp only [add_smul]

Premises used: add_smul
-- 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 ⟶ Z
add add₁ : Eq.{v + 1} (α := F.obj X ⟶ F.obj Z) 0 0
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- 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 ⟶ Z
b₁ b₂ : R
⊢ (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
simp only [add_smul]

Premises used: add_smul
-- 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
f' : X ⟶ Y
r : R
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ 0) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum 0 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
single :
  Eq (α := F.obj X ⟶ F.obj Z)
    (sum (HAdd.hAdd (α := X ⟶ Z) (Finsupp.single f' r ≫ f₁) (Finsupp.single f' r ≫ f₂)) fun (f' : X ⟶ Z) (r : R) ↦
      r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      ((f₁ + f₂).sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ (f₁ + f₂)) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      ((f₁ + f₂).sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
rw [comp_add]

Premises used: CategoryTheory.Preadditive.comp_add
-- 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
single :
  HAdd.hAdd (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (sum (Finsupp.single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f') =
    (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') ≫
      HAdd.hAdd (α := F.obj Y ⟶ F.obj Z) (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f')
        (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f')
single₁ : ∀ (a : Y ⟶ Z), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
single₂ : ∀ (a : Y ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
single₃ : ∀ (a : X ⟶ Z), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
single₄ : ∀ (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) (Finsupp.single f' r ≫ f₁) (Finsupp.single f' r ≫ f₂)) fun (f' : X ⟶ Z) (r : R) ↦
      r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      ((f₁ + f₂).sum 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
⊢ HAdd.hAdd (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (sum (single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f') =
    (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') ≫
      HAdd.hAdd (α := F.obj Y ⟶ F.obj Z) (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f')
        (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f')

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

Premises used: CategoryTheory.Preadditive.comp_add
-- 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
a : Y ⟶ Z
single single₁ : Eq.{v + 1} (α := F.obj Y ⟶ F.obj Z) 0 0
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
a : Y ⟶ Z
b₁ b₂ : R
⊢ (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
simp only [add_smul]

Premises used: add_smul
-- 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
a : X ⟶ Z
single single₁ : Eq.{v + 1} (α := F.obj X ⟶ F.obj Z) 0 0
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0

Tactic:
rw [zero_smul]

Premises used: zero_smul
-- 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
f' : X ⟶ Y
r : R
f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R
w₁ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
w₂ :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
a : X ⟶ Z
b₁ b₂ : R
⊢ (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
simp only [add_smul]

Premises used: add_smul
-- 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
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
single :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single (f' ≫ g') (r * s)) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum (Finsupp.single g' s) fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ Finsupp.single g' s) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum (Finsupp.single g' s) fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
rw [single_comp_single _ _ f' g' r s]

Premises used: CategoryTheory.Free.single_comp_single
-- 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
f' : X ⟶ Y
r : R
g' : Y ⟶ Z
s : R
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (single (f' ≫ g') (r * s)) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum (single g' s) fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
simp [mul_comm r s, mul_smul]

Premises used: mul_comm, SemigroupAction.mul_smul
-- 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' : X ⟶ Y
r : R
single :
  Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ 0) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum 0 fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
single₁ :
  ∀ (f₁ f₂ : Finsupp.{v, u_1} (Y ⟶ Z) R)
    (w₁ :
      Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₁) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
        (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
          (f₁.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f')))
    (w₂ :
      Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ f₂) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
        (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
          (f₂.sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))),
    Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ (f₁ + f₂)) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
        ((f₁ + f₂).sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
single₂ :
  ∀ (g' : Y ⟶ Z) (s : R),
    Eq (α := F.obj X ⟶ F.obj Z)
      (sum (Finsupp.single f' r ≫ Finsupp.single g' s) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
        (sum (Finsupp.single g' s) fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
induction g using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [comp_add]
        rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
        · simp only [w₁, w₂, comp_add]
        · intros; rw [zero_smul]
        · intros; simp only [add_smul]
        · intros; rw [zero_smul]
        · intros; simp only [add_smul]
      | single g' s =>
        rw [single_comp_single _ _ f' g' r s]
        simp [mul_comm r s, mul_smul]

Premises used: Finsupp.sum_add_index', zero_smul, add_smul, CategoryTheory.Preadditive.comp_add, SemigroupAction.mul_smul, Finsupp.single
-- 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
f : X ⟶ Y
g : Y ⟶ Z
zero :
  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'))
add :
  ∀ (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'))),
    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'))
single :
  ∀ (f' : X ⟶ Y) (r : R),
    Eq (α := F.obj X ⟶ F.obj Z) (sum (Finsupp.single f' r ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
      (CategoryStruct.comp (Y := F.obj Y) (sum (Finsupp.single f' r) 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 ≫ g) fun (f' : X ⟶ Z) (r : R) ↦ r • F.map f')
    (CategoryStruct.comp (Y := F.obj Y) (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))

Tactic:
induction f using Finsupp.induction_linear with
    | zero => simp
    | add f₁ f₂ w₁ w₂ =>
      rw [add_comp]
      rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
      · simp only [w₁, w₂, add_comp]
      · intros; rw [zero_smul]
      · intros; simp only [add_smul]
      · intros; rw [zero_smul]
      · intros; simp only [add_smul]
    | single f' r =>
      induction g using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [comp_add]
        rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
        · simp only [w₁, w₂, comp_add]
        · intros; rw [zero_smul]
        · intros; simp only [add_smul]
        · intros; rw [zero_smul]
        · intros; simp only [add_smul]
      | single g' s =>
        rw [single_comp_single _ _ f' g' r s]
        simp [mul_comm r s, mul_smul]

Premises used: Finsupp.sum_add_index', CategoryTheory.Preadditive.add_comp, zero_smul, add_smul, CategoryTheory.Preadditive.comp_add, SemigroupAction.mul_smul, Finsupp.single
-- 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 : C
f : X ⟶ Y
r : R
⊢ Functor.map (lift R F) (single f 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 : Free R C
f g : X ⟶ Y
dsimp :
  (sum (f + g) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') =
    HAdd.hAdd (α := F.obj X ⟶ F.obj Y) (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
⊢ Functor.map (lift R F) (f + g) =
    HAdd.hAdd (α := Functor.obj (lift R F) X ⟶ Functor.obj (lift R F) Y) (Functor.map (lift R F) f)
      (Functor.map (lift R F) g)

Tactic:
dsimp
-- 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 : Free R C
f g : X ⟶ Y
h_zero : ∀ (a : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
h_add : ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
⊢ (sum (f + g) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') =
    HAdd.hAdd (α := F.obj X ⟶ F.obj Y) (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
      (sum g fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')

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
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 : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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 : Free R C
f g : X ⟶ Y
⊢ ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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 : Free R C
f : X ⟶ Y
r : R
dsimp :
  (sum (r • f) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') =
    HSMul.hSMul (β := F.obj X ⟶ F.obj Y) r (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
⊢ Functor.map (lift R F) (r • f) =
    HSMul.hSMul (β := Functor.obj (lift R F) X ⟶ Functor.obj (lift R F) Y) r (Functor.map (lift R F) f)

Tactic:
dsimp
-- 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 : Free R C
f : X ⟶ Y
r : R
rw :
  (sum f fun (i : X ⟶ Y) (a : R) ↦ (r * a) • F.map i) =
    HSMul.hSMul (β := F.obj X ⟶ F.obj Y) r (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')
rw₁ : ∀ (i : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map i) = 0
⊢ (sum (r • f) fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f') =
    HSMul.hSMul (β := F.obj X ⟶ F.obj Y) r (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')

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
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 : Free R C
f : X ⟶ Y
r : R
⊢ (sum f fun (i : X ⟶ Y) (a : R) ↦ (r * a) • F.map i) =
    HSMul.hSMul (β := F.obj X ⟶ F.obj Y) r (sum f fun (f' : X ⟶ Y) (r : R) ↦ r • F.map f')

Tactic:
simp [Finsupp.smul_sum, mul_smul]

Premises used: Finsupp.smul_sum, SemigroupAction.mul_smul