awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.AB
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
X Y : ModuleCat.{v, u} R
f g : X ⟶ Y
h :
  ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R),
    Eq (α := (↑Y : Type v))
      ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
      ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
hf :
  ∀ (x : (↑X : Type v)),
    Eq (α := (↑Y : Type v)) ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
      ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.AB
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
X Y : ModuleCat.{v, u} R
f g : X ⟶ Y
h :
  ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R),
    Eq (α := (↑Y : Type v))
      ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
      ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
x : (↑X : Type v)
⊢ Eq (α := (↑Y : Type v)) ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))
    ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v)) x : (↑Y : Type v))

Tactic:
simpa using h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp
    (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1

Premises used: LinearMap.comp, LinearEquiv.toLinearMap, ModuleCat.carrier, Shrink.linearEquiv, ModuleCat.ofHom, OfNat.ofNat, LinearMap.toSpanSingleton
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
hf : Mono f
hf₁ :
  ∀ (x : (↑(of R (↑M : Type v)) : Type v)),
    Eq (α := (↑N : Type v))
      ((Hom.hom
              ((LinearEquiv.toModuleIso
                    (((Hom.hom f).ker.quotEquivOfEqBot ⋯).symm ≪≫ₗ
                      ((Hom.hom f).quotKerEquivRange ≪≫ₗ
                        LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker ⋯))).hom ≫
                Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ))) :
            (a : (↑(of R (↑M : Type v)) : Type v)) → (↑N : Type v))
          x :
        (↑N : Type v))
      ((Hom.hom f : (a : (↑(of R (↑M : Type v)) : Type v)) → (↑N : Type v)) x : (↑N : Type v))
⊢ (LinearEquiv.toModuleIso
          (((Hom.hom f).ker.quotEquivOfEqBot ⋯).symm ≪≫ₗ
            ((Hom.hom f).quotKerEquivRange ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker ⋯))).hom ≫
      Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ)) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
hf : Mono f
x : (↑(of R (↑M : Type v)) : Type v)
⊢ Eq (α := (↑N : Type v))
    ((Hom.hom
            ((LinearEquiv.toModuleIso
                  (((Hom.hom f).ker.quotEquivOfEqBot ⋯).symm ≪≫ₗ
                    ((Hom.hom f).quotKerEquivRange ≪≫ₗ
                      LinearEquiv.ofEq (Hom.hom f).range (Hom.hom (↟(Hom.hom f).range.mkQ)).ker ⋯))).hom ≫
              Fork.ι (kernelCone (↟(Hom.hom f).range.mkQ))) :
          (a : (↑(of R (↑M : Type v)) : Type v)) → (↑N : Type v))
        x :
      (↑N : Type v))
    ((Hom.hom f : (a : (↑(of R (↑M : Type v)) : Type v)) → (↑N : Type v)) x : (↑N : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
hf : Epi f
hf₁ :
  ∀ (x : (↑M : Type v)),
    Eq (α := (↑(of R (↑N : Type v)) : Type v))
      ((Hom.hom
              (Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
                (LinearEquiv.toModuleIso
                    ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker ⋯ ≪≫ₗ
                        (Hom.hom f).quotKerEquivRange ≪≫ₗ
                      LinearEquiv.ofTop (Hom.hom f).range ⋯)).hom) :
            (a : (↑M : Type v)) → (↑(of R (↑N : Type v)) : Type v))
          x :
        (↑(of R (↑N : Type v)) : Type v))
      ((Hom.hom f : (a : (↑M : Type v)) → (↑(of R (↑N : Type v)) : Type v)) x : (↑(of R (↑N : Type v)) : Type v))
⊢ Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
      (LinearEquiv.toModuleIso
          ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker ⋯ ≪≫ₗ
              (Hom.hom f).quotKerEquivRange ≪≫ₗ
            LinearEquiv.ofTop (Hom.hom f).range ⋯)).hom =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
hf : Epi f
x : (↑M : Type v)
⊢ Eq (α := (↑(of R (↑N : Type v)) : Type v))
    ((Hom.hom
            (Cofork.π (cokernelCocone (↟(Hom.hom f).ker.subtype)) ≫
              (LinearEquiv.toModuleIso
                  ((Hom.hom (↟(Hom.hom f).ker.subtype)).range.quotEquivOfEq (Hom.hom f).ker ⋯ ≪≫ₗ
                      (Hom.hom f).quotKerEquivRange ≪≫ₗ
                    LinearEquiv.ofTop (Hom.hom f).range ⋯)).hom) :
          (a : (↑M : Type v)) → (↑(of R (↑N : Type v)) : Type v))
        x :
      (↑(of R (↑N : Type v)) : Type v))
    ((Hom.hom f : (a : (↑M : Type v)) → (↑(of R (↑N : Type v)) : Type v)) x : (↑(of R (↑N : Type v)) : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ HasLimitsOfSize.{v, v, max v w, max (max (v + 1) (w + 1)) u} (ModuleCat R)

Tactic:
ModuleCat.hasLimitsOfSize.{v, v, max v w}

Premises used: ModuleCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ ReflectsLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)}
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w))) (CC :=
      carrier))

