-- 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)))
H₁ :
  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))
h₁ : IsColimit
  (CokernelCofork.ofπ
    (ModuleCat.ofHom (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))
    ⋯) :=
  ModuleCat.isColimitCokernelCofork
    (ModuleCat.ofHom
      (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))
    (ModuleCat.ofHom (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))) H₁
    ⋯
⊢ Iso.hom (tildeFinsupp (↑s : Type u)) ≫
      Cofork.π
        (CokernelCofork.ofπ
          (Iso.inv (tildeFinsupp (↑s : Type u)) ≫
            tilde.map
              (ModuleCat.ofHom
                (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))))
          ⋯) =
    Cofork.π
        ((CokernelCofork.ofπ
              (ModuleCat.ofHom
                (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))
              ⋯).map
          (tilde.functor R)) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            parallelPair (X := (tilde.functor R).obj (ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))))
              (Y := (tilde.functor R).obj (ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))))
              ((tilde.functor R).map
                (ModuleCat.ofHom
                  (Finsupp.linearCombination (↑R : Type u)
                    (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t)))))
              0)
            ((CokernelCofork.ofπ
                  (ModuleCat.ofHom
                    (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))
                  ⋯).map
              (tilde.functor R))))

Tactic:
simp