-- 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))
simp :
  Eq.{u + 1} (α := tilde (ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) ⟶ tilde M)
    (CategoryStruct.comp (Y := tilde (ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))))
      (tilde.map
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u)
            (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t)))))
      (tilde.map
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))))
    0
⊢ Eq.{u + 1} (α := SheafOfModules.free (↑t : Type u) ⟶ tilde M)
    (CategoryStruct.comp (Y := SheafOfModules.free (↑s : Type u))
      (Iso.inv (tildeFinsupp (↑t : Type u)) ≫
        tilde.map
            (ModuleCat.ofHom
              (Finsupp.linearCombination (↑R : Type u)
                (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t)))) ≫
          Iso.hom (tildeFinsupp (↑s : Type u)))
      (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))))))
    0

Tactic:
simp only [Category.assoc, Iso.hom_inv_id_assoc, Preadditive.IsIso.comp_left_eq_zero]

Premises used: CategoryTheory.Preadditive.IsIso.comp_left_eq_zero, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_assoc