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
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
⊢ HSMul.hSMul (β := ↥(localized₀ p f M')) (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).2
      (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f x s) ⋯) =
    ((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
        (a : ↥M') → ↥(localized₀ p f M'))
      (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).1
have a : (↑(HSMul.hSMul (β := ↥(localized₀ p f M')) (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).2
        (Subtype.mk (p := fun (x : N) ↦ x ∈ localized₀ p f M') (IsLocalizedModule.mk' f x s) sorry)) :
    N) =
  (↑(((toLocalized₀ p f M' : LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ↥M' ↥(localized₀ p f M')) :
          (a : ↥M') → ↥(localized₀ p f M'))
        (Subtype.mk (p := fun (x : M) ↦ x ∈ M') x hx, s).1) :
    N)
Tactic: ext
-- 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
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f a r ∈ localized₀ p f Q
have refine : IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r
Tactic: refine ⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
⊢ (((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : R) → Module.End R (N ⧸ localized' S p f M'))
            (↑x : R) :
          Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
      (IsLocalization.mk' S 1 x • m) =
    m
have rw : (↑x : R) • IsLocalization.mk' S 1 x • m = m
Tactic: rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
rw : (↑x : R) • IsLocalization.mk' S 1 x • m = m
⊢ (((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : R) → Module.End R (N ⧸ localized' S p f M'))
            (↑x : R) :
          Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
      (IsLocalization.mk' S 1 x • m) =
    m
have rw₁ : ((↑x : R) • IsLocalization.mk' S 1 x) • m = m
Tactic: rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
rw : (↑x : R) • IsLocalization.mk' S 1 x • m = m
rw₁ : ((↑x : R) • IsLocalization.mk' S 1 x) • m = m
⊢ (((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : R) → Module.End R (N ⧸ localized' S p f M'))
            (↑x : R) :
          Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
      (IsLocalization.mk' S 1 x • m) =
    m
have rw₂ : IsLocalization.mk' S (↑x : R) x • m = m
Tactic: rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
rw : (↑x : R) • IsLocalization.mk' S 1 x • m = m
rw₁ : ((↑x : R) • IsLocalization.mk' S 1 x) • m = m
rw₂ : IsLocalization.mk' S (↑x : R) x • m = m
⊢ (((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : R) → Module.End R (N ⧸ localized' S p f M'))
            (↑x : R) :
          Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
      (IsLocalization.mk' S 1 x • m) =
    m
have rw₃ : HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 m = m
Tactic: rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')
rw : (↑x : R) • IsLocalization.mk' S 1 x • m = m
rw₁ : ((↑x : R) • IsLocalization.mk' S 1 x) • m = m
rw₂ : IsLocalization.mk' S (↑x : R) x • m = m
rw₃ : HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 m = m
⊢ (((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
              (a : R) → Module.End R (N ⧸ localized' S p f M'))
            (↑x : R) :
          Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
        (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
      (IsLocalization.mk' S 1 x • m) =
    m
have rw₄ : m = m
Tactic: rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
⊢ IsUnit.{u_8} (M := Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')))
    ((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : R) → Module.End R (N ⧸ localized' S p f M'))
        (↑x : R) :
      Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')))
have refine : ∀ (m n : HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
  (e :
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
      ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                  (a : R) → Module.End R (N ⧸ localized' S p f M'))
                (↑x : R) :
              Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
            (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
          m :
        HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
      ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                  (a : R) → Module.End R (N ⧸ localized' S p f M'))
                (↑x : R) :
              Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
            (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
          n :
        HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))),
  m = n
Tactic: refine (Module.End.isUnit_iff _).mpr ⟨fun m n e ↦ ?_, fun m ↦ ⟨(IsLocalization.mk' S 1 x) • m,
      by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e :
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                (a : R) → Module.End R (N ⧸ localized' S p f M'))
              (↑x : R) :
            Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk m) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
    ((((algebraMap R (Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
                (a : R) → Module.End R (N ⧸ localized' S p f M'))
              (↑x : R) :
            Module.End R (HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))) :
          (a : N ⧸ localized' S p f M') → N ⧸ localized' S p f M')
        (Submodule.Quotient.mk n) :
      HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M'))
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have e₁ : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • (m - n))
Tactic: simp only [Module.algebraMap_end_apply, ← mk_smul, Submodule.Quotient.eq, ← smul_sub] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • (m - n))
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have e₁ : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
Tactic: replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have rwa : ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
rwa :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have rwa₁ : ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (((↑x : R) • IsLocalization.mk' S 1 x) • (m - n))),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
rwa :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₁ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (((↑x : R) • IsLocalization.mk' S 1 x) • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have rwa₂ : ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S (↑x : R) x • (m - n))),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Submodule (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
M_1 : Type u_3
N_1 : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Algebra R_1 S_1
inst_7 : Module S_1 N_1
inst_8 : IsScalarTower R_1 S_1 N_1
p_1 : Submonoid R_1
inst_9 : IsLocalization p_1 S_1
f_1 : M_1 →ₗ[R_1] N_1
inst_10 : IsLocalizedModule p_1 f_1
M'_1 M'' : Submodule R_1 M_1
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst_11 : CommRing R
inst_12 : CommRing S
inst_13 : AddCommGroup M
inst_14 : AddCommGroup N
inst_15 : Module R M
inst_16 : Module R N
inst_17 : Algebra R S
inst_18 : Module S N
inst_19 : IsScalarTower R S N
p : Submonoid R
inst_20 : IsLocalization p S
f : M →ₗ[R] N
inst_21 : IsLocalizedModule p f
M'_2 M' : Submodule R M
x : ↥p
m n : N
e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S 1 x • (↑x : R) • (m - n))
rwa :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') ((↑x : R) • IsLocalization.mk' S 1 x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₁ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (((↑x : R) • IsLocalization.mk' S 1 x) • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
rwa₂ :
  ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (IsLocalization.mk' S (↑x : R) x • (m - n))),
    Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
      (Submodule.Quotient.mk n)
⊢ Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
have rwa₃ : ∀ (e : Membership.mem (γ := Submodule S N) (localized' S p f M') (HSMul.hSMul.{u_6, u_8, u_8} (α := S) 1 (m - n))),
  Eq (α := HasQuotient.Quotient N (B := Submodule S N) (localized' S p f M')) (Submodule.Quotient.mk m)
    (Submodule.Quotient.mk n)
Tactic: rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
Cleared hypotheses: e