awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
S : Type u
inst_5 : CommRing S
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this_3 : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this :
  Function.Bijective (α := LocalizedModule y.asIdeal.primeCompl N) (β := LocalizedModule y.asIdeal.primeCompl N)
    (⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
              (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
            (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑x : R)) ⋯) : S) :
          Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
      (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
⊢ Function.Bijective (α := LocalizedModule y.asIdeal.primeCompl N) (β := LocalizedModule y.asIdeal.primeCompl N)
    (⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N)) :
              (a : R) → Module.End R (LocalizedModule y.asIdeal.primeCompl N))
            (↑x : R) :
          Module.End R (LocalizedModule y.asIdeal.primeCompl N)) :
      (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
have h : Eq (α := LocalizedModule y.asIdeal.primeCompl N → LocalizedModule y.asIdeal.primeCompl N)
  (⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N)) :
            (a : R) → Module.End R (LocalizedModule y.asIdeal.primeCompl N))
          (↑x : R) :
        Module.End R (LocalizedModule y.asIdeal.primeCompl N)) :
    (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
  (⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
            (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
          (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑x : R)) sorry) : S) :
        Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
    (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
Tactic: convert! this using 2 with a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (hypothesis)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this : Algebra R S := σ.toAlgebra
⊢ Eq (α := Localizations N y)
    ((comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y) (LocalizedModule.mk a b) :
      Localizations N y)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
      LocalizedModule y.asIdeal.primeCompl N)
have this₁ : IsScalarTower R S N
Tactic: haveI : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ Eq (α := Localizations N y)
    ((comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y) (LocalizedModule.mk a b) :
      Localizations N y)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
      LocalizedModule y.asIdeal.primeCompl N)
have a₁ : Eq (α := LocalizedModule y.asIdeal.primeCompl N)
  ((((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
              (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
            (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) : S) :
          Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
        (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
      ((comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y) (LocalizedModule.mk a b)) :
    LocalizedModule y.asIdeal.primeCompl N)
  ((((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
              (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
            (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) : S) :
          Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
        (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
      (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry)) :
    LocalizedModule y.asIdeal.primeCompl N)
Tactic: apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
    (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ b, b.2⟩)).1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ Eq (α := LocalizedModule y.asIdeal.primeCompl N)
    ((((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
                (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
              (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) : S) :
            Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
          (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
        ((comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y)
          (LocalizedModule.mk a b)) :
      LocalizedModule y.asIdeal.primeCompl N)
    ((((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
                (a : S) → Module.End S (LocalizedModule y.asIdeal.primeCompl N))
              (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) : S) :
            Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
          (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)
        (LocalizedModule.mk ((f : (a : M) → N) a)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯)) :
      LocalizedModule y.asIdeal.primeCompl N)
have a₁ : HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
    ((comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y) (LocalizedModule.mk a b) :
      Localizations N y) =
  HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) :
      LocalizedModule y.asIdeal.primeCompl N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
      ((comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y) (LocalizedModule.mk a b) :
        Localizations N y) =
    HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
      (LocalizedModule.mk ((f : (a : M) → N) a)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
        LocalizedModule y.asIdeal.primeCompl N)
have a₁ : (comapFun f y : (a : Localizations M (PrimeSpectrum.comap σ y)) → Localizations N y)
    ((LocalizedModule.mkLinearMap (Ideal.primeCompl (Ideal.comap σ y.asIdeal)) M :
        (a : M) → LocalizedModule (Ideal.comap σ y.asIdeal).primeCompl M)
      a) =
  HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) :
      LocalizedModule y.asIdeal.primeCompl N)
Tactic: rw [← (comapFun f y).map_smulₛₗ, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ (IsLocalizedModule.lift (Ideal.primeCompl (Ideal.comap σ y.asIdeal))
          (LocalizedModule.mkLinearMap (Ideal.primeCompl (Ideal.comap σ y.asIdeal)) M)
          ((↑R :
                {S M M₂ : Type u} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ
            { toAddHom := f.toAddHom, map_smul' := ⋯ : M →ₗ[R] N })
          ⋯ :
        (a : LocalizedModule (Ideal.comap σ y.asIdeal).primeCompl M) → LocalizedModule y.asIdeal.primeCompl N)
      (LocalizedModule.mk a 1) =
    HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
      (LocalizedModule.mk ((f : (a : M) → N) a)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
        LocalizedModule y.asIdeal.primeCompl N)
have a₁ : ((↑R :
            {S M M₂ : Type u} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ
        { toAddHom := f.toAddHom, map_smul' := sorry : M →ₗ[R] N } :
      (a : M) → LocalizedModule y.asIdeal.primeCompl N)
    a =
  HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) :
      LocalizedModule y.asIdeal.primeCompl N)
Tactic: refine (IsLocalizedModule.lift_apply ..).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ ((↑R :
              {S M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ
          { toAddHom := f.toAddHom, map_smul' := ⋯ : M →ₗ[R] N } :
        (a : M) → LocalizedModule y.asIdeal.primeCompl N)
      a =
    HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
      (LocalizedModule.mk ((f : (a : M) → N) a)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
        LocalizedModule y.asIdeal.primeCompl N)
have a₁ : LocalizedModule.mk ((f : (a : M) → N) a) 1 =
  HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) :
      LocalizedModule y.asIdeal.primeCompl N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : (↑(PrimeSpectrum.Top S) : Type u)
a : M
b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
⊢ LocalizedModule.mk ((f : (a : M) → N) a) 1 =
    HSMul.hSMul (α := S) (β := LocalizedModule y.asIdeal.primeCompl N) ((σ : (a : R) → S) (↑b : R) : S)
      (LocalizedModule.mk ((f : (a : M) → N) a)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
        LocalizedModule y.asIdeal.primeCompl N)
have a₁ : Eq (α := LocalizedModule y.asIdeal.primeCompl N)
  (LocalizedModule.mk
      (HSMul.hSMul (α := ↥y.asIdeal.primeCompl) (β := N)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry :
          ↥y.asIdeal.primeCompl)
        ((f : (a : M) → N) a : N))
      (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) :
    LocalizedModule y.asIdeal.primeCompl N)
  (LocalizedModule.mk (HSMul.hSMul (α := S) (β := N) ((σ : (a : R) → S) (↑b : R) : S) ((f : (a : M) → N) a : N))
      (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) sorry) :
    LocalizedModule y.asIdeal.primeCompl N)
Tactic: rw [← LocalizedModule.mk_cancel ⟨σ b.1, b.2⟩, LocalizedModule.smul'_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (hypothesis)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
hs :
  PrelocalPredicate.pred (T := Localizations M)
    (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) s
this_1 : Module R N := Module.compHom N σ
this : Algebra R S := σ.toAlgebra
⊢ PrelocalPredicate.pred (T := Localizations N)
    (LocalPredicate.toPrelocalPredicate (T := Localizations N) (isLocallyFraction S N)) (comapFun f U V hUV s)
have this₁ : IsScalarTower R S N
Tactic: haveI : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u
inst_3 : CommRing S
N : Type u
inst_4 : AddCommGroup N
inst_5 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))
hs :
  PrelocalPredicate.pred (T := Localizations M)
    (LocalPredicate.toPrelocalPredicate (T := Localizations M) (isLocallyFraction R M)) s
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
p : (↑(PrimeSpectrum.Top S) : Type u)
hpV : p ∈ V
⊢ ∃ (V_1 : Opens (↑(PrimeSpectrum.Top S) : Type u)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦ x ∈ V) p hpV) :
        (↑(PrimeSpectrum.Top S) : Type u)) ∈
      V_1)
    (i : V_1 ⟶ V),
    PrelocalPredicate.pred (T := Localizations N) (isFractionPrelocal S N) (U := V_1) fun (x : ↥V_1) ↦
      comapFun f U V hUV s ((i : (a : ↥V_1) → ↥V) x)
have obtain : ∀ (W : Opens (↑(PrimeSpectrum.Top R) : Type u))
  (m :
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) sorry) :
        (↑(PrimeSpectrum.Top R) : Type u)) ∈
      W)
  (iWU : W ⟶ U) (a : M) (b : R)
  (h_frac :
    ∀ (x : ↥W),
      ∃ (hs : b ∉ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal),
        Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          ((fun (x : ↥W) ↦
              (s ((iWU : (a : ↥W) → ↥U) x) :
                Localizations (R := R) M (↑((iWU : (a : ↥W) → ↥U) x) : (↑(PrimeSpectrum.Top R) : Type u))))
            x)
          (LocalizedModule.mk a
            (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) b
              hs))),
  ∃ (V_1 : Opens (↑(PrimeSpectrum.Top S) : Type u)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top S) : Type u)) ↦ x ∈ V) p hpV) :
        (↑(PrimeSpectrum.Top S) : Type u)) ∈
      V_1)
    (i : V_1 ⟶ V),
    PrelocalPredicate.pred (T := Localizations N) (isFractionPrelocal S N) (U := V_1) fun (x : ↥V_1) ↦
      comapFun f U V hUV s ((i : (a : ↥V_1) → ↥V) x)
