awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ 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'))
have add₂ : ∀ (a : X ⟶ Y) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ 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'))
have add₃ : ∀ (a : X ⟶ Z), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ 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'))
have add₄ : ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
have add : Eq.{v + 1} (α := F.obj X ⟶ F.obj Y) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
have add : Eq.{v + 1} (α := F.obj X ⟶ F.obj Z) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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'))
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ (f₁ + 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₁ + f₂).sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
have single : Eq (α := F.obj X ⟶ F.obj Z)
  (sum (HAdd.hAdd (α := X ⟶ Z) (single f' r ≫ f₁) (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₁ + f₂).sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
Tactic: rw [comp_add]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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'))
⊢ Eq (α := F.obj X ⟶ F.obj Z)
    (sum (HAdd.hAdd (α := X ⟶ Z) (single f' r ≫ f₁) (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₁ + f₂).sum fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
have single : 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: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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')
⊢ 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'))
have single₁ : ∀ (a : Y ⟶ Z), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ 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'))
have single₂ : ∀ (a : Y ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ 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'))
have single₃ : ∀ (a : X ⟶ Z), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ 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'))
have single₄ : ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
have single : Eq.{v + 1} (α := F.obj Y ⟶ F.obj Z) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
have single : Eq.{v + 1} (α := F.obj X ⟶ F.obj Z) 0 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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' r ≫ single g' 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'))
have single : 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: rw [single_comp_single _ _ f' g' r s]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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
⊢ Eq (α := F.obj X ⟶ F.obj Z) (sum (single f' r ≫ g) 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 g fun (f' : Y ⟶ Z) (r : R) ↦ r • F.map f'))
have single : 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: 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]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
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'))
⊢ 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'))
have 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'))
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]
Cleared hypotheses: g