awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R_1 : Sheaf J RingCat
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
N : PresheafOfModules.{v, v₁, u₁, u} R
hN : Presheaf.IsSheaf J N.presheaf
inst_1 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_2 : IsLocallySurjective J f
inst_3 : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN :
        (a : (toPresheaf R).obj M₂ ⟶ N.presheaf) → (toPresheaf R).obj M₁ ⟶ N.presheaf)
      φ =
    (toPresheaf R).map ψ
⊢ ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
    (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
            (M₂.presheaf.obj X) (N.presheaf.obj X)
            (NatTrans.app
              (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                  (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                ((toPresheaf R).map ψ))
              X) :
          (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
        ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                (fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) AddCommGrpCat.carrier _ _
                (M₂.presheaf.obj X) (N.presheaf.obj X)
                (NatTrans.app
                  (((ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN).symm :
                      (a : (toPresheaf R).obj M₁ ⟶ N.presheaf) → (toPresheaf R).obj M₂ ⟶ N.presheaf)
                    ((toPresheaf R).map ψ))
                  X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            m :
          (↑(N.presheaf.obj X) : Type v))
have simp : ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (φ.app X) :
        (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
      (r • m) =
    HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (φ.app X) :
            (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
          m :
        (↑(N.presheaf.obj X) : Type v))
Tactic: simp only [← hφ, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R_1 : Sheaf J RingCat
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
f : M₁ ⟶ M₂
N : PresheafOfModules.{v, v₁, u₁, u} R
hN : Presheaf.IsSheaf J N.presheaf
inst_1 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
    (CA := AddCommGrpCat.carrier)
inst_2 : IsLocallySurjective J f
inst_3 : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) ⋯ N.presheaf hN :
        (a : (toPresheaf R).obj M₂ ⟶ N.presheaf) → (toPresheaf R).obj M₁ ⟶ N.presheaf)
      φ =
    (toPresheaf R).map ψ
⊢ ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₂.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(N.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₂.presheaf.obj X) : Type v)) → (↑(N.presheaf.obj X) : Type v))
            m :
          (↑(N.presheaf.obj X) : Type v))
have hφ₁ : ∀ (Z : Cᵒᵖ) (x : (↑(M₁.obj Z) : Type v)),
  Eq (α := (↑(N.presheaf.obj Z) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app Z) :
          (a : (↑(((toPresheaf R).obj M₂).obj Z) : Type v)) → (↑(N.presheaf.obj Z) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (f.app Z) :
              (a : (↑(M₁.obj Z) : Type v)) → (↑(M₂.obj Z) : Type v))
            x :
          (↑(M₂.obj Z) : Type v)) :
      (↑(N.presheaf.obj Z) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (ψ.app Z) :
          (a : (↑(M₁.obj Z) : Type v)) → (↑(N.obj Z) : Type v))
        x :
      (↑(N.obj Z) : Type v))
Tactic: replace hφ : ∀ (Z : Cᵒᵖ) (x : M₁.obj Z), φ.app Z (f.app Z x) = ψ.app Z x :=
          fun Z x ↦ CategoryTheory.congr_fun (congr_app hφ Z) x
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Simple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Simple (C := ModuleCat.{u_2, u_1} R) (of R M) ↔ IsSimpleModule R M
have rw : IsSimpleOrder (Subobject (C := ModuleCat.{u_2, u_1} R) (of R M)) ↔ IsSimpleModule R M
Tactic: rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff,
    isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Simple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : IsSimpleOrder (Subobject (C := ModuleCat.{u_2, u_1} R) (of R M)) ↔ IsSimpleModule R M
⊢ Simple (C := ModuleCat.{u_2, u_1} R) (of R M) ↔ IsSimpleModule R M
have rw₁ : IsSimpleOrder.{u_2} (Submodule R (↑(of R M) : Type u_2)) ↔ IsSimpleModule R M
Tactic: rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff,
    isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Simple (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : IsSimpleOrder (Subobject (C := ModuleCat.{u_2, u_1} R) (of R M)) ↔ IsSimpleModule R M
rw₁ : IsSimpleOrder.{u_2} (Submodule R (↑(of R M) : Type u_2)) ↔ IsSimpleModule R M
⊢ Simple (C := ModuleCat.{u_2, u_1} R) (of R M) ↔ IsSimpleModule R M
have rw₂ : IsSimpleOrder.{u_2} (Submodule R (↑(of R M) : Type u_2)) ↔ IsSimpleOrder.{u_2} (Submodule R M)
Tactic: rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff,
    isSimpleModule_iff]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Stalk (goal)
Goal:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : (↑X : Type u)
i : (OpenNhds x)ᵒᵖ
⊢ Module (↑(((OpenNhds.inclusion x).op ⋙ R).obj i) : Type u)
    (↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) : Type u)
have dsimp : Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
  (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Stalk (goal)
Goal:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
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 (↑(((OpenNhds.inclusion x).op ⋙ R).obj i) : Type u)
    (↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i) : Type u)
have dsimp : Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
  (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Stalk (goal)
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
    (↑(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)
have dsimp : Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
  (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Stalk (goal)
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
    (↑(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)
have dsimp : Module (↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
  (↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i)))) : Type u)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
⊢ (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) = N
have 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
Tactic: convert!
          congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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
⊢ (fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) ((fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) N) = N
have h₁ : N = (Hom.hom (↟N.subtype)).range
Tactic: convert!
          congr_arg LinearMap.range
            (ModuleCat.hom_ext_iff.mp (underlyingIso_arrow (ofHom N.subtype))) using 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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)))
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (hypothesis)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
N : Submodule R (↑M : Type v)
⊢ (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
have 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)))
Tactic: have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
              ext x
              rfl
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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)))
⊢ (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
have 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
Tactic: rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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
⊢ (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
have 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
Tactic: rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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
⊢ (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
have 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
Tactic: rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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
⊢ (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
have 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
Tactic: rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ S = (fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
have i : Functor.obj underlying S ≅ of R ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
Tactic: fapply eq_mk_of_comm
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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)
⊢ S = (fun (N : Submodule R (↑M : Type v)) ↦ mk (↟N.subtype)) ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
have w : (LinearEquiv.toModuleIso
        (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) sorry) sorry)).hom ≫
    ↟(Submodule.subtype ((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)) =
  S.arrow
Tactic: fapply eq_mk_of_comm
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ Functor.obj underlying S ≅ of R ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
have i : (↑(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.toModuleIso
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ (↑(Functor.obj (MonoOver.forget M) (Functor.obj representative S)).1 : Type v) ≃ₗ[R]
    ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
have 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) sorry) :
    (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)
Tactic: apply LinearEquiv.ofBijective (LinearMap.codRestrict
            (LinearMap.range S.arrow.hom) S.arrow.hom _)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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)
⊢ (↑(Functor.obj (MonoOver.forget M) (Functor.obj representative S)).1 : Type v) ≃ₗ[R]
    ↥((fun (S : Subobject M) ↦ (Hom.hom S.arrow).range) S)
have 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))
Tactic: apply LinearEquiv.ofBijective (LinearMap.codRestrict
            (LinearMap.range S.arrow.hom) S.arrow.hom _)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
S : Subobject M
⊢ 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)
have 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) sorry) :
    (a : (↑(underlying.obj S) : Type v)) → ↥(Hom.hom S.arrow).range)
Tactic: constructor