awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F : Functor.{v, v, u, u} C D
X Y : Free R C
f : X ⟶ Y
r : R
⊢ ∀ (i : X ⟶ Y), HSMul.hSMul.{u_1, v, v} (α := R) 0 (F.map i) = 0

Tactic:
simp [Finsupp.smul_sum, mul_smul]

Premises used: Finsupp.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F 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
⊢ Eq (α := F.obj X ⟶ G.obj Y)
    (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)))
    (CategoryStruct.comp (Y := G.obj X) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X)) (G.map 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F 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₂)
add₅ 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₂)
⊢ 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₂)

Tactic:
rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F 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
single : r • F.map (Finsupp.single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (Finsupp.single f' 1)
⊢ F.map (Finsupp.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 (Finsupp.single f' r)

Tactic:
rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]

Premises used: CategoryTheory.Functor.map_smul, CategoryTheory.Iso.app_hom, CategoryTheory.Linear.comp_smul, Finsupp.smul_single_one, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F 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
single : r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
⊢ r • F.map (Finsupp.single f' 1) ≫ α.hom.app Y = r • α.hom.app X ≫ G.map (Finsupp.single f' 1)

Tactic:
change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'

Premises used: CategoryTheory.Free.embedding, CategoryTheory.Functor.comp, CategoryTheory.Functor.map
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F 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
single single₁ : r • α.hom.app X ≫ (embedding R C ⋙ G).map f' = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'
⊢ r • (embedding R C ⋙ F).map f' ≫ α.hom.app Y = r • α.hom.app X ≫ (embedding R C ⋙ G).map f'

Tactic:
rw [α.hom.naturality f']

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u_1
inst : CommRing R
C : Type u
inst_1 : Category.{v, u} C
D : Type u
inst_2 : Category.{v, u} D
inst_3 : Preadditive.{v, u} D
inst_4 : Linear.{u_1, v, u} R D
F 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
zero :
  Eq (α := F.obj X ⟶ G.obj Y)
    (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (Iso.hom ((fun (X : Free R C) ↦ α.app X) Y)))
    (CategoryStruct.comp (Y := G.obj X) (Iso.hom ((fun (X : Free R C) ↦ α.app X) X)) (G.map 0))
add :
  ∀ (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₂)
single :
  ∀ (f' : X ⟶ Y) (r : R),
    F.map (Finsupp.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 (Finsupp.single f' r)
⊢ 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

Tactic:
induction f using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [Functor.map_add, add_comp, w₁, w₂, Functor.map_add, comp_add]
      | single f' r =>
        rw [Iso.app_hom, Iso.app_hom, ← smul_single_one, F.map_smul, G.map_smul, smul_comp,
          comp_smul]
        change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f'
        rw [α.hom.naturality f']

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.Functor.map_smul, CategoryTheory.Iso.app_hom, CategoryTheory.Linear.comp_smul, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, Finsupp.smul_single_one, CategoryTheory.Linear.smul_comp, Finsupp.single
-- Module: Mathlib.Algebra.Category.ModuleCat.Algebra
Goal:
k : Type u
inst : Field k
A : Type w
inst_1 : Ring A
inst_2 : Algebra k A
M : ModuleCat.{v, w} A
⊢ IsScalarTower.{u, w, v} k A (↑M : Type v)

Tactic:
IsScalarTower.restrictScalars k A M

Premises used: ModuleCat.carrier, IsScalarTower.restrictScalars
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X : Type v
inst_1 : Ring X
inst_2 : Module R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X : Type v
inst_1 : Ring X
inst_2 : Module R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X : Type v
inst_1 : Ring X
inst_2 : Module R X
⊢ (↑(of R X) : Type v) = X

Tactic:
with_reducible rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
⊢ of R (↑M : Type v) = M

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
⊢ of R (↑M : Type v) = M

Tactic:
with_reducible rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
⊢ Hom.hom (𝟙 M) = LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
x : (↑M : Type v)
⊢ (@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          carrier
          (fun (X Y : ModuleCat.{v, u} R) ↦
            (LinearMap.instFunLike : FunLike ((↑X : Type v) →ₗ[R] (↑Y : Type v)) (↑X : Type v) (↑Y : Type v)))
          _ _ _ (𝟙 M : M ⟶ M) :
        (a : (↑M : Type v)) → (↑M : Type v))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N O : ModuleCat.{v, u} R
f : M ⟶ N
g : N ⟶ O
⊢ Hom.hom (f ≫ g) = Hom.hom g ∘ₗ Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N O : ModuleCat.{v, u} R
f : M ⟶ N
g : N ⟶ O
x : (↑M : Type v)
⊢ Eq (α := (↑O : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (f ≫ g) :
          (a : (↑M : Type v)) → (↑O : Type v))
        x :
      (↑O : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) g :
          (a : (↑N : Type v)) → (↑O : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) f :
              (a : (↑M : Type v)) → (↑N : Type v))
            x :
          (↑N : Type v)) :
      (↑O : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f g : M ⟶ N
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: ModuleCat.Hom.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f g : M.Hom N
h : f.hom = g.hom
_private :
  ∀ (hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = g.hom),
    { hom' := hom' : M.Hom N } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
g : M.Hom N
hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)
h : { hom' := hom' : M.Hom N }.hom = g.hom
_private :
  ∀ (hom'_1 : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = { hom' := hom'_1 }.hom),
    { hom' := hom' : M.Hom N } = { hom' := hom'_1 }
⊢ { hom' := hom' : M.Hom N } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
hom' hom'_1 : (↑M : Type v) →ₗ[R] (↑N : Type v)
h : { hom' := hom' : M.Hom N }.hom = { hom' := hom'_1 }.hom
⊢ { hom' := hom' : M.Hom N } = { hom' := hom'_1 }

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Function.Injective.{v + 1, v + 1} (α := M.Hom N) Hom.hom

Tactic:
hom_bijective.injective

Premises used: Function.Bijective.injective, ModuleCat.hom_bijective
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Function.Surjective.{v + 1, v + 1} (α := M.Hom N) Hom.hom

Tactic:
hom_bijective.surjective

Premises used: Function.Bijective.surjective, ModuleCat.hom_bijective
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X Y : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : AddCommGroup Y
inst_4 : Module R Y
f : X →ₗ[R] Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Quiver.Hom (V := ModuleCat.{v, u} R) (of R M) (of R M)) (ofHom LinearMap.id) (𝟙 (of R M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N O : Type v
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup O
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R O
f : M →ₗ[R] N
g : N →ₗ[R] O
⊢ ofHom (g ∘ₗ f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : Type v
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
x : M
⊢ Eq (α := (↑(of R N) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (ofHom f) :
          (a : (↑(of R M) : Type v)) → (↑(of R N) : Type v))
        x :
      (↑(of R N) : Type v))
    ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
e : M ≅ N
x : (↑M : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          e.inv :
        (a : (↑N : Type v)) → (↑M : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) e.hom :
            (a : (↑M : Type v)) → (↑N : Type v))
          x :
        (↑N : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
e : M ≅ N
x : (↑N : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          e.hom :
        (a : (↑M : Type v)) → (↑N : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) e.inv :
            (a : (↑N : Type v)) → (↑M : Type v))
          x :
        (↑M : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
⊢ Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      M =
    (↑M : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ Eq (α :=
    (a :
        (fun (X : Type v) ↦ X)
          (Functor.obj
            (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier))
            M)) →
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
            (CC := carrier))
          N))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
              (CC := carrier))
            f)) :
      (a : (fun (X : Type v) ↦ X) ((forget (ModuleCat R)).obj M)) →
        (fun (X : Type v) ↦ X) ((forget (ModuleCat R)).obj N))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
          carrier) f) :
      (a : (↑M : Type v)) → (↑N : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X : ModuleCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (ModuleCat.{u_1, u} R) (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
        (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommGrpCat (FD :=
        fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommGrpCat.carrier))
      X =
    AddCommGrpCat.of (↑X : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
⊢ Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      (of R X) =
    AddCommGrpCat.of X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X Y : ModuleCat.{u_1, u} R
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj
        (forget₂ (ModuleCat.{u_1, u} R) (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
          (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommGrpCat (FD :=
          fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommGrpCat.carrier))
        X ⟶
      Functor.obj
        (forget₂ (ModuleCat.{u_1, u} R) (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
          (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommGrpCat (FD :=
          fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommGrpCat.carrier))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{u_1, u} R) (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
        (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommGrpCat (FD :=
        fun (x1 x2 : AddCommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommGrpCat.carrier))
      f)
    (AddCommGrpCat.ofHom (↑(Hom.hom f) : (↑X : Type u_1) →+ (↑Y : Type u_1)))

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X : ModuleCat.{u_1, u} R
⊢ of R (↑X : Type u_1) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : M ⟶ X
hf :
  ∀ (x : (↑M : Type u_1)),
    Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
      ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : M ⟶ X
x : (↑M : Type u_1)
hf :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
rw [Subsingleton.elim x (0 : M)]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : M ⟶ X
x : (↑M : Type u_1)
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : X ⟶ M
hf :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑M : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
      ((Hom.hom default : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : ModuleCat.{u_1, u} R
f : X ⟶ M
x : (↑X : Type u_1)
⊢ Eq (α := (↑M : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
⊢ HasZeroObject (ModuleCat.{v, u} R)

Tactic:
⟨⟨of R PUnit, isZero_of_subsingleton _⟩⟩

Premises used: CategoryTheory.Limits.HasZeroObject.mk, ModuleCat.of, PUnit, Exists.intro, ModuleCat.isZero_of_subsingleton
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
hf :
  ∀ (x : (↑(of R X₁) : Type v)),
    Eq (α := (↑(of R X₁) : Type v))
      ((Hom.hom (↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v))
          x :
        (↑(of R X₁) : Type v))
      ((Hom.hom (𝟙 (of R X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v)) x : (↑(of R X₁) : Type v))
⊢ ↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁) = 𝟙 (of R X₁)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x : (↑(of R X₁) : Type v)
⊢ Eq (α := (↑(of R X₁) : Type v))
    ((Hom.hom (↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v))
        x :
      (↑(of R X₁) : Type v))
    ((Hom.hom (𝟙 (of R X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v)) x : (↑(of R X₁) : Type v))

Tactic:
apply e.left_inv

Premises used: LinearEquiv.left_inv
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
hf :
  ∀ (x : (↑(of R X₂) : Type v)),
    Eq (α := (↑(of R X₂) : Type v))
      ((Hom.hom (↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v))
          x :
        (↑(of R X₂) : Type v))
      ((Hom.hom (𝟙 (of R X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v)) x : (↑(of R X₂) : Type v))
⊢ ↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂) = 𝟙 (of R X₂)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x : (↑(of R X₂) : Type v)
⊢ Eq (α := (↑(of R X₂) : Type v))
    ((Hom.hom (↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v))
        x :
      (↑(of R X₂) : Type v))
    ((Hom.hom (𝟙 (of R X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v)) x : (↑(of R X₂) : Type v))

Tactic:
apply e.right_inv

Premises used: LinearEquiv.right_inv