awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X_1 : TopCat
R_1 : TopCat.Presheaf RingCat X_1
M_1 : PresheafOfModules R_1
x_1 : (↑X_1 : Type u)
X : TopCat
R : TopCat.Presheaf CommRingCat X
M :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : (↑X : Type u)
i : (OpenNhds x)ᵒᵖ
dsimp :
  Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
⊢ Module
    (↑(Functor.obj
          ((OpenNhds.inclusion x).op ⋙
            R ⋙
              forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                RingCat.carrier))
          i) :
      Type u)
    (↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) : Type u)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X_1 : TopCat
R_1 : TopCat.Presheaf RingCat X_1
M_1 : PresheafOfModules R_1
x_1 : (↑X_1 : Type u)
X : TopCat
R : TopCat.Presheaf CommRingCat X
M :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : (↑X : Type u)
i : (OpenNhds x)ᵒᵖ
⊢ Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X : TopCat
R : TopCat.Presheaf CommRingCat X
M :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : (↑X : Type u)
U : Opens (↑X : Type u)
hx : x ∈ U
r : (↑(R.obj (op U)) : Type u)
m : (↑(M.obj (op U)) : Type u)
i : (OpenNhds x)ᵒᵖ
dsimp :
  Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
⊢ Module
    (↑(Functor.obj
          ((OpenNhds.inclusion x).op ⋙
            R ⋙
              forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                RingCat.carrier))
          i) :
      Type u)
    (↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) : Type u)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
X : TopCat
R : TopCat.Presheaf CommRingCat X
M :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
x : (↑X : Type u)
U : Opens (↑X : Type u)
hx : x ∈ U
r : (↑(R.obj (op U)) : Type u)
m : (↑(M.obj (op U)) : Type u)
i : (OpenNhds x)ᵒᵖ
⊢ Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
    (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
⊢ (Hom.hom (Iso.inv (underlyingIso (↟N.subtype)) ≫ (mk (↟N.subtype)).arrow)).range = (Hom.hom (↟N.subtype)).range

Tactic:
congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype)))

Premises used: LinearMap.range, ModuleCat.hom_ext_iff, CategoryTheory.Subobject.underlyingIso_arrow, congr_arg, Iff.mp, Submodule.subtype, ModuleCat.ofHom
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
h :
  (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) =
    (Hom.hom (Iso.inv (underlyingIso (↟N.subtype)) ≫ (mk (↟N.subtype)).arrow)).range
h₁ : N = (Hom.hom (↟N.subtype)).range
⊢ (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) = N

Tactic:
convert!
          congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1

Premises used: LinearMap.range, ModuleCat.hom_ext_iff, CategoryTheory.Subobject.underlyingIso_arrow, congr_arg, Iff.mp, Submodule.subtype, ModuleCat.ofHom
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
hf :
  ∀ (x : (↑(of R ↥N) : Type v)),
    Eq (α := (↑(Functor.obj underlying (mk (↟N.subtype))) : Type v))
      ((Hom.hom (Iso.inv (underlyingIso (↟N.subtype))) :
            (a : (↑(of R ↥N) : Type v)) → (↑(underlying.obj (mk (↟N.subtype))) : Type v))
          x :
        (↑(Functor.obj underlying (mk (↟N.subtype))) : Type v))
      ((Hom.hom
              (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
                  (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v))) :
            (a : (↑(of R ↥N) : Type v)) → (↑(underlying.obj (mk (↟N.subtype))) : Type v))
          x :
        (↑(Functor.obj underlying (mk (↟N.subtype))) : Type v))
⊢ Eq (α := of R ↥N ⟶ Functor.obj underlying (mk (↟N.subtype))) (Iso.inv (underlyingIso (↟N.subtype)))
    (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
        (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v)))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
x : (↑(of R ↥N) : Type v)
⊢ Eq (α := (↑(Functor.obj underlying (mk (↟N.subtype))) : Type v))
    ((Hom.hom (Iso.inv (underlyingIso (↟N.subtype))) :
          (a : (↑(of R ↥N) : Type v)) → (↑(underlying.obj (mk (↟N.subtype))) : Type v))
        x :
      (↑(Functor.obj underlying (mk (↟N.subtype))) : Type v))
    ((Hom.hom
            (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
                (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v))) :
          (a : (↑(of R ↥N) : Type v)) → (↑(underlying.obj (mk (↟N.subtype))) : Type v))
        x :
      (↑(Functor.obj underlying (mk (↟N.subtype))) : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
⊢ Eq (α := of R ↥N ⟶ Functor.obj underlying (mk (↟N.subtype))) (Iso.inv (underlyingIso (↟N.subtype)))
    (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
        (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v)))

Tactic:
have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
              ext x
              rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
