awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
⊢ 0 = HSMul.hSMul (β := N) (mk'.{u_1, u_2} (R := R) (M := M) S 1 1) 0
have rw : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) ((algebraMap R S : (a : R) → S) 1 : S) 0
Tactic: rw [mk'_one, map_one, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
rw : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) ((algebraMap R S : (a : R) → S) 1 : S) 0
⊢ 0 = HSMul.hSMul (β := N) (mk'.{u_1, u_2} (R := R) (M := M) S 1 1) 0
have rw₁ : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) 1 0
Tactic: rw [mk'_one, map_one, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
rw : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) ((algebraMap R S : (a : R) → S) 1 : S) 0
rw₁ : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) 1 0
⊢ 0 = HSMul.hSMul (β := N) (mk'.{u_1, u_2} (R := R) (M := M) S 1 1) 0
have rw₂ : Eq.{u_3 + 1} (α := N) 0 0
Tactic: rw [mk'_one, map_one, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧
      ∃ (z_1 : ↥M), mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 z_1 • y_1
have mp : mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • ((↑z' : R) • y + (↑z : R) • y')
Tactic: refine
        ⟨(z' : R) • y + (z : R) • y',
          Submodule.add_mem _ (Submodule.smul_mem _ _ hy) (Submodule.smul_mem _ _ hy'), z * z', ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
⊢ mk' S 1 z • y + mk' S 1 z' • y' = mk' S 1 (z * z') • ((↑z' : R) • y + (↑z : R) • y')
have mp : mk' S 1 z • y + mk' S 1 z' • y' =
  HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y +
    HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
Tactic: rw [smul_add, ← IsScalarTower.algebraMap_smul S (z : R), ←
        IsScalarTower.algebraMap_smul S (z' : R), smul_smul, smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y +
      HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp : mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp : mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y +
      HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp₁ : mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp : mk' S (HMul.hMul (α := R) 1 1) z • y =
  HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp₁ : mk' S (HMul.hMul (α := R) 1 1) z • y =
  HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp₂ : mk' S (HMul.hMul (α := R) 1 1) z • y =
  (mk' S 1 z * HMul.hMul (β := S) (mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S)) • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    (mk' S 1 z * HMul.hMul (β := S) (mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S)) • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp₃ : mk' S (HMul.hMul (α := R) 1 1) z • y = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) 1 : S) • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    (mk' S 1 z * HMul.hMul (β := S) (mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S)) • y
mp₃ : mk' S (HMul.hMul (α := R) 1 1) z • y = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) 1 : S) • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp₄ : mk' S (HMul.hMul (α := R) 1 1) z • y = (mk' S 1 z * 1) • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    (mk' S 1 z * HMul.hMul (β := S) (mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S)) • y
mp₃ : mk' S (HMul.hMul (α := R) 1 1) z • y = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) 1 : S) • y
mp₄ : mk' S (HMul.hMul (α := R) 1 1) z • y = (mk' S 1 z * 1) • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp₅ : mk' S 1 z • y = (mk' S 1 z * 1) • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z • y =
    (mk' S 1 z * HMul.hMul (β := S) (mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z' : R) : S)) • y
mp₃ : mk' S (HMul.hMul (α := R) 1 1) z • y = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) 1 : S) • y
mp₄ : mk' S (HMul.hMul (α := R) 1 1) z • y = (mk' S 1 z * 1) • y
mp₅ : mk' S 1 z • y = (mk' S 1 z * 1) • y
⊢ mk' S 1 z • y = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z' : R) : S) • y
have mp₆ : mk' S 1 z • y = mk' S 1 z • y
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_assoc, mk'_spec, map_one, mul_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
⊢ mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp : mk' S (HMul.hMul (α := R) 1 1) z' • y' =
  HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
⊢ mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp₁ : mk' S (HMul.hMul (α := R) 1 1) z' • y' =
  HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
⊢ mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp₂ : mk' S (HMul.hMul (α := R) 1 1) z' • y' =
  (HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) (↑z : R) : S) * mk' S 1 z') • y'
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    (HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) (↑z : R) : S) * mk' S 1 z') • y'
⊢ mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp₃ : mk' S (HMul.hMul (α := R) 1 1) z' • y' = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) 1 : S) (mk' S 1 z') • y'
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z • y)
y' : N
hy' : Membership.mem (γ := Submodule R N) (Submodule.span R a) y'
z' : ↥M
hy_1 : Membership.mem (γ := Submodule S N) (Submodule.span S a) (mk' S 1 z' • y')
mp :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S (HMul.hMul (α := R) 1 1) (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₁ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    HMul.hMul (β := S) (mk' S 1 z * mk' S 1 z') ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
mp₂ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' =
    (HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) (↑z : R) : S) * mk' S 1 z') • y'
mp₃ :
  mk' S (HMul.hMul (α := R) 1 1) z' • y' = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) 1 : S) (mk' S 1 z') • y'
⊢ mk' S 1 z' • y' = HMul.hMul (β := S) (mk' S 1 (z * z')) ((algebraMap R S : (a : R) → S) (↑z : R) : S) • y'
have mp₄ : mk' S (HMul.hMul (α := R) 1 1) z' • y' = (1 * mk' S 1 z') • y'
Tactic: rw [← mul_one (1 : R), mk'_mul, mul_right_comm, mk'_spec, map_one, mul_one, one_mul]