awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : TopCat
f : X ⟶ Y
τ : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R)
h :
  Membership.mem (γ := Set (TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v))))
    {t : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R) |
      ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R) ∧
        ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R) ∧
          TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ t}
    τ
hτ₁ : ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R)
hτ₂ : ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R)
hτ₃ : TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ LE.le (α := TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (TopologicalSpace.coinduced
      (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
        (AddHom.toFun
          (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
        fun (x : (↑X : Type v)) ↦ Finsupp.single x 1)
      X.str)
    (TopologicalSpace.coinduced ((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) X.str)
have hxy : (↑(toModuleCat (freeObj R Y)) : Type (max u v)) = Finsupp.{v, u} (↑Y : Type v) R →
  Eq (α := (↑X : Type v) → (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      fun (x : (↑X : Type v)) ↦ Finsupp.single x 1)
    ((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun)
Tactic: congr! 1
-- 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 : TopCat
f : X ⟶ Y
τ : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R)
h :
  Membership.mem (γ := Set (TopologicalSpace (↑(toModuleCat (freeObj R Y)) : Type (max u v))))
    {t : TopologicalSpace (Finsupp.{v, u} (↑Y : Type v) R) |
      ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R) ∧
        ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R) ∧
          TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ t}
    τ
hτ₁ : ContinuousSMul R (Finsupp.{v, u} (↑Y : Type v) R)
hτ₂ : ContinuousAdd (Finsupp.{v, u} (↑Y : Type v) R)
hτ₃ : TopologicalSpace.coinduced (fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) Y.str ≤ τ
e_2 : (↑(toModuleCat (freeObj R Y)) : Type (max u v)) = Finsupp.{v, u} (↑Y : Type v) R
⊢ Eq (α := (↑X : Type v) → (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      fun (x : (↑X : Type v)) ↦ Finsupp.single x 1)
    ((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun)
have hxy : ∀ (x : (↑X : Type v)),
  Eq (α := (↑(toModuleCat (freeObj R Y)) : Type (max u v)))
    (Function.comp (β := Finsupp.{v, u} (↑X : Type v) R)
      (AddHom.toFun
        (LinearMap.toAddHom (Finsupp.lmapDomain R R (⇑(TopCat.Hom.hom f) : (a : (↑X : Type v)) → (↑Y : Type v)))))
      (fun (x : (↑X : Type v)) ↦ Finsupp.single x 1) x)
    (((fun (x : (↑Y : Type v)) ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) x)
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 : TopCat
⊢ Eq (α := Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) (freeMap R (𝟙 M)) (𝟙 (freeObj R M))
have h : ∀ (x : (↑(toModuleCat (freeObj R M)) : Type (max u v))),
  Eq (α := (↑(toModuleCat (freeObj R M)) : Type (max u v)))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat R) ↦ (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
            (fun (X Y : TopModuleCat R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                  (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
            _ _ _ (freeMap R (𝟙 M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
          (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R M)) : Type (max u v)))
    ((@hom _ (instCategory R)
            (fun (x1 x2 : TopModuleCat R) ↦ (↑x1.toModuleCat : Type (max u v)) →L[R] (↑x2.toModuleCat : Type (max u v)))
            (fun (X : TopModuleCat R) ↦ (↑X.toModuleCat : Type (max u v)))
            (fun (X Y : TopModuleCat R) ↦
              (ContinuousLinearMap.funLike :
                FunLike ((↑X.toModuleCat : Type (max u v)) →L[R] (↑Y.toModuleCat : Type (max u v)))
                  (↑X.toModuleCat : Type (max u v)) (↑Y.toModuleCat : Type (max u v))))
            _ _ _ (𝟙 (freeObj R M) : Quiver.Hom (V := TopModuleCat R) (freeObj R M) (freeObj R M)) :
          (a : (↑(freeObj R M).toModuleCat : Type (max u v))) → (↑(freeObj R M).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R M)) : Type (max u v)))
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
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Quiver.Hom (V := TopModuleCat R) (freeObj R X) (freeObj R Z)) (freeMap R (f ≫ g)) (freeMap R f ≫ freeMap R g)
have h : ∀ (x : (↑(toModuleCat (freeObj R X)) : Type (max u v))),
  Eq (α := (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
    ((hom (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))) (freeMap R (f ≫ g)) :
          (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
    ((hom (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))) (freeMap R f ≫ freeMap R g) :
          (a : (↑(freeObj R X).toModuleCat : Type (max u v))) → (↑(freeObj R Z).toModuleCat : Type (max u v)))
        x :
      (↑(toModuleCat (freeObj R Z)) : Type (max u v)))
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 : TopModuleCat R
⊢ Continuous (X :=
    (↑(toModuleCat
          (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) ⋙
              free R)
            X)) :
      Type (max u v)))
    (Y := (↑(Functor.obj (𝟭 (TopModuleCat R)) X).toModuleCat : Type (max u v)))
    (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)))
have rw : LE.le (α :=
  TopologicalSpace
    (↑(toModuleCat
          (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) ⋙
              free R)
            X)) :
      Type (max u v)))
  (topologicalSpace
    (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) ⋙
        free R)
      X))
  (TopologicalSpace.induced
    (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)))
    (Functor.obj (𝟭 (TopModuleCat R)) X).topologicalSpace)
Tactic: rw [continuous_iff_le_induced]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
⊢ kerι φ ≫ φ = 0
have 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))
Tactic: ext ⟨_, hm⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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)
⊢ 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))
have 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))
Tactic: rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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))
⊢ 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))
have 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))
Tactic: rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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))
⊢ 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))
have 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))
Tactic: rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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))
⊢ 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))
have 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))
Tactic: rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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))
⊢ 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))
have rw₄ : Eq.{v + 1} (α := (↑N.toModuleCat : Type v)) 0 0
Tactic: rw [LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
        ← ConcreteCategory.comp_apply (Fork.ι s) φ, KernelFork.condition, hom_zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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
⊢ m =
    ofHom
      ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
        ⋯)
have rw : Fork.ι s =
  ofHom
      ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ) : (↑M.toModuleCat : Type v) →ₗ[R] (↑N.toModuleCat : Type v)).ker
        sorry) ≫
    kerι φ
Tactic: rw [← cancel_mono (kerι φ), h]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
⊢ φ ≫ cokerπ φ = 0
have 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))
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
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 (α := (↑(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))
have 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)
Tactic: change Submodule.mkQ _ (φ m) = 0
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Topology.Homology (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : TopologicalSpace R
M N : TopModuleCat.{v, u} R
φ : M ⟶ N
s : CokernelCofork φ
⊢ (↑(Hom.hom (φ ≫ Cofork.π s)) : (↑M.toModuleCat : Type v) →ₗ[R] (↑s.pt.toModuleCat : Type v)) = 0
have 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
Tactic: rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero]