awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 :
  IsUnit (M := Module.End S (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))
rw :
  ∀
    (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)
⊢ IsUnit (M := Module.End R (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))

Tactic:
rw [Module.End.isUnit_iff] at this ⊢

Premises used: Module.End.isUnit_iff
-- 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
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 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)

Tactic:
this
-- 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
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)
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)) ⋯) : 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)

Tactic:
convert! this using 2 with a
-- 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
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)
⊢ 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)) ⋯) : S) :
          Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
      (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)

Tactic:
(IsScalarTower.algebraMap_smul ..).symm

Premises used: IsScalarTower.algebraMap_smul, Eq.symm
-- 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
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)
⊢ 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)) ⋯) : S) :
          Module.End S (LocalizedModule y.asIdeal.primeCompl N)) :
      (a : LocalizedModule y.asIdeal.primeCompl N) → LocalizedModule y.asIdeal.primeCompl N)

Tactic:
exact (IsScalarTower.algebraMap_smul ..).symm

Premises used: IsScalarTower.algebraMap_smul, Eq.symm
-- 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
y : (↑(PrimeSpectrum.Top S) : Type u)
this_1 : Module R N := Module.compHom N σ
this_2 : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
g : LocalizedModule (PrimeSpectrum.comap σ y).asIdeal.primeCompl M →ₗ[R] LocalizedModule y.asIdeal.primeCompl N :=
  IsLocalizedModule.lift (PrimeSpectrum.comap σ y).asIdeal.primeCompl
    (LocalizedModule.mkLinearMap (PrimeSpectrum.comap σ y).asIdeal.primeCompl M)
    ((↑R :
          {S M M₂ : Type u} →
            [inst : Semiring R] →
              [inst_8 : Semiring S] →
                [inst_9 : AddCommMonoid M] →
                  [inst_10 : AddCommMonoid M₂] →
                    [inst_11 : Module R M] →
                      [inst_12 : Module R M₂] →
                        [inst_13 : Module S M] →
                          [inst_14 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ∘ₗ
      f')
    ⋯
r : R
x : Localizations M (PrimeSpectrum.comap σ y)
⊢ g.toFun (r • x) = HSMul.hSMul (α := S) ((σ : (a : R) → S) r : S) (g.toFun x)

Tactic:
simpa [Localizations] using (IsScalarTower.algebraMap_smul ..).symm

Premises used: AlgebraicGeometry.StructureSheaf.Localizations, IsScalarTower.algebraMap_smul, Eq.symm
-- 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 : 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
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)
    ((((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)
⊢ 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)

Tactic:
apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units (S := y.asIdeal.primeCompl)
    (LocalizedModule.mkLinearMap y.asIdeal.primeCompl N) ⟨σ b, b.2⟩)).1

Premises used: Module.End.isUnit_iff, Subtype.mk, And.left, Iff.mp, LocalizedModule.mkLinearMap, Ideal.primeCompl, IsLocalizedModule.map_units, Subtype.val, DFunLike.coe, PrimeSpectrum.asIdeal, Subtype.property
-- 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₁ :
  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)
⊢ 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)

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₁ :
  (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)) ⋯) :
        LocalizedModule y.asIdeal.primeCompl 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)

Tactic:
rw [← (comapFun f y).map_smulₛₗ, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply]

Premises used: AlgebraicGeometry.StructureSheaf.Localizations.comapFun, LocalizedModule.mk_cancel, LocalizedModule.smul'_mk, Submonoid.smul_def, LinearMap.map_smulₛₗ, LocalizedModule.mkLinearMap_apply
-- 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
⊢ (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:
(IsLocalizedModule.lift_apply ..).trans ?_

Premises used: Set.Mem, Quotient.mk', IsLocalizedModule.lift_apply, OreLocalization.oreDiv, Eq.trans