awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
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' := ⋯ : 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)
⊢ (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)

Tactic:
refine (IsLocalizedModule.lift_apply ..).trans ?_

Premises used: IsLocalizedModule.lift_apply, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
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)) ⋯) :
        LocalizedModule y.asIdeal.primeCompl 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)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
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)) ⋯ :
            ↥y.asIdeal.primeCompl)
          ((f : (a : M) → N) a : N))
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
      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)) ⋯) :
      LocalizedModule y.asIdeal.primeCompl 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)

Tactic:
rw [← LocalizedModule.mk_cancel ⟨σ b.1, b.2⟩, LocalizedModule.smul'_mk]

Premises used: LocalizedModule.mk_cancel, LocalizedModule.smul'_mk, Subtype.mk, Subtype.val, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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)
    (LocalizedModule.mk
        (HSMul.hSMul (α := ↥y.asIdeal.primeCompl) (β := N)
          (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯ :
            ↥y.asIdeal.primeCompl)
          ((f : (a : M) → N) a : N))
        (Subtype.mk (p := fun (x : S) ↦ x ∈ y.asIdeal.primeCompl) ((σ : (a : R) → S) (↑b : R)) ⋯) :
      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)) ⋯) :
      LocalizedModule y.asIdeal.primeCompl N)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
⊢ IsScalarTower R S N

Tactic:
haveI : IsScalarTower R S N := .of_algebraMap_smul fun _ _ ↦ rfl
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
obtain :
  ∀ (W : Opens (↑(PrimeSpectrum.Top R) : Type u))
    (m :
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
          (↑(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)
⊢ ∃ (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⟩

Premises used: Subtype.mk, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
m :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
      (↑(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:
⟨⟨_, (PrimeSpectrum.continuous_comap σ).isOpen_preimage _ W.2⟩ ⊓ V,
    ⟨m, hpV⟩, Opens.infLERight _ _, f a, σ b, ?_⟩

Premises used: PrimeSpectrum.continuous_comap, TopologicalSpace.Opens.mk, And.intro, Exists.intro, TopologicalSpace.Opens.is_open', TopologicalSpace.Opens.infLERight, Continuous.isOpen_preimage, DFunLike.coe, Min.min
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
m :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
      (↑(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))
q : (↑(PrimeSpectrum.Top S) : Type u)
hqW :
  q ∈
    (↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ : Opens (↑(PrimeSpectrum.Top S) : Type u) } :
      Set (↑(PrimeSpectrum.Top S) : Type u))
hqV : q ∈ (↑V : Set (↑(PrimeSpectrum.Top S) : Type u))
⊢ b ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal

Tactic:
obtain ⟨hs, H⟩ := h_frac ⟨PrimeSpectrum.comap σ q, hqW⟩

Premises used: Subtype.mk, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
m :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
      (↑(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))
q : (↑(PrimeSpectrum.Top S) : Type u)
hqW :
  q ∈
    (↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ : Opens (↑(PrimeSpectrum.Top S) : Type u) } :
      Set (↑(PrimeSpectrum.Top S) : Type u))
hqV : q ∈ (↑V : Set (↑(PrimeSpectrum.Top S) : Type u))
hs₁ :
  b ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
⊢ Eq (α :=
    Localizations M
      (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(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))))
      (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW))
    (LocalizedModule.mk a
      (Subtype.mk (p := fun (x : R) ↦
        x ∈
          (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
                (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
        b hs₁))

Tactic:
obtain ⟨hs, H⟩ := h_frac ⟨PrimeSpectrum.comap σ q, hqW⟩

Premises used: Subtype.mk, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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_1 :
  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
W : Opens (↑(PrimeSpectrum.Top R) : Type u)
m :
  (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ p) ⋯) :
      (↑(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))
q : (↑(PrimeSpectrum.Top S) : Type u)
hqW :
  q ∈
    (↑{ carrier := PrimeSpectrum.comap σ ⁻¹' W.carrier, is_open' := ⋯ : Opens (↑(PrimeSpectrum.Top S) : Type u) } :
      Set (↑(PrimeSpectrum.Top S) : Type u))
hqV : q ∈ (↑V : Set (↑(PrimeSpectrum.Top S) : Type u))
hs :
  b ∉
    (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ W) (PrimeSpectrum.comap σ q) hqW) :
        (↑(PrimeSpectrum.Top R) : Type u)).asIdeal
H :
  Eq (α := Localizations M (PrimeSpectrum.comap σ q))
    (s (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ q) ⋯) :
      Localizations M
        (↑(Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ U) (PrimeSpectrum.comap σ q) ⋯) :
          (↑(PrimeSpectrum.Top R) : Type u)))
    (LocalizedModule.mk a
      (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap σ q.asIdeal)) x)
        b hs))
⊢ Eq (α := Localizations N q)
    ((Localizations.comapFun f q : (a : Localizations M (PrimeSpectrum.comap σ q)) → Localizations N q)
        (LocalizedModule.mk a
          (Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submonoid R) (Ideal.primeCompl (Ideal.comap σ q.asIdeal)) x) b hs)) :
      Localizations N q)
    (LocalizedModule.mk ((f : (a : M) → N) a)
        (Subtype.mk (p := fun (x : S) ↦ x ∈ q.asIdeal.primeCompl) ((σ : (a : R) → S) b) hs) :
      LocalizedModule q.asIdeal.primeCompl N)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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))
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))) ⋯)) =
    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))) ⋯)) :
        Localizations N (↑x : (↑(PrimeSpectrum.Top S) : Type u)))
⊢ (↑(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

Tactic:
dsimp [comapFun]

Premises used: AlgebraicGeometry.StructureSheaf.comapFun