Tactic: obtain ⟨W, m, iWU, a, b, h_frac⟩ := hs ⟨PrimeSpectrum.comap σ p, hUV hpV⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R M A : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
S : Type u
inst_5 : CommRing S
N : Type u
inst_6 : AddCommGroup N
inst_7 : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
x : ↥(unop (op V))
⊢ (↑(Subtype.mk (p := fun (f : (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ↦
            PrelocalPredicate.pred (T := Localizations N)
              (LocalPredicate.toPrelocalPredicate (T := Localizations N) (isLocallyFraction S N)) f)
            (comapFun f U V hUV
              (↑(r • m) : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
            ⋯) :
        (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x =
    (↑(HSMul.hSMul (α := S) ((σ : (a : R) → S) r : S)
            (Subtype.mk (p :=
              fun (f : (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ↦
              PrelocalPredicate.pred (T := Localizations N)
                (LocalPredicate.toPrelocalPredicate (T := Localizations N) (isLocallyFraction S N)) f)
              (comapFun f U V hUV
                (↑m : (x : ↥(unop (op U))) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u))))
              ⋯)) :
        (x : ↥(unop (op V))) → Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
      x
have dsimp : (Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
      (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
        Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
    (r •
      (↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
          (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) sorry)) =
  HSMul.hSMul (α := S) (β := Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u))) ((σ : (a : R) → S) r : S)
    ((Localizations.comapFun f (↑x : (↑(PrimeSpectrum.Top S) : Type u)) :
          (a : Localizations M (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u)))) →
            Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
        ((↑m : (x : ↥U) → Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U)
            (PrimeSpectrum.comap σ (↑x : (↑(PrimeSpectrum.Top S) : Type u))) sorry)) :
      Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
Tactic: dsimp [comapFun]