awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ (↑(localized' S p f (M' ⊓ M'')) : Set N) = (↑(localized' S p f M' ⊓ localized' S p f M'') : Set N)

Tactic:
apply SetLike.ext'_iff.mp <| Submodule.localized₀_inf p f M' M''

Premises used: Iff.mp, SetLike.ext'_iff, Submodule.localized₀_inf
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
⊢ Eq (α := Submodule S N) (localized' S p f (⨆ (i : ι), g i)) (⨆ (i : ι), localized' S p f (g i))

Tactic:
GaloisConnection.l_iSup (localized'gi S p f).gc

Premises used: Submodule.localized'gi, GaloisConnection.l_iSup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
⊢ Eq (α := Submodule S N) (localized' S p f (⨆ (i : ι), g i)) (⨆ (i : ι), localized' S p f (g i))

Tactic:
exact GaloisConnection.l_iSup (localized'gi S p f).gc

Premises used: Submodule.localized'gi, GaloisConnection.l_iSup, GaloisInsertion.gc
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
this : Module.{u_1, u_4} (Localization (M := R) p) N := IsLocalizedModule.module p f
⊢ IsScalarTower R (Localization (M := R) p) N

Tactic:
have : IsScalarTower R (Localization p) N := IsLocalizedModule.isScalarTower_module p f
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
this_1 : Module.{u_1, u_4} (Localization (M := R) p) N := IsLocalizedModule.module p f
this : IsScalarTower R (Localization (M := R) p) N
⊢ localized₀ p f (⨆ (i : ι), g i) = ⨆ (i : ι), localized₀ p f (g i)

Tactic:
simpa using congr_arg (restrictScalars R) (localized'_iSup (Localization p) p f g)

Premises used: Submodule.restrictScalars, Submodule.localized'_iSup, Localization, congr_arg
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
rw : localized₀ p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)) = sSup (localized₀ p f '' s)
rw₁ : ⨆ (i : (↑s : Type u_3)), localized₀ p f (↑i : Submodule R M) = sSup (localized₀ p f '' s)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := Submodule R N) (⨆ (i : (↑s : Type u_3)), localized₀ p f (↑i : Submodule R M))
    (⨆ (a : (↑s : Type u_3)), localized₀ p f (↑a : Submodule R M))
⊢ localized₀ p f (sSup s) = sSup (localized₀ p f '' s)

Tactic:
rw [sSup_eq_iSup', localized₀_iSup, sSup_image']

Premises used: Submodule.localized₀_iSup, sSup_image', sSup_eq_iSup'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
⊢ (localized₀FrameHom p f : (a : Submodule R M) → Submodule R N) M' = localized₀ p f M'

Tactic:
rfl

Premises used: rfl, Submodule.localized₀
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
s : Set (Submodule R M)
rw :
  Eq (α := Submodule S N) (localized' S p f (⨆ (a : (↑s : Type u_3)), (↑a : Submodule R M)))
    (sSup (localized' S p f '' s))
rw₁ :
  Eq (α := Submodule S N) (⨆ (i : (↑s : Type u_3)), localized' S p f (↑i : Submodule R M))
    (sSup (localized' S p f '' s))
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := Submodule S N) (⨆ (i : (↑s : Type u_3)), localized' S p f (↑i : Submodule R M))
    (⨆ (a : (↑s : Type u_3)), localized' S p f (↑a : Submodule R M))
⊢ Eq (α := Submodule S N) (localized' S p f (sSup s)) (sSup (localized' S p f '' s))

Tactic:
rw [sSup_eq_iSup', localized'_iSup, sSup_image']

Premises used: Submodule.localized'_iSup, sSup_image', sSup_eq_iSup'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
⊢ Eq.{u_4 + 1} (α := Submodule S N)
    (((localized'FrameHom S p f : FrameHom.{u_3, u_4} (Submodule R M) (Submodule S N)) :
          (a : Submodule R M) → Submodule S N)
        M' :
      Submodule S N)
    (localized' S p f M' : Submodule S N)

Tactic:
rfl

Premises used: Submodule.localized', rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
s : Set M
rw :
  Eq.{u_4 + 1} (α := Submodule S N) (span S ((⇑f : (a : M) → N) '' (↑(span R s) : Set M)))
    (span S ((⇑f : (a : M) → N) '' s))
rw₁ : Eq (α := Submodule S N) (span S (↑(map f (span R s)) : Set N)) (span S ((⇑f : (a : M) → N) '' s))
rw₂ : Eq (α := Submodule S N) (span S (↑(span R ((⇑f : (a : M) → N) '' s)) : Set N)) (span S ((⇑f : (a : M) → N) '' s))
rw₃ rw₄ : Eq.{u_4 + 1} (α := Submodule S N) (span S ((⇑f : (a : M) → N) '' s)) (span S ((⇑f : (a : M) → N) '' s))
⊢ Eq (α := Submodule S N) (localized' S p f (span R s)) (span S ((⇑f : (a : M) → N) '' s))

Tactic:
rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]

Premises used: Submodule.span_span_of_tower, Submodule.localized'_eq_span, Submodule.map_span, Submodule.map_coe
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : localized₀ p f (I • M') ≤ I • localized₀ p f M'
a₁ : I • localized₀ p f M' ≤ localized₀ p f (I • M')
⊢ localized₀ p f (I • M') = I • localized₀ p f M'

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ IsLocalizedModule.mk' f a s ∈ I • localized₀ p f M'

Tactic:
Submodule.smul_induction_on ha ?_ ?_

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
a₁ : ∀ r ∈ I, ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'
a₂ :
  ∀ (x y : M),
    IsLocalizedModule.mk' f x s ∈ I • localized₀ p f M' →
      IsLocalizedModule.mk' f y s ∈ I • localized₀ p f M' → IsLocalizedModule.mk' f (x + y) s ∈ I • localized₀ p f M'
⊢ IsLocalizedModule.mk' f a s ∈ I • localized₀ p f M'

Tactic:
refine Submodule.smul_induction_on ha ?_ ?_
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
a₁ : r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'
⊢ IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

Tactic:
rw [IsLocalizedModule.mk'_smul]

Premises used: IsLocalizedModule.mk'_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'

Tactic:
Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩

Premises used: And.intro, Exists.intro, Submodule.smul_mem_smul, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'

Tactic:
exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
⊢ ∀ (x y : M),
    IsLocalizedModule.mk' f x s ∈ I • localized₀ p f M' →
      IsLocalizedModule.mk' f y s ∈ I • localized₀ p f M' → IsLocalizedModule.mk' f (x + y) s ∈ I • localized₀ p f M'

Tactic:
simp +contextual only [IsLocalizedModule.mk'_add, add_mem, implies_true]

Premises used: IsLocalizedModule.mk'_add, AddMemClass.add_mem, implies_true
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
⊢ I • localized₀ p f M' ≤ localized₀ p f (I • M')

Tactic:
Submodule.smul_le.mpr ?_

Premises used: Iff.mpr, Submodule.smul_le
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : ∀ r ∈ I, ∀ n ∈ localized₀ p f M', r • n ∈ localized₀ p f (I • M')
⊢ I • localized₀ p f M' ≤ localized₀ p f (I • M')

Tactic:
refine Submodule.smul_le.mpr ?_

Premises used: Iff.mpr, Submodule.smul_le
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
r : R
hr : r ∈ I
a : M
ha : a ∈ M'
s : ↥p
a₁ : IsLocalizedModule.mk' f (r • a) s ∈ localized₀ p f (I • M')
⊢ r • IsLocalizedModule.mk' f a s ∈ localized₀ p f (I • M')

Tactic:
rw [← IsLocalizedModule.mk'_smul]

Premises used: IsLocalizedModule.mk'_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
r : R
hr : r ∈ I
a : M
ha : a ∈ M'
s : ↥p
⊢ IsLocalizedModule.mk' f (r • a) s ∈ localized₀ p f (I • M')

Tactic:
⟨_, Submodule.smul_mem_smul hr ha, s, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Submodule.smul_mem_smul, rfl
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst_5 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
r : R
hr : r ∈ I
a : M
ha : a ∈ M'
s : ↥p
⊢ IsLocalizedModule.mk' f (r • a) s ∈ localized₀ p f (I • M')

Tactic:
exact ⟨_, Submodule.smul_mem_smul hr ha, s, rfl⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
⊢ restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N') =
    HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')

Tactic:
le_antisymm (fun x hx ↦ ?_) (Submodule.smul_le.mpr fun r hr n hn ↦ ?_)

Premises used: Iff.mpr, le_antisymm, Submodule.smul_le
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx :
  Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) x
⊢ x ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')

Tactic:
smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ fun _ _ ↦ add_mem

Premises used: Algebra.linearMap, Submodule.localized', Submodule.smul_induction_on, Submodule.restrictScalars_mem, Iff.mp, HSMul.hSMul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx :
  Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) x
refine_1 :
  ∀ (r : S),
    Membership.mem (γ := Submodule S S) (localized' S p (Algebra.linearMap R S) I) r →
      ∀ n ∈ N', r • n ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')
⊢ x ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')

Tactic:
refine smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ fun _ _ ↦ add_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx :
  Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) x
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
refine_1 : r • IsLocalization.mk' S 1 s • n ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r s • n ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')

Tactic:
rw [← IsLocalization.mk'_eq_mk', IsLocalization.mk'_eq_mul_mk'_one, mul_smul, algebraMap_smul]

Premises used: IsLocalization.mk'_eq_mul_mk'_one, IsLocalization.mk'_eq_mk', algebraMap_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx :
  Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) x
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ r • IsLocalization.mk' S 1 s • n ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')

Tactic:
smul_mem_smul hr ((Submodule.restrictScalars_mem _ _ _).mpr <| smul_mem _ _ hn)

Premises used: Iff.mpr, Submodule.restrictScalars_mem, Submodule.smul_mem_smul, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx :
  Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) x
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ r • IsLocalization.mk' S 1 s • n ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')

