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' : 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'))
⊢ 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₂ : ∀ (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'))
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
f : X ⟶ Y
g : Y ⟶ Z
⊢ 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'))
have 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'))
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]
Cleared hypotheses: f
-- 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
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'))
⊢ 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'))
have 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'))
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]
Cleared hypotheses: f
-- 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
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'))
⊢ 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'))
have single : ∀ (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'))
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]
Cleared hypotheses: f
-- 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 : Free R C
f g : X ⟶ Y
⊢ 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)
have 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')
Tactic: dsimp
-- 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 : Free R C
f g : X ⟶ Y
⊢ (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')
have h_zero : ∀ (a : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
Tactic: rw [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 : Free R C
f g : X ⟶ Y
h_zero : ∀ (a : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
⊢ (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')
have h_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']
-- 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 : Free R C
f : X ⟶ Y
r : R
⊢ 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)
have 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')
Tactic: dsimp
-- 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 : Free R C
f : X ⟶ Y
r : R
⊢ (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')
have 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')
Tactic: rw [Finsupp.sum_smul_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 : 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')
⊢ (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')
have rw₁ : ∀ (i : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map i) = 0
Tactic: rw [Finsupp.sum_smul_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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁
w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂
⊢ F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
have add : (F.map f₁ + F.map f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
Tactic: rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, 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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁
w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂
add :
  (F.map f₁ + F.map f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
⊢ F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
have add₁ : HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y))
    (F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)) =
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
Tactic: rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, 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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁
w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂
add :
  (F.map f₁ + F.map f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₁ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y))
      (F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
⊢ F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
have add₂ : Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁ + F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
Tactic: rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, 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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁
w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂
add :
  (F.map f₁ + F.map f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₁ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y))
      (F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₂ :
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁ + F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
⊢ F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
have add₃ : HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
    (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂) =
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
Tactic: rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, 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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁
w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂
add :
  (F.map f₁ + F.map f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₁ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y))
      (F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₂ :
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁ + F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₃ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
      (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
⊢ F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
have add₄ : HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
    (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂) =
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ (G.map f₁ + G.map f₂)
Tactic: rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, 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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f₁ f₂ : Finsupp.{v, u_1} (X ⟶ Y) R
w₁ : F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁
w₂ : F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) = Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂
add :
  (F.map f₁ + F.map f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₁ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (F.map f₁ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y))
      (F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₂ :
  Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁ + F.map f₂ ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₃ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
      (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
add₄ :
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
      (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ (G.map f₁ + G.map f₂)
⊢ F.map (f₁ + f₂) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (f₁ + f₂)
have add₅ : HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
    (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂) =
  HAdd.hAdd (α := F.obj X ⟶ G.obj Y) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₁)
    (Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map f₂)
Tactic: rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, 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 G : Free R C ⥤ D
inst_5 : F.Additive
inst_6 : Functor.Linear R F
inst_7 : G.Additive
inst_8 : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ F.map (single f' r) ≫ Iso.hom ((fun (X : Free R C) ↦ α.app X) Y) =
    Iso.hom ((fun (X : Free R C) ↦ α.app X) X) ≫ G.map (single f' r)
have single : r • F.map (single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (single f' 1)
Tactic: rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]