awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : Type u
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (tensorObj (𝒞 := moduleCategory R)
        (tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) (Functor.obj (free R) Y)) (Functor.obj (free R) Z))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))))
    (Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
      Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
      Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z)))
have rw : Eq (α :=
  Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z))
    (Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))))
  (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
    Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
      Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z)))
  (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
    Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
      Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
        Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z)))
Tactic: rw [← cancel_epi ((μIso R X Y).inv ▷ _), ← cancel_epi (μIso R _ _).inv]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : Type u
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) (Functor.obj (free R) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z))
      (Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))))
    (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
      Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
          Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z)))
    (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
      Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
        Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
          Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z)))
have h : ∀ (z : Z) (x : X) (y : Y),
  Eq (α := (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
              Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
                Iso.hom (μIso R X Y) ▷ Functor.obj (free R) Z ≫
                  Iso.hom (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
                    CategoryTheory.Functor.map (free R) (Iso.hom (α_ X Y Z))) :
          (a : (↑((free R).obj ((X ⊗ Y) ⊗ Z)) : Type u)) → (↑((free R).obj (X ⊗ Y ⊗ Z)) : Type u))
        (freeMk ((x, y), z)) :
      (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (Iso.inv (μIso R (tensorObj (𝒞 := types) X Y) Z) ≫
              Iso.inv (μIso R X Y) ▷ Functor.obj (free R) Z ≫
                Iso.hom (α_ (Functor.obj (free R) X) (Functor.obj (free R) Y) (Functor.obj (free R) Z)) ≫
                  Functor.obj (free R) X ◁ Iso.hom (μIso R Y Z) ≫ Iso.hom (μIso R X (tensorObj (𝒞 := types) Y Z))) :
          (a : (↑((free R).obj ((X ⊗ Y) ⊗ Z)) : Type u)) → (↑((free R).obj (X ⊗ Y ⊗ Z)) : Type u))
        (freeMk ((x, y), z)) :
      (↑(Functor.obj (free R) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))) : Type u))
Tactic: ext ⟨⟨x, y⟩, z⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X : Type u
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) (Functor.obj (free R) X))
      (Functor.obj (free R) X))
    (Iso.hom (λ_ (Functor.obj (free R) X)))
    (Iso.hom (εIso R) ▷ Functor.obj (free R) X ≫
      Iso.hom (μIso R ((𝟙_ (Type u)) (𝒞 := types)) X) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (λ_ X)))
have rw : 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)) ≫
    Iso.hom (εIso R) ▷ Functor.obj (free R) X ≫
      Iso.hom (μIso R ((𝟙_ (Type u)) (𝒞 := types)) X) ≫ CategoryTheory.Functor.map (free R) (Iso.hom (λ_ X)))
Tactic: rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Adjunctions (goal)
Goal:
R : Type u
inst : CommRing R
X : Type u
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (tensorObj (𝒞 := moduleCategory R) (Functor.obj (free R) X) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))
      (Functor.obj (free R) X))
    (Iso.hom (ρ_ (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)))
have rw : 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: rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id]
-- 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
X Y Z : Free R C
f f' : X ⟶ Y
g : Y ⟶ Z
⊢ ((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))
have 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
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
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
⊢ ((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))
have 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))
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
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (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))
have 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)))
Tactic: rw [← Finsupp.sum_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
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ 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)))
have 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))
Tactic: congr
-- 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
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ 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))
have 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)
Tactic: ext r h
-- 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
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
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)
have e_g : ∀ (a : Y ⟶ Z), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (r ≫ a) (h * 0)) 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
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
⊢ 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)
have 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₂))
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
X Y Z : Free R C
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ ((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))
have 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))
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
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))
⊢ ((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))
have 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
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
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (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))
have 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)))
Tactic: simp_rw [Finsupp.smul_sum]
-- 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
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ 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)))
have 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))
Tactic: congr
-- 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
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ 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))
have 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)
Tactic: ext h 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
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) (((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)
have 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)
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
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)
⊢ 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)
have e_g₁ : ∀ (i : Y ⟶ Z), Eq (α := Finsupp.{v, u_1} (X ⟶ Z) R) (single (h ≫ i) (s * 0)) 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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single f 1 ≫ single g 1)
have rw : Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single (f ≫ g) (HMul.hMul (α := R) 1 1))
Tactic: rw [single_comp_single, one_mul]
-- 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
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))
⊢ Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single f 1 ≫ single g 1)
have rw₁ : Eq (α := X ⟶ Z) (single (f ≫ g) 1) (single (f ≫ g) 1)
Tactic: rw [single_comp_single, one_mul]
-- 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'))
⊢ 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'))
have 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'))
Tactic: rw [add_comp]
-- 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'))
⊢ 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 : 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: 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'
⊢ 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), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map a) = 0
Tactic: rw [Finsupp.sum_add_index', Finsupp.sum_add_index']