awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X _Y _Z : C
r : ℕ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
exact (Preadditive.rightComp X g).map_nsmul r f

Premises used: AddMonoidHom.map_nsmul, CategoryTheory.Preadditive.rightComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
_X _Y Z : C
f : _X ⟶ _Y
r : ℕ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
(Preadditive.leftComp Z f).map_nsmul r g

Premises used: AddMonoidHom.map_nsmul, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
_X _Y Z : C
f : _X ⟶ _Y
r : ℕ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
exact (Preadditive.leftComp Z f).map_nsmul r g

Premises used: AddMonoidHom.map_nsmul, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X _Y _Z : C
r : ℤ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
(Preadditive.rightComp X g).map_zsmul r f

Premises used: AddMonoidHom.map_zsmul, CategoryTheory.Preadditive.rightComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X _Y _Z : C
r : ℤ
f : X ⟶ _Y
g : _Y ⟶ _Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
exact (Preadditive.rightComp X g).map_zsmul r f

Premises used: AddMonoidHom.map_zsmul, CategoryTheory.Preadditive.rightComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
_X _Y Z : C
f : _X ⟶ _Y
r : ℤ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
(Preadditive.leftComp Z f).map_zsmul r g

Premises used: AddMonoidHom.map_zsmul, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
_X _Y Z : C
f : _X ⟶ _Y
r : ℤ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
exact (Preadditive.leftComp Z f).map_zsmul r g

Premises used: AddMonoidHom.map_zsmul, CategoryTheory.Preadditive.leftComp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : R
x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
h : ((x_3 • x_4) ≫ x_5).hom = (x_3 • x_4 ≫ x_5).hom
⊢ (x_3 • x_4) ≫ x_5 = x_3 • x_4 ≫ x_5

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : R
x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ ((x_3 • x_4) ≫ x_5).hom = (x_3 • x_4 ≫ x_5).hom

Tactic:
apply smul_comp

Premises used: CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : x ⟶ x_1
x_4 : R
x_5 : x_1 ⟶ x_2
h : (x_3 ≫ (x_4 • x_5)).hom = (x_4 • x_3 ≫ x_5).hom
⊢ x_3 ≫ (x_4 • x_5) = x_4 • x_3 ≫ x_5

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : x ⟶ x_1
x_4 : R
x_5 : x_1 ⟶ x_2
⊢ (x_3 ≫ (x_4 • x_5)).hom = (x_4 • x_3 ≫ x_5).hom

Tactic:
apply comp_smul

