awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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)
⊢ 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.Surjective (α := (↑(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
-- 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.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)
have 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))
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict,
              Submodule.comap_subtype_self]
-- 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
⊢ (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
have 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) sorry) sorry)).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: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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
have 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 := sorry, right_inv := sorry } :
            (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 := sorry, right_inv := sorry } :
            (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⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
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 ≤ T
have h₁ : S = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range
Tactic: convert! LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).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 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
⊢ S ≤ T
have h₂ : T = (Hom.hom (↟T.subtype)).range
Tactic: convert! LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).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 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 (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range
have h₁ : S = (Hom.hom (↟S.subtype)).range
Tactic: rw [← hom_comp, ofMkLEMk_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Subobject (goal)
Goal:
R : Type u
inst : Ring R
L M N : ModuleCat.{v, u} R
f : L ⟶ M
inst_1 : HasImage f
g : Functor.obj underlying (imageSubobject f) ⟶ N
inst_2 : HasCokernel g
x y : (↑N : Type v)
l : (↑L : Type v)
w :
  x =
    HAdd.hAdd (β := (↑N : Type v)) y
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) g :
            (a : (↑(underlying.obj (imageSubobject f)) : Type v)) → (↑N : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  carrier) (Y := Functor.obj underlying (imageSubobject f)) (factorThruImageSubobject f) :
                (a : (↑L : Type v)) → (↑(underlying.obj (imageSubobject f)) : Type v))
              l :
            (↑(Functor.obj underlying (imageSubobject f)) : Type v)) :
        (↑N : Type v))
⊢ Eq (α := (↑(cokernel g) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (Y := cokernel g) (cokernel.π g) :
          (a : (↑N : Type v)) → (↑(cokernel g) : Type v))
        x :
      (↑(cokernel g) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) (Y := cokernel g) (cokernel.π g) :
          (a : (↑N : Type v)) → (↑(cokernel g) : Type v))
        y :
      (↑(cokernel g) : Type v))
have subst : Eq (α := (↑(cokernel g) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          (Y := cokernel g) (cokernel.π g) :
        (a : (↑N : Type v)) → (↑(cokernel g) : Type v))
      (HAdd.hAdd (β := (↑N : Type v)) y
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) g :
              (a : (↑(underlying.obj (imageSubobject f)) : Type v)) → (↑N : Type v))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                    carrier) (Y := Functor.obj underlying (imageSubobject f)) (factorThruImageSubobject f) :
                  (a : (↑L : Type v)) → (↑(underlying.obj (imageSubobject f)) : Type v))
                l :
              (↑(Functor.obj underlying (imageSubobject f)) : Type v)) :
          (↑N : Type v))) :
    (↑(cokernel g) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
          (Y := cokernel g) (cokernel.π g) :
        (a : (↑N : Type v)) → (↑(cokernel g) : Type v))
      y :
    (↑(cokernel g) : Type v))