Tactic:
exact smul_mem_smul hr ((Submodule.restrictScalars_mem _ _ _).mpr <| smul_mem _ _ hn)

Premises used: Iff.mpr, Submodule.restrictScalars_mem, Submodule.smul_mem_smul, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : Membership.mem (γ := Submodule R N) (restrictScalars R N') n
refine_2 :
  HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) n ∈
    HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N'
⊢ Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) (r • n)

Tactic:
rw [← algebraMap_smul S, Submodule.restrictScalars_mem]

Premises used: algebraMap_smul, Submodule.restrictScalars_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : Membership.mem (γ := Submodule R N) (restrictScalars R N') n
⊢ IsLocalizedModule.mk' (S := p) (Algebra.linearMap R S) r 1 = (algebraMap R S : (a : R) → S) r

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid N
inst_3 : Module R N
inst_4 : Algebra R S
inst_5 : Module S N
inst_6 : IsScalarTower R S N
p : Submonoid R
inst_7 : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : Membership.mem (γ := Submodule R N) (restrictScalars R N') n
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) n ∈
    HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N'

Tactic:
exact Submodule.smul_mem_smul ⟨_, hr, 1, by simp⟩ hn
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
simp_rw :
  restrictScalars R (localized' S p f (I • M')) =
    HSMul.hSMul (β := Submodule R N) I (restrictScalars R (localized' S p f M'))
