awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ T = (Hom.hom (↟T.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)
⊢ T = (Hom.hom (↟T.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
⊢ WellPowered.{v, v, max (v + 1) u} (ModuleCat.{v, u} R)

Tactic:
⟨fun M => ⟨⟨_, ⟨(subobjectModule M).toEquiv⟩⟩⟩⟩

Premises used: Submodule, CategoryTheory.WellPowered.mk, Small.mk, Nonempty.intro, ModuleCat.subobjectModule, ModuleCat.carrier, Exists.intro, RelIso.toEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{u_1, u} R
f : M ⟶ N
x : ↥(Hom.hom f).ker
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC :=
          carrier) (kernelSubobject f).arrow :
        (a : (↑(underlying.obj (kernelSubobject f)) : Type u_1)) → (↑M : Type u_1))
      ((toKernelSubobject : (a : ↥(Hom.hom f).ker) → (↑(underlying.obj (kernelSubobject f)) : Type u_1)) x :
        (↑(Functor.obj underlying (kernelSubobject f)) : Type u_1)) =
    (↑x : (↑M : Type u_1))

Tactic:
simp [toKernelSubobject, -hom_comp, ← CategoryTheory.comp_apply]

Premises used: ModuleCat.toKernelSubobject, CategoryTheory.comp_apply, ModuleCat.hom_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
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))
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))
⊢ 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))

Tactic:
subst w
-- Module: Mathlib.Algebra.Category.ModuleCat.Subobject
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
y : (↑N : Type v)
l : (↑L : 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))
        (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:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Tannaka
Goal:
R : Type u
inst : Ring R
x : R
⊢ (fun
          (φ :
            End (C := ModuleCat R ⥤+ AddCommGrpCat)
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier)))) ↦
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (X :=
                Functor.obj
                  (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                    (AdditiveFunctor.of
                      (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                        (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                        (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
                  (ModuleCat.of R R))
                (φ.hom.app (ModuleCat.of R R)) :
              (a :
                  (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj (ModuleCat.of R R)) : Type u)) →
                (↑((AdditiveFunctor.of (forget₂ (ModuleCat R) AddCommGrpCat)).obj.obj (ModuleCat.of R R)) : Type u))
            1 :
          (↑(Functor.obj
                (ObjectProperty.FullSubcategory.obj (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
                  (AdditiveFunctor.of
                    (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                      (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier))))
                (ModuleCat.of R R)) :
            Type u)))
      ((fun (r : R) ↦
          (ObjectProperty.homMk (P := additiveFunctor (ModuleCat R) AddCommGrpCat)
              { app := fun (M : ModuleCat R) ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M : Type u) r),
                naturality := ⋯ } :
            Quiver.Hom (V :=
              ObjectProperty.FullSubcategory (C := ModuleCat R ⥤ AddCommGrpCat)
                (additiveFunctor (ModuleCat R) AddCommGrpCat))
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier)))
              (AdditiveFunctor.of
                (forget₂ (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CD := AddCommGrpCat.carrier)))))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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 (x : M) ↦ HSMul.hSMul.{u, v, v} (α := R) (-1) x

Tactic:
continuous_const_smul (-1 : R) (T := M)

Premises used: ContinuousConstSMul.continuous_const_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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
h : ∀ (x : M), Neg.neg = HSMul.hSMul.{u, v, v} (α := R) (-1)
⊢ Continuous (Y := M) fun (a : M) ↦ -a

Tactic:
convert! continuous_const_smul (-1 : R) (T := M)

Premises used: ContinuousConstSMul.continuous_const_smul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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
h : ∀ (x : M), -x = HSMul.hSMul.{u, v, v} (α := R) (-1) x
⊢ Neg.neg = HSMul.hSMul.{u, v, v} (α := R) (-1)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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 x_1 : M
⊢ -x_1 = HSMul.hSMul.{u, v, v} (α := R) (-1) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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
⊢ (↑(toModuleCat (of R M)) : Type v) = M

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : Type v
inst_2 : AddCommGroup X
inst_3 : Module R X
inst_4 : TopologicalSpace X
inst_5 : ContinuousAdd X
inst_6 : ContinuousSMul R X
inst_7 : AddCommGroup Y
inst_8 : Module R Y
inst_9 : TopologicalSpace Y
inst_10 : ContinuousAdd Y
inst_11 : ContinuousSMul R Y
f : X →L[R] Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat.{u_1, u} R
f : X.Hom Y
⊢ ofHom f.hom = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y Z : TopModuleCat.{u_1, u} R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.hom (f ≫ g) = Hom.hom g ∘SL Hom.hom f

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat.{u_1, u} R
⊢ @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) =
    ContinuousLinearMap.id R (↑X.toModuleCat : Type u_1)

Tactic:
rfl

Premises used: ContinuousLinearMap.id, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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)
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))
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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)
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:
e.symm_apply_apply _

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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)
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:
exact e.symm_apply_apply _

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
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)
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))
⊢ 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)

Tactic:
ext