this :
  Eq (α := of R ↥N ⟶ Functor.obj underlying (mk (↟N.subtype))) (Iso.inv (underlyingIso (↟N.subtype)))
    (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
        (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v)))
h :
  (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) =
    (Hom.hom
        (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
              (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v)) ≫
          (mk (↟N.subtype)).arrow)).range
h₁ :
  (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) =
    (Hom.hom (mk (↟N.subtype)).arrow ∘ₗ
        Hom.hom
          (↟(↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
              (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v)))).range
h₂ :
  (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) =
    (Hom.hom (mk (↟N.subtype)).arrow ∘ₗ
        (↑(Iso.toLinearEquiv (Iso.symm (underlyingIso (↟N.subtype)))) :
          (↑(of R ↥N) : Type v) →ₗ[R] (↑(underlying.obj (mk (↟N.subtype))) : Type v))).range
h₃ h₄ :
  (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) =
    (Hom.hom (mk (↟N.subtype)).arrow).range
⊢ (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) =
    (Hom.hom (Iso.inv (underlyingIso (↟N.subtype)) ≫ (mk (↟N.subtype)).arrow)).range

Tactic:
rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]

Premises used: LinearEquiv.range_comp, ModuleCat.hom_ofHom, ModuleCat.hom_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
⊢ N = (Hom.hom (↟N.subtype)).range

Tactic:
(Submodule.range_subtype _).symm

Premises used: Submodule.subtype, Eq.symm, Submodule.range_subtype
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
⊢ N = (Hom.hom (↟N.subtype)).range

Tactic:
exact (Submodule.range_subtype _).symm

Premises used: Eq.symm, Submodule.range_subtype
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
i : Functor.obj underlying S ≅ of R ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
w :
  (LinearEquiv.toModuleIso
          (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) ⋯)).hom ≫
      ↟(Submodule.subtype ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)) =
    S.arrow
⊢ S = (fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)

Tactic:
fapply eq_mk_of_comm

Premises used: CategoryTheory.Subobject.eq_mk_of_comm
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
i :
  (↑(Functor.obj (MonoOver.forget M) (Functor.obj representative S)).1 : Type v) ≃ₗ[R]
    ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
⊢ Functor.obj underlying S ≅ of R ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)

Tactic:
apply LinearEquiv.toModuleIso

Premises used: LinearEquiv.toModuleIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
i :
  Function.Bijective (α := (↑(Functor.obj underlying S) : Type v)) (β := ↥(Hom.hom S.arrow).range)
    (⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) :
      (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)
apply :
  ∀ (c : (↑(Functor.obj underlying S) : Type v)),
    Membership.mem (α := (↑M : Type v)) (Hom.hom S.arrow).range
      ((Hom.hom S.arrow : (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v)) c : (↑M : Type v))
⊢ (↑(Functor.obj (MonoOver.forget M) (Functor.obj representative S)).1 : Type v) ≃ₗ[R]
    ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)

Tactic:
apply LinearEquiv.ofBijective (LinearMap.codRestrict
            (LinearMap.range S.arrow.hom) S.arrow.hom _)

Premises used: CategoryTheory.Subobject.arrow, LinearMap.range, LinearMap.codRestrict, ModuleCat.Hom.hom, LinearEquiv.ofBijective
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
i :
  Function.Injective (α := (↑(Functor.obj underlying S) : Type v)) (β := ↥(Hom.hom S.arrow).range)
    (⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) :
      (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)
i₁ :
  Function.Surjective (α := (↑(Functor.obj underlying S) : Type v)) (β := ↥(Hom.hom S.arrow).range)
    (⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) :
      (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)
⊢ Function.Bijective (α := (↑(Functor.obj underlying S) : Type v)) (β := ↥(Hom.hom S.arrow).range)
    (⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) :
      (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ Function.Injective (α := (↑(Functor.obj underlying S) : Type v)) (β := ↥(Hom.hom S.arrow).range)
    (⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) :
      (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)

Tactic:
simp [← LinearMap.ker_eq_bot, ker_eq_bot_of_mono]

Premises used: LinearMap.ker_eq_bot, ModuleCat.ker_eq_bot_of_mono
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
i :
  ∀ (c : (↑(Functor.obj underlying S) : Type v)),
    Membership.mem (α := (↑M : Type v)) (Hom.hom S.arrow).range
      ((Hom.hom S.arrow : (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v)) c : (↑M : Type v))
⊢ Function.Surjective (α := (↑(Functor.obj underlying S) : Type v)) (β := ↥(Hom.hom S.arrow).range)
    (⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) :
      (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)

Tactic:
rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict,
              Submodule.comap_subtype_self]

