awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
rw :
  IsUnit (M := Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
    ((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
            (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
          (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
            Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
        ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
            (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
          f) :
      Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
⊢ Function.Bijective (α := (↑Γ(M, basicOpen f) : Type u)) (β := (↑Γ(M, basicOpen f) : Type u))
    (⇑((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
                (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
              (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
                Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
            ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
                (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
              f) :
          Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
      (a : (↑Γ(M, basicOpen f) : Type u)) → (↑Γ(M, basicOpen f) : Type u))

Tactic:
rw [← Module.End.isUnit_iff]

Premises used: Module.End.isUnit_iff
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
⊢ IsUnit (M := Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
    ((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
            (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
          (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
            Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
        ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
            (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
          f) :
      Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))

Tactic:
(IsLocalization.Away.algebraMap_isUnit _).map _

Premises used: IsUnit.map, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)
⊢ IsUnit (M := Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
    ((algebraMap (↑Γ(Spec R, basicOpen f) : Type u)
            (Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u)) :
          (a : (↑Γ(Spec R, basicOpen f) : Type u)) →
            Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))
        ((algebraMap (↑R : Type u) (↑Γ(Spec R, basicOpen f) : Type u) :
            (a : (↑R : Type u)) → (↑Γ(Spec R, basicOpen f) : Type u))
          f) :
      Module.End (↑Γ(Spec R, basicOpen f) : Type u) (↑Γ(M, basicOpen f) : Type u))

Tactic:
exact (IsLocalization.Away.algebraMap_isUnit _).map _

Premises used: IsUnit.map, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)ᵒᵖ
refine :
  ∀ (x : ↥(Submonoid.powers (unop f))),
    IsUnit (M :=
      Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
          Type u))
      ((algebraMap (↑R : Type u)
              (Module.End (↑R : Type u)
                (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                      (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
                  Type u)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f)))) :
                  Type u))
          (↑x : (↑R : Type u)) :
        Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u))
⊢ Functor.obj
      (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
        (Functor.obj modulesSpecToSheaf (tilde ((Functor.obj modulesSpecToSheaf M).presheaf.obj (op ⊤)))).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
      f ⟶
    Functor.obj
      (Functor.op (inducedFunctor PrimeSpectrum.basicOpen) ⋙
        (Functor.obj modulesSpecToSheaf M).obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))))
      f

Tactic:
refine (ModuleCat.ofHom (IsLocalizedModule.lift (.powers (M := R) f.unop)
          (tilde.toOpen _ (PrimeSpectrum.basicOpen f.unop)).hom
          ((modulesSpecToSheaf.obj M).obj.map (homOfLE le_top).op).hom ?_):)

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.tilde.toOpen, Quiver.Hom.op, IsLocalizedModule.lift, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, le_top, CategoryTheory.homOfLE, Submonoid.powers, ModuleCat.ofHom, ModuleCat.Hom.hom, Opposite.unop, 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
f : (↑R : Type u)ᵒᵖ
change :
  LE.le (α := Submonoid (↑R : Type u)) (Submonoid.powers (unop f))
    (Submonoid.comap (F :=
      (↑R : Type u) →+*
        Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u))
      (algebraMap (↑R : Type u)
        (Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u)))
      (IsUnit.submonoid
        (Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u))))