Tactic: subst w
Cleared hypotheses: x, w
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
⊢ Continuous (Y := M) fun (a : M) ↦ -a
have h : ∀ (x : M), Neg.neg = HSMul.hSMul.{u, v, v} (α := R) (-1)
Tactic: convert! continuous_const_smul (-1 : R) (T := M)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
x : M
⊢ Neg.neg = HSMul.hSMul.{u, v, v} (α := R) (-1)
have h : ∀ (x : M), -x = HSMul.hSMul.{u, v, v} (α := R) (-1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1)
⊢ Eq (α := X ⟶ X)
    (CategoryStruct.comp (Y := Y)
        (ofHom (↑e : (↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) :
          Quiver.Hom (V := TopModuleCat.{u_1, u} R) (of R (↑X.1 : Type u_1)) (of R (↑Y.1 : Type u_1)))
        (ofHom (↑e.symm : (↑Y.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1))) :
      X ⟶ X)
    (𝟙 X : X ⟶ X)
have h : ∀ (x : (↑X.toModuleCat : Type u_1)),
  Eq (α := (↑X.toModuleCat : Type u_1))
    (((@hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
              (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
              (fun (X Y : TopModuleCat.{u_1, u} R) ↦
                (ContinuousLinearMap.funLike :
                  FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                    (↑Y.toModuleCat : Type u_1)))
              _ _ _
              (CategoryStruct.comp (Y := Y)
                  (ofHom (↑e : (↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) :
                    Quiver.Hom (V := TopModuleCat.{u_1, u} R) (of R (↑X.1 : Type u_1)) (of R (↑Y.1 : Type u_1)))
                  (ofHom (↑e.symm : (↑Y.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1))) :
                X ⟶ X) :
            (↑X.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1)) :
          (a : (↑X.toModuleCat : Type u_1)) → (↑X.toModuleCat : Type u_1))
        x :
      (↑X.toModuleCat : Type u_1))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
            (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
            (fun (X Y : TopModuleCat.{u_1, u} R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                  (↑Y.toModuleCat : Type u_1)))
            _ _ _ (𝟙 X : X ⟶ X) :
          (a : (↑X.toModuleCat : Type u_1)) → (↑X.toModuleCat : Type u_1))
        x :
      (↑X.toModuleCat : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1)
⊢ Eq (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := X)
        (ofHom (↑e.symm : (↑Y.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1)) :
          Quiver.Hom (V := TopModuleCat.{u_1, u} R) (of R (↑Y.1 : Type u_1)) (of R (↑X.1 : Type u_1)))
        (ofHom (↑e : (↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1))) :
      Y ⟶ Y)
    (𝟙 Y : Y ⟶ Y)
have h : ∀ (x : (↑Y.toModuleCat : Type u_1)),
  Eq (α := (↑Y.toModuleCat : Type u_1))
    (((@hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
              (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
              (fun (X Y : TopModuleCat.{u_1, u} R) ↦
                (ContinuousLinearMap.funLike :
                  FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                    (↑Y.toModuleCat : Type u_1)))
              _ _ _
              (CategoryStruct.comp (Y := X)
                  (ofHom (↑e.symm : (↑Y.toModuleCat : Type u_1) →L[R] (↑X.toModuleCat : Type u_1)) :
                    Quiver.Hom (V := TopModuleCat.{u_1, u} R) (of R (↑Y.1 : Type u_1)) (of R (↑X.1 : Type u_1)))
                  (ofHom (↑e : (↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1))) :
                Y ⟶ Y) :
            (↑Y.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) :
          (a : (↑Y.toModuleCat : Type u_1)) → (↑Y.toModuleCat : Type u_1))
        x :
      (↑Y.toModuleCat : Type u_1))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦ (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1))
            (fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1))
            (fun (X Y : TopModuleCat.{u_1, u} R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type u_1) →L[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
                  (↑Y.toModuleCat : Type u_1)))
            _ _ _ (𝟙 Y : Y ⟶ Y) :
          (a : (↑Y.toModuleCat : Type u_1)) → (↑Y.toModuleCat : Type u_1))
        x :
      (↑Y.toModuleCat : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
f : X ⟶ Y
hf :
  IsIso (X :=
    Functor.obj
      (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
        (CD := TopCat.carrier))
      X)
    (CategoryTheory.Functor.map
      (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
        (CD := TopCat.carrier))
      f)
e : (↑X.toModuleCat : Type u_1) ≃L[R] (↑Y.toModuleCat : Type u_1) :=
  let __spread.0 := Hom.hom f;
  let __spread.1 :
    (↑(Functor.obj
            (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
              (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC :=
              fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
              C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
            X) :
        Type u_1) ≃ₜ
      (↑(Functor.obj
            (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
              (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC :=
              fun (X : TopModuleCat.{u_1, u} R) ↦ (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦
              C((↑X : Type u_1), (↑Y : Type u_1))) (CD := TopCat.carrier))
            Y) :
        Type u_1) :=
    TopCat.homeoOfIso
      (asIso
        (CategoryTheory.Functor.map
          (forget₂ (TopModuleCat.{u_1, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_1, u} R) ↦
            (↑x1.toModuleCat : Type u_1) →L[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : TopModuleCat.{u_1, u} R) ↦
            (↑X.toModuleCat : Type u_1)) TopCat (FD := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
            (CD := TopCat.carrier))
          f));
  { toLinearMap := (↑__spread.0 : (↑X.toModuleCat : Type u_1) →ₗ[R] (↑Y.toModuleCat : Type u_1)),
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso f
have change : IsIso (ofIso e).hom
Tactic: change IsIso (ofIso e).hom
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X_1 : I → TopModuleCat R
f_1 : (i : I) → Quiver.Hom.{?u.207351, max u (?u.207351 + 1)} (X_1 i).toModuleCat M
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cocone
    (F ⋙
      forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
        (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
        (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦
        (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD := ModuleCat.carrier))
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ toCoinduced c.ι.app Y =
    toCoinduced c.ι.app X ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (coinduced c.ι.app)) f
have h : ∀ (x : (↑(F.obj X).toModuleCat : Type u_3)),
  Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y).toModuleCat : Type u_3))
    ((hom (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
            (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
            (↑X.toModuleCat : Type u_3)) (F.map f ≫ toCoinduced c.ι.app Y) :
          (a : (↑(F.obj X).toModuleCat : Type u_3)) →
            (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y).toModuleCat : Type u_3))
    ((hom (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
            (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
            (↑X.toModuleCat : Type u_3)) (Y := Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y)
            (toCoinduced c.ι.app X ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (coinduced c.ι.app)) f) :
          (a : (↑(F.obj X).toModuleCat : Type u_3)) →
            (↑(((Functor.const J).obj (coinduced c.ι.app)).obj Y).toModuleCat : Type u_3))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) (coinduced c.ι.app)) Y).toModuleCat : Type u_3))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Basic (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X_1 : I → TopModuleCat R
f_1 : (i : I) → Quiver.Hom.{?u.284171, max u (?u.284171 + 1)} M (X_1 i).toModuleCat
J : Type u_2
inst_2 : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat.{u_3, u} R
c :
  Cone
    (F ⋙
      forget₂ (TopModuleCat.{u_3, u} R) (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
        (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
        (↑X.toModuleCat : Type u_3)) (ModuleCat.{u_3, u} R) (FD := fun (x1 x2 : ModuleCat.{u_3, u} R) ↦
        (↑x1 : Type u_3) →ₗ[R] (↑x2 : Type u_3)) (CD := ModuleCat.carrier))
X Y : J
f : X ⟶ Y
⊢ CategoryTheory.Functor.map (Functor.obj (Functor.const J) (induced c.π.app)) f ≫ fromInduced c.π.app Y =
    fromInduced c.π.app X ≫ F.map f
have h : ∀ (x : (↑(Functor.obj (Functor.obj (Functor.const J) (induced c.π.app)) X).toModuleCat : Type u_3)),
  Eq (α := (↑(F.obj Y).toModuleCat : Type u_3))
    ((hom (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
            (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
            (↑X.toModuleCat : Type u_3)) (X := Functor.obj (Functor.obj (Functor.const J) (induced c.π.app)) X) (Y :=
            F.obj Y)
            (CategoryTheory.Functor.map (Functor.obj (Functor.const J) (induced c.π.app)) f ≫ fromInduced c.π.app Y) :
          (a : (↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat : Type u_3)) →
            (↑(F.obj Y).toModuleCat : Type u_3))
        x :
      (↑(F.obj Y).toModuleCat : Type u_3))
    ((hom (FC := fun (x1 x2 : TopModuleCat.{u_3, u} R) ↦
            (↑x1.toModuleCat : Type u_3) →L[R] (↑x2.toModuleCat : Type u_3)) (CC := fun (X : TopModuleCat.{u_3, u} R) ↦
            (↑X.toModuleCat : Type u_3)) (fromInduced c.π.app X ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat : Type u_3)) →
            (↑(F.obj Y).toModuleCat : Type u_3))
        x :
      (↑(F.obj Y).toModuleCat : Type u_3))
Tactic: ext x