awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
⊢ IsUnit (M :=
    Module.End (↑R : Type u)
      (↑(Functor.obj
            (Functor.op (inducedFunctor basicOpen) ⋙
              (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
            r) :
        Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑(Functor.obj
                    (Functor.op (inducedFunctor basicOpen) ⋙
                      (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                    r) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r) :
                Type u))
        (unop r) :
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              r) :
          Type u))

Tactic:
isUnit_algebraMap_end_basicOpen ..

Premises used: PrimeSpectrum.basicOpen, Set.Mem, setOf, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
⊢ IsUnit (M :=
    Module.End (↑R : Type u)
      (↑(Functor.obj
            (Functor.op (inducedFunctor basicOpen) ⋙
              (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
            r) :
        Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑(Functor.obj
                    (Functor.op (inducedFunctor basicOpen) ⋙
                      (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                    r) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor basicOpen).op ⋙ (modulesSpecToSheaf.obj ((tilde.functor R).obj M)).obj).obj r) :
                Type u))
        (unop r) :
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf ((tilde.functor R).obj M)).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              r) :
          Type u))

Tactic:
exact isUnit_algebraMap_end_basicOpen ..

Premises used: AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
h :
  Eq (α :=
    LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑M : Type u)
      (↑((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (basicOpen (unop r)))) :
        Type u))
    (ModuleCat.Hom.hom
        (NatTrans.app
          (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map (toOpen M ⊤) ≫ (tilde M).fromTildeΓ)))
          (op (basicOpen (unop r)))) ∘ₗ
      ModuleCat.Hom.hom (toOpen M (basicOpen (unop r))))
    (ModuleCat.Hom.hom
        (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 (tilde M))))
          (op (basicOpen (unop r)))) ∘ₗ
      ModuleCat.Hom.hom (toOpen M (basicOpen (unop r))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp [toTildeΓNatIso, isoTop,
      TopCat.Sheaf.restrictHomEquivHom, Functor.IsCoverDense.restrictHomEquivHom,
      fromTildeΓNatTrans, moduleSpecΓFunctor, Sheaf.forget, sheafToPresheaf]

Premises used: TopCat.Sheaf.restrictHomEquivHom, AlgebraicGeometry.Scheme.Modules.fromTildeΓNatTrans, AlgebraicGeometry.moduleSpecΓFunctor, AlgebraicGeometry.tilde.isoTop, CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom, AlgebraicGeometry.tilde.toTildeΓNatIso, TopCat.Sheaf.forget, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
h :
  Eq (α :=
    LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑M : Type u)
      (↑((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (basicOpen (unop r)))) :
        Type u))
    (ModuleCat.Hom.hom
      (toOpen M (basicOpen (unop r)) ≫
        NatTrans.app
          (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map (toOpen M ⊤)) ≫
              CategoryTheory.Functor.map modulesSpecToSheaf (tilde M).fromTildeΓ))
          (op (basicOpen (unop r)))))
    (ModuleCat.Hom.hom
      (toOpen M (basicOpen (unop r)) ≫
        NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 (tilde M))))
          (op (basicOpen (unop r)))))
⊢ Eq (α :=
    LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑M : Type u)
      (↑((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (basicOpen (unop r)))) :
        Type u))
    (ModuleCat.Hom.hom
        (NatTrans.app
          (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map (toOpen M ⊤) ≫ (tilde M).fromTildeΓ)))
          (op (basicOpen (unop r)))) ∘ₗ
      ModuleCat.Hom.hom (toOpen M (basicOpen (unop r))))
    (ModuleCat.Hom.hom
        (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 (tilde M))))
          (op (basicOpen (unop r)))) ∘ₗ
      ModuleCat.Hom.hom (toOpen M (basicOpen (unop r))))

Tactic:
simp only [← ModuleCat.hom_comp, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, ModuleCat.hom_comp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
h :
  Eq (α :=
    M.Hom
      ((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op (basicOpen (unop r)))))
    (toOpen M (basicOpen (unop r)) ≫
      NatTrans.app
        (InducedCategory.Hom.hom
          (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map (toOpen M ⊤)) ≫
            CategoryTheory.Functor.map modulesSpecToSheaf (tilde M).fromTildeΓ))
        (op (basicOpen (unop r))))
    (toOpen M (basicOpen (unop r)) ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 (tilde M))))
        (op (basicOpen (unop r))))
