awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
f : M ⟶ N
⊢ Eq (α :=
    (a :
        (fun (X : Type v) ↦ X)
          (Functor.obj
            (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
              (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
            M)) →
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
            (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
          N))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
              (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
            f)) :
      (a : (fun (X : Type v) ↦ X) ((forget (SemimoduleCat R)).obj M)) →
        (fun (X : Type v) ↦ X) ((forget (SemimoduleCat R)).obj N))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat.{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.Semi
Goal:
R : Type u
inst : Semiring R
X : SemimoduleCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (SemimoduleCat.{u_1, u} R) (FC := fun (x1 x2 : SemimoduleCat.{u_1, u} R) ↦
        (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) AddCommMonCat (FD :=
        fun (x1 x2 : AddCommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →+ (↑x2 : Type u_1)) (CD := AddCommMonCat.carrier))
      X =
    AddCommMonCat.of (↑X : Type u_1)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{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.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{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.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{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.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{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.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{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.Semi
Goal:
R : Type u
inst : Semiring R
⊢ HasZeroObject (SemimoduleCat.{v, u} R)

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

Premises used: CategoryTheory.Limits.HasZeroObject.mk, SemimoduleCat.isZero_of_subsingleton, PUnit, SemimoduleCat.of, Exists.intro
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid 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.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid 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.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid 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.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid 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
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
X Y : SemimoduleCat.{u_1, u} R
i : X ≅ Y
⊢ Hom.hom i.hom ∘ₗ Hom.hom i.inv = LinearMap.id

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
X Y : SemimoduleCat.{u_1, u} R
i : X ≅ Y
⊢ Hom.hom i.inv ∘ₗ Hom.hom i.hom = LinearMap.id

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
f g : M ⟶ N
⊢ Hom.hom (f + g) = Hom.hom f + Hom.hom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
⊢ Eq.{v + 1} (α := (↑M : Type v) →ₗ[R] (↑N : Type v)) (Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
n : ℕ
f : M ⟶ N
⊢ Hom.hom (n • f) = n • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
ι : Type u_1
f : ι → (M ⟶ N)
s : Finset ι
⊢ Eq.{v + 1} (α := (↑M : Type v) →ₗ[R] (↑N : Type v)) (Hom.hom (∑ i ∈ s, f i)) (∑ i ∈ s, Hom.hom (f i))

Tactic:
map_sum ({ toFun := SemimoduleCat.Hom.hom, map_zero' := SemimoduleCat.hom_zero,
             map_add' := hom_add } : (M ⟶ N) →+ (M →ₗ[R] N)) _ _

Premises used: AddMonoidHom.mk, map_sum, ZeroHom.mk, SemimoduleCat.hom_zero, SemimoduleCat.Hom.hom, SemimoduleCat.hom_add
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
h : IsZero M
⊢ Subsingleton.{v + 1} (↑M : Type v)

Tactic:
subsingleton_of_forall_eq 0 (fun x ↦ ?_)

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
h : IsZero M
refine : ∀ (x : (↑M : Type v)), x = 0
⊢ Subsingleton.{v + 1} (↑M : Type v)

Tactic:
refine subsingleton_of_forall_eq 0 (fun x ↦ ?_)

Premises used: subsingleton_of_forall_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
h : IsZero M
x : (↑M : Type v)
rw :
  Eq (α := (↑M : Type v)) ((Hom.hom (𝟙 M) : (a : (↑M : Type v)) → (↑M : Type v)) x : (↑M : Type v)) (0 : (↑M : Type v))
⊢ x = 0

Tactic:
rw [← LinearMap.id_apply (R := R) x, ← SemimoduleCat.hom_id]

Premises used: LinearMap.id_apply, SemimoduleCat.hom_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
h : IsZero M
x : (↑M : Type v)
⊢ Eq (α := (↑M : Type v)) ((Hom.hom (𝟙 M) : (a : (↑M : Type v)) → (↑M : Type v)) x : (↑M : Type v)) (0 : (↑M : Type v))

Tactic:
simp only [(CategoryTheory.Limits.IsZero.iff_id_eq_zero M).mp h, hom_zero, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, SemimoduleCat.hom_zero, Iff.mp, CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsZero (C := SemimoduleCat.{u_1, u} R) (of R M) ↔ Subsingleton M

Tactic:
isZero_iff_subsingleton

Premises used: SemimoduleCat.isZero_iff_subsingleton
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
S : Type u_1
inst_1 : Monoid S
inst_2 : DistribMulAction.{u_1, v} S (↑N : Type v)
inst_3 : SMulCommClass.{u, u_1, v} R S (↑N : Type v)
s : S
f : M ⟶ N
⊢ Hom.hom (s • f) = s • Hom.hom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
x : S₀
x_1 : S
x_2 : (↑M : Type v)
rw : HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) x : S) (x_1 • x_2) = x • x_1 • x_2
⊢ (x • x_1) • x_2 = x • x_1 • x_2

Tactic:
rw [Algebra.smul_def, mul_smul]

Premises used: Algebra.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
x : S₀
x_1 : S
x_2 : (↑M : Type v)
⊢ HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) x : S) (x_1 • x_2) = x • x_1 • x_2

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₁ :
  HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₂ :
  HMul.hMul (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) s • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₃ rw₄ :
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n) =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)

Tactic:
rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]

Premises used: smul_assoc, smul_eq_mul, SemigroupAction.mul_smul, Algebra.commutes
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
S : Type u
inst : CommSemiring S
X Y X' Y' : SemimoduleCat.{v, u} S
i : X ≅ X'
j : Y ≅ Y'
f : X ⟶ Y
⊢ Eq (α := X' ⟶ Y') ((i.homCongr j : (a : X ⟶ Y) → X' ⟶ Y') f : X' ⟶ Y')
    ({
        hom' :=
          (i.toLinearEquivₛ.arrowCongr j.toLinearEquivₛ :
              (a : (↑X : Type v) →ₗ[S] (↑Y : Type v)) → (↑X' : Type v) →ₗ[S] (↑Y' : Type v))
            (Hom.hom f) } :
      X'.Hom Y')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
S : Type u
inst : CommSemiring S
X X' : SemimoduleCat.{v, u} S
i : X ≅ X'
f : End X
⊢ Eq (α := End X') ((i.conj : (a : End X) → End X') f : End X')
    ({ hom' := (i.toLinearEquivₛ.conj : (a : Module.End S (↑X : Type v)) → Module.End S (↑X' : Type v)) (Hom.hom f) } :
      X'.Hom X')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
A B : SemimoduleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f)
change :
  IsIso (X :=
    Functor.obj
      (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommMonCat.carrier))
      (Functor.obj
        (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
          (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
        A))
    (CategoryTheory.Functor.map
      (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommMonCat.carrier))
      (CategoryTheory.Functor.map
        (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
          (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
        f))
⊢ IsIso (X :=
    Functor.obj
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      f)

Tactic:
change IsIso ((forget _).map ((forget₂ _ AddCommMonCat).map f))

Premises used: CategoryTheory.IsIso, AddCommMonCat, CategoryTheory.Functor.map, CategoryTheory.forget₂, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
A B : SemimoduleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f)
⊢ IsIso (X :=
    Functor.obj
      (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommMonCat.carrier))
      (Functor.obj
        (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
          (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
        A))
    (CategoryTheory.Functor.map
      (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommMonCat.carrier))
      (CategoryTheory.Functor.map
        (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
          (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
        f))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
A B : SemimoduleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f)
⊢ IsIso (X :=
    Functor.obj
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      f)

Tactic:
have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommMonCat).map f))
      infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
