awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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))
⊢ Eq (α := Submodule S N) (localized' S p f (span R s)) (span S ((⇑f : (a : M) → N) '' s))
have rw₂ : Eq (α := Submodule S N) (span S (↑(span R ((⇑f : (a : M) → N) '' s)) : Set N)) (span S ((⇑f : (a : M) → N) '' s))
Tactic: rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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))
⊢ Eq (α := Submodule S N) (localized' S p f (span R s)) (span S ((⇑f : (a : M) → N) '' s))
have rw₃ : Eq.{u_4 + 1} (α := Submodule S N) (span S ((⇑f : (a : M) → N) '' s)) (span S ((⇑f : (a : M) → N) '' s))
Tactic: rw [localized'_eq_span, ← map_coe, map_span, span_span_of_tower]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ localized₀ p f (I • M') = I • localized₀ p f M'
have a : localized₀ p f (I • M') ≤ I • localized₀ p f M'
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'
⊢ localized₀ p f (I • M') = I • localized₀ p f M'
have a₁ : I • localized₀ p f M' ≤ localized₀ p f (I • M')
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'
have a₁ : ∀ r ∈ I, ∀ n ∈ M', IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'
Tactic: refine Submodule.smul_induction_on ha ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'
⊢ IsLocalizedModule.mk' f a s ∈ I • localized₀ p f M'
have 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'
Tactic: refine Submodule.smul_induction_on ha ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'
⊢ IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'
have a₁ : r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'
Tactic: rw [IsLocalizedModule.mk'_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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')
have a : ∀ r ∈ I, ∀ n ∈ localized₀ p f M', r • n ∈ localized₀ p f (I • M')
Tactic: refine Submodule.smul_le.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ r • IsLocalizedModule.mk' f a s ∈ localized₀ p f (I • M')
have a₁ : IsLocalizedModule.mk' f (r • a) s ∈ localized₀ p f (I • M')
Tactic: rw [← IsLocalizedModule.mk'_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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')
have 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')
Tactic: refine smul_induction_on ((Submodule.restrictScalars_mem _ _ _).mp hx) ?_ fun _ _ ↦ add_mem
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r s • n ∈ HSMul.hSMul (β := Submodule R N) I (restrictScalars R N')
have refine_1 : r • IsLocalization.mk' S 1 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ Membership.mem (γ := Submodule R N)
    (restrictScalars R (HSMul.hSMul (α := Submodule S S) (localized' S p (Algebra.linearMap R S) I) N')) (r • n)
have 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'
Tactic: rw [← algebraMap_smul S, Submodule.restrictScalars_mem]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ 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')))
have simp_rw : restrictScalars R (localized' S p f (I • M')) =
  HSMul.hSMul (β := Submodule R N) I (restrictScalars R (localized' S p f M'))
Tactic: simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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'))
⊢ 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')))
have simp_rw₁ : localized₀ p f (I • M') = I • localized₀ p f M'
Tactic: simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ 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'))
have 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'))
Tactic: simp_rw [Module.End.isUnit_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
⊢ 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'))
have left : Function.Injective.{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'))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
left :
  Function.Injective.{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'))
⊢ 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'))
have right : Function.Surjective.{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'))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
m : M
hm : m ∈ M'
s : ↥p
⊢ ∃ (a : ↥(localized₀ p f M')),
    Eq (α := ↥(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'))
          a :
        ↥(localized₀ p f M'))
      (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯ : ↥(localized₀ p f M'))
have right : (↑((((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'))
        (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) sorry)) :
    N) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) sorry) : N)
Tactic: refine ⟨⟨IsLocalizedModule.mk' f m (s * x), ⟨_, hm, _, rfl⟩⟩, Subtype.ext ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
m : M
hm : m ∈ M'
s : ↥p
⊢ (↑((((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'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
have right : (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (↑x : R)
        (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) sorry)) :
    N) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) sorry) : N)
Tactic: rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
m : M
hm : m ∈ M'
s : ↥p
right :
  (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (↑x : R)
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
⊢ (↑((((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'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
have right₁ : (↑x : R) • (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) sorry) : N) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) sorry) : N)
Tactic: rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
m : M
hm : m ∈ M'
s : ↥p
right :
  (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (↑x : R)
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₁ :
  (↑x : R) • (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
⊢ (↑((((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'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
have right₂ : IsLocalizedModule.mk' f ((↑x : R) • m) (s * x) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) sorry) : N)
Tactic: rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
m : M
hm : m ∈ M'
s : ↥p
right :
  (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (↑x : R)
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₁ :
  (↑x : R) • (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₂ :
  IsLocalizedModule.mk' f ((↑x : R) • m) (s * x) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
⊢ (↑((((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'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
have right₃ : IsLocalizedModule.mk' f (x • m) (s * x) =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) sorry) : N)
Tactic: rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
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
m : M
hm : m ∈ M'
s : ↥p
right :
  (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (↑x : R)
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₁ :
  (↑x : R) • (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯) : N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₂ :
  IsLocalizedModule.mk' f ((↑x : R) • m) (s * x) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
right₃ :
  IsLocalizedModule.mk' f (x • m) (s * x) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
⊢ (↑((((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'))
          (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m (s * x)) ⋯)) :
      N) =
    (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) ⋯) : N)
have right₄ : IsLocalizedModule.mk' f m s =
  (↑(Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f m s) sorry) : N)
Tactic: rw [Module.algebraMap_end_apply, SetLike.val_smul_of_tower,
        ← IsLocalizedModule.mk'_smul, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel_right]