⊢ Eq (α :=
    LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑M : Type u)
      (↑((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (basicOpen (unop r)))) :
        Type u))
    (ModuleCat.Hom.hom
      (toOpen M (basicOpen (unop r)) ≫
        NatTrans.app
          (InducedCategory.Hom.hom
            (CategoryTheory.Functor.map modulesSpecToSheaf (tilde.map (toOpen M ⊤)) ≫
              CategoryTheory.Functor.map modulesSpecToSheaf (tilde M).fromTildeΓ))
          (op (basicOpen (unop r)))))
    (ModuleCat.Hom.hom
      (toOpen M (basicOpen (unop r)) ≫
        NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 (tilde M))))
          (op (basicOpen (unop r)))))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 M : ModuleCat (↑R : Type u)
r :
  (InducedCategory (C := (↑(CommRingCat.of (↑R : Type u)) : Type u)) (Opens ↥(Spec (CommRingCat.of (↑R : Type u))))
      basicOpen)ᵒᵖ
⊢ Eq (α :=
    M.Hom
      ((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op (basicOpen (unop r)))))
    (CategoryStruct.comp (Y :=
      (Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op ⊤))
      (toOpen M ⊤)
      ((Functor.obj modulesSpecToSheaf (tilde M)).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
        (Quiver.Hom.op (homOfLE ⋯))))
    (toOpen M (basicOpen (unop r)) ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf (𝟙 (tilde M))))
        (op (basicOpen (unop r))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
dsimp :
  toOpen
        ((Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
          (op ⊤))
        ⊤ ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op ⊤) =
    𝟙
      ((Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op ⊤))
⊢ NatTrans.app (Iso.hom toTildeΓNatIso) (Functor.obj moduleSpecΓFunctor M) ≫
      CategoryTheory.Functor.map moduleSpecΓFunctor (NatTrans.app fromTildeΓNatTrans M) =
    𝟙 (Functor.obj moduleSpecΓFunctor M)

Tactic:
dsimp [toTildeΓNatIso, fromTildeΓNatTrans, tilde.isoTop, moduleSpecΓFunctor, Sheaf.forget]

Premises used: AlgebraicGeometry.Scheme.Modules.fromTildeΓNatTrans, AlgebraicGeometry.moduleSpecΓFunctor, AlgebraicGeometry.tilde.isoTop, AlgebraicGeometry.tilde.toTildeΓNatIso, TopCat.Sheaf.forget
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
rw :
  (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯)) =
    𝟙
      ((Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op ⊤))
⊢ toOpen
        ((Functor.obj modulesSpecToSheaf M).obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
          (op ⊤))
        ⊤ ≫
      NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map modulesSpecToSheaf M.fromTildeΓ)) (op ⊤) =
    𝟙
      ((Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op ⊤))

Tactic:
rw [toOpen_fromTildeΓ_app]

Premises used: AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
⊢ (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯)) =
    𝟙
      ((Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op ⊤))

Tactic:
(modulesSpecToSheaf.obj M).obj.map_id _