Tactic:
reflectsLimits_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ ReflectsLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)}
    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max v w)) →ₗ[R] (↑x2 : Type (max v w)))
      (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat) ↦
      (↑x1 : Type (max v w)) →+ (↑x2 : Type (max v w))) (CD := AddCommGrpCat.carrier))

Tactic:
reflectsLimits_of_reflectsIsomorphisms

Premises used: CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ ReflectsLimits
    (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
      carrier))

Tactic:
ModuleCat.forget_reflectsLimitsOfSize.{v, v}

Premises used: ModuleCat.forget_reflectsLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Abelian
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
f : M ⟶ N
⊢ ReflectsLimits
    (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))

Tactic:
ModuleCat.forget₂_reflectsLimitsOfSize.{v, v}

Premises used: ModuleCat.forget₂_reflectsLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f g : Functor.obj (free R) X ⟶ M
h :
  ∀ (x : X),
    Eq (α := (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
          (freeMk x) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) g :
            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
          (freeMk x) :
        (↑M : Type u))
⊢ f = g

Tactic:
ModuleCat.hom_ext (Finsupp.lhom_ext' (fun x ↦ LinearMap.ext_ring (h x)))

Premises used: Finsupp.lhom_ext', LinearMap.ext_ring, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
dsimp :
  Eq (α := (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (Y := M)
            (↟((Finsupp.lift (↑M : Type u) R X : (a : X → (↑M : Type u)) → (X →₀ R) →ₗ[R] (↑M : Type u))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → (↑M : Type u)))) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u))
⊢ Eq (α := (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (freeDesc f) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))
        x :
      (fun (X : Type u) ↦ X) (↑M : Type u))

Tactic:
dsimp [freeDesc]

Premises used: ModuleCat.freeDesc
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
erw :
  HSMul.hSMul (α := R) (β := (↑M : Type u)) 1
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x
erw₁ :
  HSMul.hSMul (α := R) (β := (↑M : Type u)) 0
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
    0
⊢ Eq (α := (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (Y := M)
            (↟((Finsupp.lift (↑M : Type u) R X : (a : X → (↑M : Type u)) → (X →₀ R) →ₗ[R] (↑M : Type u))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → (↑M : Type u)))) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u))

Tactic:
erw [Finsupp.lift_apply, Finsupp.sum_single_index]

Premises used: Finsupp.sum_single_index, Finsupp.lift_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
⊢ HSMul.hSMul (α := R) (β := (↑M : Type u)) 1
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ (↑M : Type u)
x : X
⊢ HSMul.hSMul (α := R) (β := (↑M : Type u)) 0
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → (↑M : Type u)) x : (↑M : Type u)) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X Y : Type u
f : X ⟶ Y
x : X
⊢ Eq (α := (↑(Functor.obj (free R) Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (CategoryTheory.Functor.map (free R) f) :
          (a : (↑((free R).obj X) : Type u)) → (↑((free R).obj Y) : Type u))
        (freeMk x) :
      (↑(Functor.obj (free R) Y) : Type u))
    (freeMk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) x) :
      (↑(Functor.obj (free R) ((fun (X : Type u) ↦ X) Y)) : Type u))

Tactic:
apply Finsupp.mapDomain_single

Premises used: Finsupp.mapDomain_single
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
x : Functor.obj (free R) X ⟶ M
h :
  ∀ (x_1 : X),
    Eq (α := (↑M : Type u))
      ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
              carrier _ _ (Functor.obj (free R) X) M
              ((fun (ψ : X ⟶ (↑M : Type u)) ↦
                  (freeDesc
                      (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
                    Functor.obj (free R) X ⟶ M))
                ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
                    (↾fun (x : X) ↦
                        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                              (CC := carrier) φ :
                            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                          (freeMk x) :
                      X ⟶ (↑M : Type u)))
                  x)) :
            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
          (freeMk x_1) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) x :
            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
          (freeMk x_1) :
        (↑M : Type u))
⊢ (fun (ψ : X ⟶ (↑M : Type u)) ↦
        (freeDesc
            (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
          Functor.obj (free R) X ⟶ M))
      ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
          (↾fun (x : X) ↦
              (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                    carrier) φ :
                  (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                (freeMk x) :
            X ⟶ (↑M : Type u)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
x : Functor.obj (free R) X ⟶ M
x_1 : X
⊢ Eq (α := (↑M : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (Functor.obj (free R) X) M
            ((fun (ψ : X ⟶ (↑M : Type u)) ↦
                (freeDesc
                    (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
                  Functor.obj (free R) X ⟶ M))
              ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
                  (↾fun (x : X) ↦
                      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                            (CC := carrier) φ :
                          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                        (freeMk x) :
                    X ⟶ (↑M : Type u)))
                x)) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x_1) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) x :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x_1) :
      (↑M : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
x : X ⟶ (↑M : Type u)
h :
  ∀ (x_1 : X),
    TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
              (↾fun (x : X) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                        carrier) φ :
                      (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                    (freeMk x) :
                X ⟶ (↑M : Type u)))
            ((fun (ψ : X ⟶ (↑M : Type u)) ↦
                (freeDesc
                    (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
                  Functor.obj (free R) X ⟶ M))
              x)))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) x).toFun x_1
