awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X : TopModuleCat R
e_2 :
  (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) =
    (↑(Functor.obj
          (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
            (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
            fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
            C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
          X) :
      Type (max v u))
x :
  (↑(Functor.obj
        (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
          (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC := fun (X : TopModuleCat R) ↦
          (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
          C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
        X) :
    Type (max v u))
⊢ Function.comp (β :=
      (↑(Functor.obj
              (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
              X) :
          Type (max v u)) →₀
        R)
      (AddHom.toFun
        (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R)
          ((Finsupp.lift (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)) R
                (↑X.toModuleCat : Type (max u v)) :
              (a : (↑X.toModuleCat : Type (max u v)) → (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v))) →
                ((↑X.toModuleCat : Type (max u v)) →₀ R) →ₗ[R]
                  (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat : Type (max u v)))
            id)))
      (fun
          (x :
            (↑(Functor.obj
                  (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
                    (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC :=
                    fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
                    C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
                  X) :
              Type (max v u))) ↦
        Finsupp.single x 1)
      x =
    id x

Tactic:
simp [coe_freeObj]

Premises used: TopModuleCat.coe_freeObj
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
a :
  (↑(Functor.obj
        (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
          (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC := fun (X : TopModuleCat R) ↦
          (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
          C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))
        X) :
    Type (max v u))
⊢ Eq (α := (↑Y.toModuleCat : Type (max u v)))
    (Finsupp.sum
      (Finsupp.mapDomain (⇑(Hom.hom f) : (a : (↑X.toModuleCat : Type (max u v))) → (↑Y.toModuleCat : Type (max u v)))
        (Finsupp.single a 1))
      fun (x : (↑Y.toModuleCat : Type (max u v))) (r : R) ↦ r • x)
    ((Hom.hom f : (a : (↑X.toModuleCat : Type (max u v))) → (↑Y.toModuleCat : Type (max u v)))
      (Finsupp.sum (Finsupp.single a 1) fun (x : (↑X.toModuleCat : Type (max u v))) (r : R) ↦ r • x))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
⊢ Functor.IsRightAdjoint
    (forget₂ (TopModuleCat R) (FC := fun (x1 x2 : TopModuleCat R) ↦
      (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v))) (CC := fun (X : TopModuleCat R) ↦
      (↑X.toModuleCat : Type (max u v))) TopCat (FD := fun (X Y : TopCat) ↦
      C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CD := TopCat.carrier))

Tactic:
⟨_, ⟨freeAdj R⟩⟩

Premises used: TopModuleCat.freeAdj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
⊢ Functor.IsLeftAdjoint (D := TopModuleCat R) (free R)

Tactic:
⟨_, ⟨freeAdj R⟩⟩

Premises used: TopModuleCat.freeAdj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
⊢ Mono (kerι φ)

Tactic:
ConcreteCategory.mono_of_injective (kerι φ) <| Subtype.val_injective

Premises used: Subtype.val_injective, TopModuleCat.kerι, CategoryTheory.ConcreteCategory.mono_of_injective
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
h :
  ∀ (val : (↑M.toModuleCat : Type v))
    (hm : val ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker),
    Eq (α := (↑N.toModuleCat : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
              (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
              (↑X.toModuleCat : Type v)) (kerι φ ≫ φ) :
            (a : (↑(ker φ).toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
          (Subtype.mk (p := fun (x : (↑M.toModuleCat : Type v)) ↦
            x ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker) val hm) :
        (↑N.toModuleCat : Type v))
      ((@ConcreteCategory.hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat.{v, u} R) ↦ (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v))
              (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) _ _ (ker φ) N 0 :
            (a : (↑(ker φ).toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
          (Subtype.mk (p := fun (x : (↑M.toModuleCat : Type v)) ↦
            x ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker) val hm) :
        (↑N.toModuleCat : Type v))
⊢ kerι φ ≫ φ = 0

Tactic:
ext ⟨_, hm⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
val : (↑M.toModuleCat : Type v)
hm : val ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
⊢ Eq (α := (↑N.toModuleCat : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
            (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
            (↑X.toModuleCat : Type v)) (kerι φ ≫ φ) :
          (a : (↑(ker φ).toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        (Subtype.mk (p := fun (x : (↑M.toModuleCat : Type v)) ↦
          x ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker) val hm) :
      (↑N.toModuleCat : Type v))
    ((@ConcreteCategory.hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{v, u} R) ↦ (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v))
            (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) _ _ (ker φ) N 0 :
          (a : (↑(ker φ).toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        (Subtype.mk (p := fun (x : (↑M.toModuleCat : Type v)) ↦
          x ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker) val hm) :
      (↑N.toModuleCat : Type v))

Tactic:
hm

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
val : (↑M.toModuleCat : Type v)
hm : val ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
⊢ Eq (α := (↑N.toModuleCat : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
            (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
            (↑X.toModuleCat : Type v)) (kerι φ ≫ φ) :
          (a : (↑(ker φ).toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        (Subtype.mk (p := fun (x : (↑M.toModuleCat : Type v)) ↦
          x ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker) val hm) :
      (↑N.toModuleCat : Type v))
    ((@ConcreteCategory.hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{v, u} R) ↦ (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v))
            (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) _ _ (ker φ) N 0 :
          (a : (↑(ker φ).toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        (Subtype.mk (p := fun (x : (↑M.toModuleCat : Type v)) ↦
          x ∈ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker) val hm) :
      (↑N.toModuleCat : Type v))

Tactic:
exact hm
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
x : (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) (ker φ)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
          (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
          (↑X.toModuleCat : Type v)) (kerι φ) :
        (a : (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) (ker φ)) →
          (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) M)
      x =
    (↑x : (↑M.toModuleCat : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : KernelFork φ
m : (↑s.pt.toModuleCat : Type v)
rw :
  Eq (α := (↑N.toModuleCat : Type v))
    (((↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)) :
          (a : (↑M.toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        ((Hom.hom (Fork.ι s) : (a : (↑s.pt.toModuleCat : Type v)) → (↑M.toModuleCat : Type v)) m :
          (↑M.toModuleCat : Type v)) :
      (↑N.toModuleCat : Type v))
    (0 : (↑N.toModuleCat : Type v))
rw₁ :
  Eq (α := (↑N.toModuleCat : Type v))
    ((Hom.hom φ : (a : (↑M.toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        ((Hom.hom (Fork.ι s) : (a : (↑s.pt.toModuleCat : Type v)) → (↑M.toModuleCat : Type v)) m :
          (↑M.toModuleCat : Type v)) :
      (↑N.toModuleCat : Type v))
    (0 : (↑N.toModuleCat : Type v))
rw₂ :
  Eq (α := (↑N.toModuleCat : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
            (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
            (↑X.toModuleCat : Type v)) (Fork.ι s ≫ φ) :
          (a : (↑s.pt.toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        m :
      (↑N.toModuleCat : Type v))
    (0 : (↑N.toModuleCat : Type v))
rw₃ :
  Eq (α := (↑N.toModuleCat : Type v))
    ((@ConcreteCategory.hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{v, u} R) ↦ (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v))
            (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) _ _ s.pt N 0 :
          (a : (↑s.pt.toModuleCat : Type v)) → (↑N.toModuleCat : Type v))
        m :
      (↑N.toModuleCat : Type v))
    (0 : (↑N.toModuleCat : Type v))
rw₄ rw₅ : Eq.{v + 1} (α := (↑N.toModuleCat : Type v)) 0 0
⊢ Membership.mem (α := (↑M.toModuleCat : Type v))
    (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
    ((Hom.hom (Fork.ι s) : (a : (↑s.pt.toModuleCat : Type v)) → (↑M.toModuleCat : Type v)) m :
      (↑M.toModuleCat : Type v))

Tactic:
rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply]

Premises used: TopModuleCat.hom_zero_apply, CategoryTheory.ConcreteCategory.comp_apply, ContinuousLinearMap.coe_coe, CategoryTheory.Limits.KernelFork.condition, LinearMap.mem_ker, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : KernelFork φ
m : s.pt ⟶ (KernelFork.ofι (kerι φ) ⋯).pt
h : m ≫ kerι φ = Fork.ι s
rw :
  Fork.ι s =
    ofHom
        ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
          ⋯) ≫
      kerι φ
⊢ m =
    ofHom
      ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
        ⋯)

Tactic:
rw [← cancel_mono (kerι φ), h]

Premises used: CategoryTheory.cancel_mono, TopModuleCat.kerι
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : KernelFork φ
m : s.pt ⟶ (KernelFork.ofι (kerι φ) ⋯).pt
h : m ≫ kerι φ = Fork.ι s
⊢ Fork.ι s =
    ofHom
        ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
          ⋯) ≫
      kerι φ

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
⊢ Continuous (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.mkQ.toFun

Tactic:
tauto
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
x : (↑N.toModuleCat : Type v)
⊢ Eq (α := (↑(coker φ).toModuleCat : Type v))
    ((Hom.hom (cokerπ φ) : (a : (↑N.toModuleCat : Type v)) → (↑(coker φ).toModuleCat : Type v)) x :
      (↑(coker φ).toModuleCat : Type v))
    (((↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.mkQ :
          (a : (↑N.toModuleCat : Type v)) →
            (↑N.toModuleCat : Type v) ⧸
              (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
        x :
      (↑N.toModuleCat : Type v) ⧸ (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
⊢ Function.Surjective (α := (↑N.toModuleCat : Type v)) (β := (↑(coker φ).toModuleCat : Type v))
    (⇑(Hom.hom (cokerπ φ)) : (a : (↑N.toModuleCat : Type v)) → (↑(coker φ).toModuleCat : Type v))

Tactic:
Submodule.mkQ_surjective _

Premises used: Submodule.mkQ_surjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
⊢ Epi (cokerπ φ)

Tactic:
ConcreteCategory.epi_of_surjective (cokerπ φ) (cokerπ_surjective φ)

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective, TopModuleCat.cokerπ, TopModuleCat.cokerπ_surjective
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
h :
  ∀ (m : (↑M.toModuleCat : Type v)),
    Eq (α := (↑(coker φ).toModuleCat : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
              (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
              (↑X.toModuleCat : Type v)) (φ ≫ cokerπ φ) :
            (a : (↑M.toModuleCat : Type v)) → (↑(coker φ).toModuleCat : Type v))
          m :
        (↑(coker φ).toModuleCat : Type v))
      ((@ConcreteCategory.hom _ (instCategory R)
              (fun (x1 x2 : TopModuleCat.{v, u} R) ↦ (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v))
              (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) _ _ M (coker φ) 0 :
            (a : (↑M.toModuleCat : Type v)) → (↑(coker φ).toModuleCat : Type v))
          m :
        (↑(coker φ).toModuleCat : Type v))
⊢ φ ≫ cokerπ φ = 0

Tactic:
ext m
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
m : (↑M.toModuleCat : Type v)
h :
  Eq (α :=
    (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) N ⧸
      (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
    (((↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.mkQ :
          (a : (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) N) →
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) N ⧸
              (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
              (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
              (↑X.toModuleCat : Type v)) φ :
            (a : (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) M) →
              (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) N)
          m) :
      (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) N ⧸
        (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
    (0 :
      (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) N ⧸
        (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
⊢ Eq (α := (↑(coker φ).toModuleCat : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
            (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
            (↑X.toModuleCat : Type v)) (φ ≫ cokerπ φ) :
          (a : (↑M.toModuleCat : Type v)) → (↑(coker φ).toModuleCat : Type v))
        m :
      (↑(coker φ).toModuleCat : Type v))
    ((@ConcreteCategory.hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat.{v, u} R) ↦ (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v))
            (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) _ _ M (coker φ) 0 :
          (a : (↑M.toModuleCat : Type v)) → (↑(coker φ).toModuleCat : Type v))
        m :
      (↑(coker φ).toModuleCat : Type v))

Tactic:
change Submodule.mkQ _ (φ m) = 0

Premises used: CategoryTheory.ConcreteCategory.hom, Submodule.mkQ, DFunLike.coe
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
m : (↑M.toModuleCat : Type v)
⊢ Eq (α :=
    (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) N ⧸
      (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
    (((↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.mkQ :
          (a : (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) N) →
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) N ⧸
              (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : TopModuleCat.{v, u} R) ↦
              (↑x1.toModuleCat : Type v) →L[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : TopModuleCat.{v, u} R) ↦
              (↑X.toModuleCat : Type v)) φ :
            (a : (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) M) →
              (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type v)) N)
          m) :
      (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) N ⧸
        (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)
    (0 :
      (fun (X : TopModuleCat.{v, u} R) ↦ (↑X.toModuleCat : Type v)) N ⧸
        (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
rw :
  Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v))
    (↑(Hom.hom 0) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0
rw₁ :
  Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v))
    (↑0 : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0
rw₂ rw₃ : Eq.{v + 1} (α := (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) 0 0
⊢ (↑(Hom.hom (φ ≫ Cofork.π s)) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) = 0

Tactic:
rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero]

Premises used: TopModuleCat.hom_zero, CategoryTheory.Limits.CokernelCofork.condition, ContinuousLinearMap.coe_zero
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : cokerπ φ ≫ m = Cofork.π s
rw :
  Cofork.π s =
    cokerπ φ ≫
      ofHom
        {
          toLinearMap :=
            (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.liftQ
              (↑(Hom.hom (Cofork.π s)) : (↑N.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) ⋯,
          cont := ⋯ }
⊢ m =
    ofHom
      {
        toLinearMap :=
          (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.liftQ
            (↑(Hom.hom (Cofork.π s)) : (↑N.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) ⋯,
        cont := ⋯ }

Tactic:
rw [← cancel_epi (cokerπ φ), h]

Premises used: TopModuleCat.cokerπ, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : cokerπ φ ≫ m = Cofork.π s
⊢ Cofork.π s =
    cokerπ φ ≫
      ofHom
        {
          toLinearMap :=
            (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).range.liftQ
              (↑(Hom.hom (Cofork.π s)) : (↑N.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) ⋯,
          cont := ⋯ }

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
⊢ Functor.Full (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)

Tactic:
(fullyFaithfulUliftFunctor R).full

Premises used: ModuleCat.fullyFaithfulUliftFunctor, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
⊢ Functor.Faithful (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)

Tactic:
(fullyFaithfulUliftFunctor R).faithful

Premises used: ModuleCat.fullyFaithfulUliftFunctor, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
⊢ Limits.PreservesLimitsOfSize.{v, v, v, max v' v, max u (v + 1), max (v' + 1) (v + 1)}
    (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier) ⋙
      CategoryTheory.uliftFunctor.{v', v})

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Ulift
Goal:
R : Type u
inst : Ring R
⊢ Limits.PreservesFiniteLimits (C := ModuleCat.{v, u} R) (uliftFunctor.{v', v, u} R)

Tactic:
Limits.PreservesLimitsOfSize.preservesFiniteLimits _

Premises used: CategoryTheory.Limits.PreservesLimitsOfSize.preservesFiniteLimits