-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
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))
⊢ 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
have 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
Tactic: simp only [Category.assoc, Iso.hom_inv_id_assoc, Preadditive.IsIso.comp_left_eq_zero]