⊢ (fun (φ : Functor.obj (free R) X ⟶ M) ↦
        (↾fun (x : X) ↦
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  carrier) φ :
                (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
              (freeMk x) :
          X ⟶ (↑M : Type u)))
      ((fun (ψ : X ⟶ (↑M : Type u)) ↦
          (freeDesc
              (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
            Functor.obj (free R) X ⟶ M))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
x : X ⟶ (↑M : Type u)
x_1 : X
⊢ TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (φ : Functor.obj (free R) X ⟶ M) ↦
            (↾fun (x : X) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                      carrier) φ :
                    (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
                  (freeMk x) :
              X ⟶ (↑M : Type u)))
          ((fun (ψ : X ⟶ (↑M : Type u)) ↦
              (freeDesc
                  (↾(⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ψ) :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (↑M : Type u))) :
                Functor.obj (free R) X ⟶ M))
            x)))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) x).toFun x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g :
  Y ⟶
    Functor.obj
      (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)) M
h :
  ∀ (x : X),
    Eq (α := (↑M : Type u))
      ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
              carrier _ _ (Functor.obj (free R) X) M
              ((Equiv.symm freeHomEquiv : (a : X ⟶ (forget (ModuleCat R)).obj M) → (free R).obj X ⟶ M) (f ≫ g)) :
            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
          (freeMk x) :
        (↑M : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              (X := Functor.obj (free R) X) (Y := M)
              (CategoryTheory.Functor.map (free R) f ≫
                (Equiv.symm freeHomEquiv : (a : Y ⟶ (forget (ModuleCat R)).obj M) → (free R).obj Y ⟶ M) g) :
            (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
          (freeMk x) :
        (↑M : Type u))
⊢ Eq (α := Functor.obj (free R) X ⟶ M)
    ((Equiv.symm freeHomEquiv : (a : X ⟶ (forget (ModuleCat R)).obj M) → (free R).obj X ⟶ M) (f ≫ g) :
      Functor.obj (free R) X ⟶ M)
    (CategoryTheory.Functor.map (free R) f ≫
        (Equiv.symm freeHomEquiv : (a : Y ⟶ (forget (ModuleCat R)).obj M) → (free R).obj Y ⟶ M) g :
      Functor.obj (free R) X ⟶ M)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X Y : Type u
M : ModuleCat R
f : X ⟶ Y
g :
  Y ⟶
    Functor.obj
      (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)) M
x : X
⊢ Eq (α := (↑M : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (Functor.obj (free R) X) M
            ((Equiv.symm freeHomEquiv : (a : X ⟶ (forget (ModuleCat R)).obj M) → (free R).obj X ⟶ M) (f ≫ g)) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            Functor.obj (free R) X) (Y := M)
            (CategoryTheory.Functor.map (free R) f ≫
              (Equiv.symm freeHomEquiv : (a : Y ⟶ (forget (ModuleCat R)).obj M) → (free R).obj Y ⟶ M) g) :
          (a : (↑((free R).obj X) : Type u)) → (↑M : Type u))
        (freeMk x) :
      (↑M : Type u))

Tactic:
simp [freeHomEquiv]

Premises used: ModuleCat.freeHomEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
X : Type u
M : ModuleCat R
⊢ Adjunction.homEquiv (adj R) X M = freeHomEquiv

Tactic:
simp only [adj, Adjunction.mkOfHomEquiv_homEquiv]

Premises used: ModuleCat.adj, CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : Ring R
⊢ Functor.IsRightAdjoint
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier))

Tactic:
(adj R).isRightAdjoint

Premises used: ModuleCat.adj, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
hf :
  Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    ((Hom.hom (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit)) : (a : R) → (↑(𝟙_ (ModuleCat R)) : Type u))
        1 :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (((Hom.hom (𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) :
            (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
              (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
          (a : R) → (↑(𝟙_ (ModuleCat R)) : Type u))
        1 :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))
      ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))
    (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit)) (𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions
Goal:
R : Type u
inst : CommRing R
⊢ Eq (α := (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    ((Hom.hom (↟(Finsupp.lsingle PUnit.unit) ≫ ↟(Finsupp.lapply PUnit.unit)) : (a : R) → (↑(𝟙_ (ModuleCat R)) : Type u))
        1 :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))
    (((Hom.hom (𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) :
            (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
              (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)) :
          (a : R) → (↑(𝟙_ (ModuleCat R)) : Type u))
        1 :
      (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))

Tactic:
simp [free]

Premises used: ModuleCat.free