simp_rw₁ : localized₀ p f (I • M') = I • localized₀ p f M'
⊢ Eq (α := Submodule R N) (restrictScalars R (localized' S p f (I • M')))
    (restrictScalars R
      (HSMul.hSMul (α := Submodule S S) (β := Submodule S N) (localized' S p (Algebra.linearMap R S) I)
        (localized' S p f M')))

Tactic:
simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]

Premises used: Submodule.localized₀_smul, Submodule.restrictScalars_localized', Submodule.restrictScalars_localized'_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' (S := p) f x 1 = (f : (a : M) → N) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Submodule
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Algebra R S
inst_7 : Module S N
inst_8 : IsScalarTower R S N
p : Submonoid R
inst_9 : IsLocalization p S
f : M →ₗ[R] N
inst_10 : IsLocalizedModule p f
M' M'' : Submodule R M
x : ↥p
simp_rw :
  Function.Bijective.{u_4 + 1, u_4 + 1} (α := ↥(localized₀ p f M')) (β := ↥(localized₀ p f M'))
    (⇑((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
          Module.End R ↥(localized₀ p f M')) :
      (a : ↥(localized₀ p f M')) → ↥(localized₀ p f M'))
⊢ IsUnit.{u_4} (M := Module.End R ↥(localized₀ p f M'))
    ((algebraMap R (Module.End R ↥(localized₀ p f M')) : (a : R) → Module.End R ↥(localized₀ p f M')) (↑x : R) :
      Module.End R ↥(localized₀ p f M'))

Tactic:
simp_rw [Module.End.isUnit_iff]

Premises used: Module.End.isUnit_iff