⊢ ∀ (a : (↑R : Type u)) (b : Membership.mem (γ := Submonoid (↑R : Type u)) (Submonoid.powers (unop f)) a),
    IsUnit (M :=
      Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
          Type u))
      ((algebraMap (↑R : Type u)
              (Module.End (↑R : Type u)
                (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                          CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                      (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
                  Type u)) :
            (a : (↑R : Type u)) →
              Module.End (↑R : Type u)
                (↑((modulesSpecToSheaf.obj M).obj.obj (op ((inducedFunctor PrimeSpectrum.basicOpen).obj (unop f)))) :
                  Type u))
          (↑(Subtype.mk (p := fun (a : (↑R : Type u)) ↦
                Membership.mem (γ := Submonoid (↑R : Type u)) (Submonoid.powers (unop f)) a) a b) :
            (↑R : Type u)) :
        Module.End (↑R : Type u)
          (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf
                      (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                (op (Functor.obj (inducedFunctor PrimeSpectrum.basicOpen) (unop f)))) :
            Type u))

Tactic:
change Submonoid.powers _ ≤ (IsUnit.submonoid _).comap _

Premises used: IsUnit.submonoid, Submonoid.comap, Submonoid.powers
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)ᵒᵖ
⊢ Membership.mem (α :=
    Module.End (↑R : Type u)
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop f)))) :
        Type u))
    (γ :=
    Submonoid
      (Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u)))
    (IsUnit.submonoid
      (Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u)))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                    (op (PrimeSpectrum.basicOpen (unop f)))) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f)))) : Type u))
        (unop f) :
      Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u))

Tactic:
tilde.isUnit_algebraMap_end_basicOpen M f.unop

Premises used: PrimeSpectrum.basicOpen, Set.Mem, setOf, IsUnit, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M : (Spec (CommRingCat.of (↑R : Type u))).Modules
f : (↑R : Type u)ᵒᵖ
⊢ Membership.mem (α :=
    Module.End (↑R : Type u)
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
            (op (PrimeSpectrum.basicOpen (unop f)))) :
        Type u))
    (γ :=
    Submonoid
      (Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u)))
    (IsUnit.submonoid
      (Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u)))
    ((algebraMap (↑R : Type u)
            (Module.End (↑R : Type u)
              (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf
                          (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
                    (op (PrimeSpectrum.basicOpen (unop f)))) :
                Type u)) :
          (a : (↑R : Type u)) →
            Module.End (↑R : Type u)
              (↑((modulesSpecToSheaf.obj M).obj.obj (op (PrimeSpectrum.basicOpen (unop f)))) : Type u))
        (unop f) :
      Module.End (↑R : Type u)
        (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf
                    (Opens.grothendieckTopology ↥(Spec (CommRingCat.of (↑R : Type u))))).obj
              (op (PrimeSpectrum.basicOpen (unop f)))) :
          Type u))

Tactic:
exact tilde.isUnit_algebraMap_end_basicOpen M f.unop

Premises used: AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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 ⊤)
hf :
  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))
⊢ LE.le (α := Submonoid (↑R : Type u)) (Submonoid.powers (unop f))
    (Submonoid.comap (F :=
      (↑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))
      (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)))
      (IsUnit.submonoid
        (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:
simp only [Submonoid.powers_le, Submonoid.mem_comap, IsUnit.mem_submonoid_iff]

Premises used: Submonoid.mem_comap, IsUnit.mem_submonoid_iff, Submonoid.powers_le
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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 : ℕ), unop f ∣ unop g ^ n

Tactic:
simpa only [Ideal.mem_radical_iff, Ideal.mem_span_singleton] using
              (basicOpen_le_basicOpen_iff _ _).mp (i.1.hom.le)

Premises used: Quiver.Hom.le, Iff.mp, PrimeSpectrum.basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, CategoryTheory.InducedCategory.Hom.hom, Ideal.mem_span_singleton, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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))

Tactic:
((Commute.isUnit_mul_iff (b := algebraMap R _ a) (.map (.all _ _) _)).mp ?_).1

Premises used: And.left, Commute.isUnit_mul_iff, Iff.mp, Commute.map, Commute.all
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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
    (HPow.hPow (α :=
      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 g) :
        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))
      n)

Tactic:
(tilde.isUnit_algebraMap_end_basicOpen M g.unop).pow n

Premises used: PrimeSpectrum.basicOpen, Set.Mem, setOf, IsUnit.pow, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
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
    (HPow.hPow (α :=
      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 g) :
        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))
      n)

Tactic:
exact (tilde.isUnit_algebraMap_end_basicOpen M g.unop).pow n

Premises used: IsUnit.pow, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Opposite.unop