Premises used: Set.Mem, setOf, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_id, CategoryTheory.homOfLE, AlgebraicGeometry.modulesSpecToSheaf, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
⊢ (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).map
      (Quiver.Hom.op (homOfLE ⋯)) =
    𝟙
      ((Functor.obj modulesSpecToSheaf M).obj (P :=
            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
        (op ⊤))

Tactic:
exact (modulesSpecToSheaf.obj M).obj.map_id _

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_id, AlgebraicGeometry.modulesSpecToSheaf, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ IsIso.{u + 1, u + 1} (C := ModuleCat (↑R : Type u) ⥤ ModuleCat (↑R : Type u)) (Iso.hom tilde.toTildeΓNatIso)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ (tilde.functor R).Full

Tactic:
tilde.fullyFaithfulFunctor.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, AlgebraicGeometry.tilde.fullyFaithfulFunctor
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ (tilde.functor R).Faithful

Tactic:
tilde.fullyFaithfulFunctor.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, AlgebraicGeometry.tilde.fullyFaithfulFunctor
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ (tilde.functor R).IsLeftAdjoint

Tactic:
tilde.adjunction.isLeftAdjoint

Premises used: AlgebraicGeometry.tilde.adjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
⊢ Eq.{u + 1} (α := tilde M ⟶ tilde N) (tilde.map 0) 0

Tactic:
(tilde.functor R).map_zero _ _

Premises used: AlgebraicGeometry.tilde, Set.Mem, CategoryTheory.Functor.map_zero, AlgebraicGeometry.tilde.map, AlgebraicGeometry.tilde.functor
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
f g : M ⟶ N
⊢ tilde.map (f + g) = tilde.map f + tilde.map g

Tactic:
(tilde.functor R).map_add

Premises used: AlgebraicGeometry.tilde, Set.Mem, CategoryTheory.Functor.map_add, AlgebraicGeometry.tilde.map, AlgebraicGeometry.tilde.functor
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M N : ModuleCat (↑R : Type u)
f : M ⟶ N
⊢ tilde.map (-f) = -tilde.map f

Tactic:
(tilde.functor R).map_neg

Premises used: AlgebraicGeometry.tilde, Set.Mem, AlgebraicGeometry.tilde.map, AlgebraicGeometry.tilde.functor, CategoryTheory.Functor.map_neg
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
⊢ IsIso M.fromTildeΓ ↔ (tilde.functor R).essImage M

Tactic:
tilde.adjunction.isIso_counit_app_iff_mem_essImage

Premises used: AlgebraicGeometry.Scheme.Modules.fromTildeΓ, AlgebraicGeometry.tilde, Set.Mem, AlgebraicGeometry.tilde.adjunction, CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ IsIso.{u, u + 1} (C := (Spec (CommRingCat.of (↑R : Type u))).Modules) (X :=
    tilde
      (Functor.obj (Sheaf.presheaf (Functor.obj modulesSpecToSheaf (SheafOfModules.unit (Spec R).ringCatSheaf)))
        (op ⊤)))
    (Scheme.Modules.fromTildeΓ (SheafOfModules.unit (Spec R).ringCatSheaf))

Tactic:
isIso_fromTildeΓ_iff.mpr ⟨_, ⟨tildeSelf⟩⟩

Premises used: Iff.mpr, AlgebraicGeometry.tildeSelf, Nonempty.intro, Exists.intro, AlgebraicGeometry.isIso_fromTildeΓ_iff
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
ι : Type u
⊢ IsIso (C := (Spec (CommRingCat.of (↑R : Type u))).Modules) (X :=
    tilde (Functor.obj (Sheaf.presheaf (Functor.obj modulesSpecToSheaf (SheafOfModules.free ι))) (op ⊤)))
    (Scheme.Modules.fromTildeΓ (SheafOfModules.free ι))

Tactic:
isIso_fromTildeΓ_iff.mpr ⟨_, ⟨tildeFinsupp _⟩⟩

Premises used: Iff.mpr, Set.Mem, setOf, Nonempty.intro, AlgebraicGeometry.tildeFinsupp, Exists.intro, AlgebraicGeometry.isIso_fromTildeΓ_iff
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
s : Set (↑M : Type u)
hs : Eq (α := Submodule (↑R : Type u) (↑M : Type u)) (Submodule.span (↑R : Type u) s) ⊤
t : Set ((↑s : Type u) →₀ (↑R : Type u))
ht :
  Submodule.span (↑R : Type u) t =
    LinearMap.ker (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))
⊢ Eq (α := Submodule (↑R : Type u) (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u))
    (LinearMap.ker (M₂ := (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
        LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) (Y :=
        ModuleCat.of (↑R : Type u) (↑M : Type u))
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))))
    (LinearMap.range (M := (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u))
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
        LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
        ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) (Y :=
        ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u)))
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u)
            (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))))

Tactic:
simp [Finsupp.range_linearCombination, ht]

Premises used: Finsupp.range_linearCombination
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
s : Set (↑M : Type u)
hs : Eq (α := Submodule (↑R : Type u) (↑M : Type u)) (Submodule.span (↑R : Type u) s) ⊤
t : Set ((↑s : Type u) →₀ (↑R : Type u))
ht :
  Submodule.span (↑R : Type u) t =
    LinearMap.ker (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))
⊢ Function.Exact (M := (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) (N :=
    (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) (P :=
    (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u)))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u)
              (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) (↑M : Type u))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))

Tactic:
haveI H₁ : Function.Exact
      (ModuleCat.ofHom (Finsupp.linearCombination (α := t) R (↑)))
      (ModuleCat.ofHom (Finsupp.linearCombination (α := s) (M := M) R (↑))) :=
    (LinearMap.exact_iff.mpr (by simp [Finsupp.range_linearCombination, ht]))