-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f g : (↑R : Type u)ᵒᵖ
i : f ⟶ g
N : ModuleCat (↑(CommRingCat.of (↑R : Type u)) : Type u) := (Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)
n : ℕ
a : (↑R : Type u)
e : unop g ^ n = unop f * a
⊢ IsUnit (M :=
    Module.End (↑R : Type u)
      (↑(Functor.obj
            (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
              (Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
            g) :
        Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑(Functor.obj
                    (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                      (Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                    g) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g) : Type u))
        (unop f) :
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              g) :
          Type u))
have hf : IsUnit
  (HMul.hMul (α :=
    Module.End (↑R : Type u)
      (↑(Functor.obj
            (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
              (Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
            g) :
        Type u))
    (β :=
    Module.End (↑R : Type u)
      (↑(Functor.obj
            (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
              (Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
            g) :
        Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑(Functor.obj
                    (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                      (Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                    g) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g) : Type u))
        (unop f) :
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              g) :
          Type u))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑(Functor.obj
                    (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                      (Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
                    g) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑(((inducedFunctor PrimeSpectrum.basicOpen).op ⋙ (modulesSpecToSheaf.obj M).obj).obj g) : Type u))
        a :
      Module.End (↑R : Type u)
        (↑(Functor.obj
              (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
                (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
              g) :
          Type u)))
Tactic: refine ((Commute.isUnit_mul_iff (b := algebraMap R _ a) (.map (.all _ _) _)).mp ?_).1