Premises used: CategoryTheory.Linear.comp_smul
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
X Y : InducedCategory C F
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (m : R) (x : X ⟶ Y),
    Equiv.toFun (AddEquiv.toEquiv InducedCategory.homAddEquiv) (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        (Equiv.toFun (AddEquiv.toEquiv InducedCategory.homAddEquiv) x)
⊢ ∀ (m : R) (x : X ⟶ Y),
    Equiv.toFun (AddEquiv.toEquiv InducedCategory.homAddEquiv) (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        (Equiv.toFun (AddEquiv.toEquiv InducedCategory.homAddEquiv) x)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (x y : Y ⟶ Z), f ≫ (x + y) = f ≫ x + f ≫ y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y Z : C
f : X ⟶ Y
⊢ ∀ (m : R) (x : Y ⟶ Z), f ≫ (m • x) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (f ≫ x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (x y : X ⟶ Y), (x + y) ≫ g = x ≫ g + y ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y Z : C
g : Y ⟶ Z
⊢ ∀ (m : R) (x : X ⟶ Y), (m • x) ≫ g = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (x ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y : C
f : X ⟶ Y
inst_4 : Epi f
r : R
inst_5 : Invertible r
Z : C
g g' : Y ⟶ Z
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ r • g = r • g'

Tactic:
rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H

Premises used: CategoryTheory.Linear.comp_smul, CategoryTheory.cancel_epi, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y : C
f : X ⟶ Y
inst_4 : Epi f
r : R
inst_5 : Invertible r
Z : C
g g' : Y ⟶ Z
H : r • g = r • g'
⊢ g = g'

Tactic:
simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H

Premises used: Invertible.invOf, smul_smul, congr_arg, HSMul.hSMul
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y : C
f : X ⟶ Y
inst_4 : Mono f
r : R
inst_5 : Invertible r
Z : C
g g' : Z ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ r • g = r • g'

Tactic:
rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Linear.comp_smul, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y : C
f : X ⟶ Y
inst_4 : Mono f
r : R
inst_5 : Invertible r
Z : C
g g' : Z ⟶ X
H : r • g = r • g'
⊢ g = g'

Tactic:
simpa [smul_smul] using congr_arg (fun f => ⅟r • f) H

Premises used: Invertible.invOf, smul_smul, congr_arg, HSMul.hSMul
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C_1
k : Type u_1
C : Type u_2
inst_4 : Category.{v_1, u_2} C
inst_5 : Semiring k
inst_6 : Preadditive.{v_1, u_2} C
inst_7 : Linear.{u_1, v_1, u_2} k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : X ⟶ W
⊢ (leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom : (a : Y ⟶ Z) → X ⟶ W)
      (AddHom.toFun (toAddHom (rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom)) x) =
    x

Tactic:
simp only [Iso.symm_hom, LinearMap.toFun_eq_coe, LinearMap.coe_comp, Function.comp_apply,
        leftComp_apply, rightComp_apply, Category.assoc, Iso.hom_inv_id, Category.comp_id,
        Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.leftComp_apply, CategoryTheory.Iso.symm_hom, LinearMap.toFun_eq_coe, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, LinearMap.coe_comp, CategoryTheory.Iso.hom_inv_id_assoc, Function.comp_apply, CategoryTheory.Linear.rightComp_apply
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C_1
k : Type u_1
C : Type u_2
inst_4 : Category.{v_1, u_2} C
inst_5 : Semiring k
inst_6 : Preadditive.{v_1, u_2} C
inst_7 : Linear.{u_1, v_1, u_2} k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : Y ⟶ Z
⊢ AddHom.toFun (toAddHom (rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom))
      ((leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom : (a : Y ⟶ Z) → X ⟶ W) x) =
    x

Tactic:
simp only [Iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, rightComp_apply,
        leftComp_apply, LinearMap.toFun_eq_coe, Iso.inv_hom_id_assoc, Category.assoc,
        Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Linear.leftComp_apply, CategoryTheory.Iso.symm_hom, LinearMap.toFun_eq_coe, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, LinearMap.coe_comp, Function.comp_apply, CategoryTheory.Linear.rightComp_apply
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
k : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Semiring k
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
f : X ⟶ W
⊢ (homCongr k f₁ f₂ : (a : X ⟶ W) → Y ⟶ Z) f = (f₁.inv ≫ f) ≫ f₂.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
k : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Semiring k
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
f : Y ⟶ Z
⊢ (LinearEquiv.symm (homCongr k f₁ f₂) : (a : Y ⟶ Z) → X ⟶ W) f = f₁.hom ≫ f ≫ f₂.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y Z : C
r : Rˣ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
apply Linear.smul_comp

Premises used: CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y Z : C
f : X ⟶ Y
r : Rˣ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
apply Linear.comp_smul

Premises used: CategoryTheory.Linear.comp_smul
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
S : Type w
inst_2 : CommSemiring S
inst_3 : Linear.{w, v, u} S C
X Y Z : C
x y : X ⟶ Y
h :
  ∀ (x_1 : Y ⟶ Z),
    Eq (α := X ⟶ Z) ((leftComp S Z (x + y) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
      ((HAdd.hAdd (α := (Y ⟶ Z) →ₗ[S] X ⟶ Z) (leftComp S Z x) (leftComp S Z y) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
⊢ leftComp S Z (x + y) = HAdd.hAdd (α := (Y ⟶ Z) →ₗ[S] X ⟶ Z) (leftComp S Z x) (leftComp S Z y)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
S : Type w
inst_2 : CommSemiring S
inst_3 : Linear.{w, v, u} S C
X Y Z : C
x y : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) ((leftComp S Z (x + y) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
    ((HAdd.hAdd (α := (Y ⟶ Z) →ₗ[S] X ⟶ Z) (leftComp S Z x) (leftComp S Z y) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
S : Type w
inst_2 : CommSemiring S
inst_3 : Linear.{w, v, u} S C
X Y Z : C
m : S
x : X ⟶ Y
h :
  ∀ (x_1 : Y ⟶ Z),
    Eq (α := X ⟶ Z) ((leftComp S Z (m • x) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
      ((HSMul.hSMul (α := S) (β := (Y ⟶ Z) →ₗ[S] X ⟶ Z) ((RingHom.id S : (a : S) → S) m : S) (leftComp S Z x) :
            (a : Y ⟶ Z) → X ⟶ Z)
          x_1 :
        X ⟶ Z)
⊢ leftComp S Z (m • x) =
    HSMul.hSMul (α := S) (β := (Y ⟶ Z) →ₗ[S] X ⟶ Z) ((RingHom.id S : (a : S) → S) m : S) (leftComp S Z x)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
S : Type w
inst_2 : CommSemiring S
inst_3 : Linear.{w, v, u} S C
X Y Z : C
m : S
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := X ⟶ Z) ((leftComp S Z (m • x) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
    ((HSMul.hSMul (α := S) (β := (Y ⟶ Z) →ₗ[S] X ⟶ Z) ((RingHom.id S : (a : S) → S) m : S) (leftComp S Z x) :
          (a : Y ⟶ Z) → X ⟶ Z)
        x_1 :
      X ⟶ Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r : R
α : F ⟶ G
X Y : C
f : X ⟶ Y
rw : r • F.map f ≫ α.app Y = (r • α.app X) ≫ G.map f
rw₁ : r • F.map f ≫ α.app Y = r • α.app X ≫ G.map f
rw₂ rw₃ : r • α.app X ≫ G.map f = r • α.app X ≫ G.map f
⊢ F.map f ≫ (r • α.app Y) = (r • α.app X) ≫ G.map f

Tactic:
rw [comp_smul, smul_comp, α.naturality]

Premises used: CategoryTheory.Linear.comp_smul, CategoryTheory.NatTrans.naturality, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
x y : R
b : F ⟶ G
w : ∀ (x_1 : C), ((x * y) • b).app x_1 = (x • y • b).app x_1
⊢ (x * y) • b = x • y • b

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
x y : R
b : F ⟶ G
x_1 : C
⊢ ((x * y) • b).app x_1 = (x • y • b).app x_1

Tactic:
apply mul_smul

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
b : F ⟶ G
w : ∀ (x : C), (HSMul.hSMul (α := R) 1 b).app x = b.app x
⊢ HSMul.hSMul (α := R) 1 b = b

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
b : F ⟶ G
x : C
⊢ (HSMul.hSMul (α := R) 1 b).app x = b.app x

Tactic:
apply one_smul

Premises used: one_smul
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
a : R
w : ∀ (x : C), (HSMul.hSMul (β := F ⟶ G) a 0).app x = NatTrans.app 0 x
⊢ HSMul.hSMul (β := F ⟶ G) a 0 = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
a : R
x : C
⊢ (HSMul.hSMul (β := F ⟶ G) a 0).app x = NatTrans.app 0 x

Tactic:
apply smul_zero

Premises used: smul_zero
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
a : R
x y : F ⟶ G
w : ∀ (x_1 : C), (a • (x + y)).app x_1 = (a • x + a • y).app x_1
⊢ a • (x + y) = a • x + a • y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
a : R
x y : F ⟶ G
x_1 : C
⊢ (a • (x + y)).app x_1 = (a • x + a • y).app x_1

Tactic:
apply smul_add

Premises used: smul_add
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r s : R
x : F ⟶ G
w : ∀ (x_1 : C), ((r + s) • x).app x_1 = (r • x + s • x).app x_1
⊢ (r + s) • x = r • x + s • x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r s : R
x : F ⟶ G
x_1 : C
⊢ ((r + s) • x).app x_1 = (r • x + s • x).app x_1

Tactic:
apply add_smul

Premises used: add_smul
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
x : F ⟶ G
w : ∀ (x_1 : C), (HSMul.hSMul (α := R) 0 x).app x_1 = NatTrans.app 0 x_1
⊢ HSMul.hSMul (α := R) 0 x = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
x : F ⟶ G
x_1 : C
⊢ (HSMul.hSMul (α := R) 0 x).app x_1 = NatTrans.app 0 x_1

Tactic:
apply zero_smul

Premises used: zero_smul
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
X Y Z : Functor.{v_1, v_2, u_2, u_3} C D
r : R
f : X ⟶ Y
g : Y ⟶ Z
w : ∀ (x : C), ((r • f) ≫ g).app x = (r • f ≫ g).app x
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
X Y Z : Functor.{v_1, v_2, u_2, u_3} C D
r : R
f : X ⟶ Y
g : Y ⟶ Z
x : C
⊢ ((r • f) ≫ g).app x = (r • f ≫ g).app x

Tactic:
apply smul_comp

Premises used: CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
X Y Z : Functor.{v_1, v_2, u_2, u_3} C D
f : X ⟶ Y
r : R
g : Y ⟶ Z
w : ∀ (x : C), (f ≫ (r • g)).app x = (r • f ≫ g).app x
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
X Y Z : Functor.{v_1, v_2, u_2, u_3} C D
f : X ⟶ Y
r : R
g : Y ⟶ Z
x : C
⊢ (f ≫ (r • g)).app x = (r • f ≫ g).app x

Tactic:
apply comp_smul

Premises used: CategoryTheory.Linear.comp_smul
-- Module: Mathlib.CategoryTheory.Linear.FunctorCategory
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
X : C
r : R
α : F ⟶ G
⊢ (r • α).app X = r • α.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
mp :
  Linear R F →
    ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
mpr :
  (∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))) →
    Linear R F
⊢ Linear R F ↔
    ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : Linear R F
X : C
r : R
mp : r • F.map (𝟙 X) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
mp₁ mp₂ : HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
⊢ F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))

Tactic:
rw [h.map_smul, F.map_id]

Premises used: CategoryTheory.Functor.Linear.map_smul, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
⊢ (∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))) →
    Linear R F

Tactic:
fun h => ⟨fun {X Y} f r => ?_⟩

Premises used: CategoryTheory.Functor.Linear.mk
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
mpr :
  ∀
    (h :
      ∀ (X : C) (r : R),
        F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)))
    {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f
⊢ (∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))) →
    Linear R F

Tactic:
refine fun h => ⟨fun {X Y} f r => ?_⟩