Premises used: Submodule.comap_subtype_self, LinearMap.range_eq_top, LinearMap.range_codRestrict
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ ∀ (c : (↑(Functor.obj underlying S) : Type v)),
    Membership.mem (α := (↑M : Type v)) (Hom.hom S.arrow).range
      ((Hom.hom S.arrow : (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v)) c : (↑M : Type v))

Tactic:
LinearMap.mem_range_self _

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ ∀ (c : (↑(Functor.obj underlying S) : Type v)),
    Membership.mem (α := (↑M : Type v)) (Hom.hom S.arrow).range
      ((Hom.hom S.arrow : (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v)) c : (↑M : Type v))

Tactic:
exact LinearMap.mem_range_self _

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
w :
  ∀ (x : (↑(Functor.obj underlying S) : Type v)),
    Eq (α := (↑M : Type v))
      ((Hom.hom
              ((LinearEquiv.toModuleIso
                    (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯)
                      ⋯)).hom ≫
                ↟(Submodule.subtype ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S))) :
            (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v))
          x :
        (↑M : Type v))
      ((Hom.hom S.arrow : (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v)) x : (↑M : Type v))
⊢ (LinearEquiv.toModuleIso
          (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) ⋯)).hom ≫
      ↟(Submodule.subtype ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)) =
    S.arrow

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
x : (↑(Functor.obj underlying S) : Type v)
⊢ Eq (α := (↑M : Type v))
    ((Hom.hom
            ((LinearEquiv.toModuleIso
                  (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) ⋯)).hom ≫
              ↟(Submodule.subtype ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S))) :
          (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v))
        x :
      (↑M : Type v))
    ((Hom.hom S.arrow : (a : (↑(underlying.obj S) : Type v)) → (↑M : Type v)) x : (↑M : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
⊢ LE.le (α := Subobject M)
      (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
              invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
            (a : Submodule R (↑M : Type v)) → Subobject M)
          S :
        Subobject M)
      (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
              invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
            (a : Submodule R (↑M : Type v)) → Subobject M)
          T :
        Subobject M) ↔
    S ≤ T

Tactic:
⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩

Premises used: CategoryTheory.Subobject.mk_le_mk_of_comm, Submodule.inclusion, Iff.intro, ModuleCat.ofHom, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
refine :
  ∀
    (h :
      LE.le (α := Subobject M)
        (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
                invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
              (a : Submodule R (↑M : Type v)) → Subobject M)
            S :
          Subobject M)
        (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
                invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
              (a : Submodule R (↑M : Type v)) → Subobject M)
            T :
          Subobject M)),
    S ≤ T
⊢ LE.le (α := Subobject M)
      (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
              invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
            (a : Submodule R (↑M : Type v)) → Subobject M)
          S :
        Subobject M)
      (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
              invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
            (a : Submodule R (↑M : Type v)) → Subobject M)
          T :
        Subobject M) ↔
    S ≤ T

Tactic:
refine ⟨fun h => ?_, fun h => mk_le_mk_of_comm (↟(Submodule.inclusion h)) rfl⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
h :
  LE.le (α := Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        S :
      Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        T :
      Subobject M)
⊢ (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range ≤ (Hom.hom (↟T.subtype)).range

Tactic:
LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom

Premises used: LinearMap.range_comp_le_range, Submodule.subtype, CategoryTheory.Subobject.ofMkLEMk, ModuleCat.ofHom, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
h :
  LE.le (α := Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        S :
      Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        T :
      Subobject M)
h₁ : S = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range
h₂ : T = (Hom.hom (↟T.subtype)).range
⊢ S ≤ T

Tactic:
convert! LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom

Premises used: LinearMap.range_comp_le_range, Submodule.subtype, CategoryTheory.Subobject.ofMkLEMk, ModuleCat.ofHom, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
h :
  LE.le (α := Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        S :
      Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        T :
      Subobject M)
h₁ : S = (Hom.hom (↟S.subtype)).range
⊢ S = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range

Tactic:
rw [← hom_comp, ofMkLEMk_comp]

Premises used: CategoryTheory.Subobject.ofMkLEMk_comp, ModuleCat.hom_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
h :
  LE.le (α := Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        S :
      Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        T :
      Subobject M)
⊢ S = (Hom.hom (↟S.subtype)).range

Tactic:
(Submodule.range_subtype _).symm

Premises used: Submodule.subtype, Eq.symm, Submodule.range_subtype
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S T : Submodule R (↑M : Type v)
h :
  LE.le (α := Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        S :
      Subobject M)
    (({ toFun := fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype),
            invFun := fun (S : Subobject M) ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } :
          (a : Submodule R (↑M : Type v)) → Subobject M)
        T :
      Subobject M)
⊢ S = (Hom.hom (↟S.subtype)).range

Tactic:
exact (Submodule.range_subtype _).symm

Premises used: Eq.symm, Submodule.range_subtype