A B : SemimoduleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f)
this :
  IsIso (X :=
    Functor.obj
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (forget _)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u_1
inst : CommSemiring R
M N P : SemimoduleCat.{u, u_1} R
f : (↑M : Type u) →ₗ[R] (↑N : Type u) →ₗ[R] (↑P : Type u)
⊢ hom₂ (ofHom₂ f) = f

Tactic:
rfl

Premises used: SemimoduleCat.Hom.hom₂, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u_1
inst : CommSemiring R
M N P : SemimoduleCat.{u, u_1} R
f : M ⟶ of R (N ⟶ P)
⊢ ofHom₂ (Hom.hom₂ f) = f

Tactic:
rfl

Premises used: SemimoduleCat.ofHom₂, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u_1
inst : Semiring R
G : SemimoduleCat.{u, u_1} R
H : Type u
inst_1 : AddCommMonoid H
inst_2 : Module R H
f : (↑G : Type u) →ₗ[R] H
⊢ f ∘ₗ Hom.hom (𝟙 G) = f

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Semi
Goal:
R : Type u_1
inst : Semiring R
G : Type u
inst_1 : AddCommMonoid G
inst_2 : Module R G
H : SemimoduleCat.{u, u_1} R
f : G →ₗ[R] (↑H : Type u)
⊢ Hom.hom (𝟙 H) ∘ₗ f = f

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
inst_1 : HasSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
adj : PresheafOfModules.sheafification (𝟙 (R.obj (P := Presheaf.IsSheaf J))) ⊣
  forget R ⋙ PresheafOfModules.restrictScalars (𝟙 (R.obj (P := Presheaf.IsSheaf J))) :=
  PresheafOfModules.sheafificationAdjunction (𝟙 (R.obj (P := Presheaf.IsSheaf J)))
⊢ Abelian (SheafOfModules.{v, v', u', u} R)

Tactic:
exact abelianOfAdjunction _ _ (asIso (adj.counit)) adj

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.abelianOfAdjunction, CategoryTheory.asIso