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
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'
mp₄ : mk' S (HMul.hMul (α := R) 1 1) z' • y' = (1 * 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 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]
-- 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'
mp₄ : mk' S (HMul.hMul (α := R) 1 1) z' • y' = (1 * mk' S 1 z') • y'
mp₅ : mk' S 1 z' • y' = (1 * 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 1 z' • y' = 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_1 : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a_1) x
a : S
y : N
hy : Membership.mem (γ := Submodule R N) (Submodule.span R a_1) y
z : ↥M
hx : Membership.mem (γ := Submodule S N) (Submodule.span S a_1) (mk' S 1 z • y)
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a_1) y_1 ∧ ∃ (z_1 : ↥M), a • mk' S 1 z • y = mk' S 1 z_1 • y_1
have mp : ∀ (y' : R) (z' : ↥M),
  ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a_1) y_1 ∧
      ∃ (z_1 : ↥M), mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1
Tactic: obtain ⟨y', z', rfl⟩ := exists_mk'_eq M a
Cleared hypotheses: a
-- 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' : R
z' : ↥M
⊢ ∃ (y_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧
      ∃ (z_1 : ↥M), mk' S y' z' • mk' S 1 z • y = mk' S 1 z_1 • y_1
have mp : mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
Tactic: refine ⟨y' • y, 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' : R
z' : ↥M
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
have mp : mk' S y' z' • mk' S 1 z • y =
  mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
Tactic: rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_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' : R
z' : ↥M
mp :
  mk' S y' z' • mk' S 1 z • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
have mp₁ : (mk' S y' z' * mk' S 1 z) • y =
  mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
Tactic: rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_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' : R
z' : ↥M
mp :
  mk' S y' z' • mk' S 1 z • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₁ :
  (mk' S y' z' * mk' S 1 z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
have mp₂ : mk' S (y' * 1) (z' * z) • y =
  mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
Tactic: rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_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' : R
z' : ↥M
mp :
  mk' S y' z' • mk' S 1 z • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₁ :
  (mk' S y' z' * mk' S 1 z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₂ :
  mk' S (y' * 1) (z' * z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
have mp₃ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (β := S) (mk' S 1 (z' * z)) ((algebraMap R S : (a : R) → S) y' : S) • y
Tactic: rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_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' : R
z' : ↥M
mp :
  mk' S y' z' • mk' S 1 z • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₁ :
  (mk' S y' z' * mk' S 1 z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₂ :
  mk' S (y' * 1) (z' * z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₃ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (β := S) (mk' S 1 (z' * z)) ((algebraMap R S : (a : R) → S) y' : S) • y
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
have mp₄ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y' : S) (mk' S 1 (z' * z)) • y
Tactic: rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_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' : R
z' : ↥M
mp :
  mk' S y' z' • mk' S 1 z • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₁ :
  (mk' S y' z' * mk' S 1 z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₂ :
  mk' S (y' * 1) (z' * z) • y =
    mk' S 1 (z' * z) • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) y' : S) y
mp₃ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (β := S) (mk' S 1 (z' * z)) ((algebraMap R S : (a : R) → S) y' : S) • y
mp₄ : mk' S (y' * 1) (z' * z) • y = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y' : S) (mk' S 1 (z' * z)) • y
⊢ mk' S y' z' • mk' S 1 z • y = mk' S 1 (z' * z) • y' • y
have mp₅ : mk' S (y' * 1) (z' * z) • y = mk' S (y' * 1) (z' * z) • y
Tactic: rw [← IsScalarTower.algebraMap_smul S y', smul_smul, ← mk'_mul, smul_smul,
        mul_comm (mk' S _ _), mul_mk'_eq_mk'_of_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
x : S
a : Set R
⊢ Membership.mem (γ := Ideal S) (Ideal.span ((⇑(algebraMap R S) : (a : R) → S) '' a)) x ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
have refine : (∃ (y : S),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
      ∃ (z : ↥M), x = mk' S 1 z • y) ↔
  ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
Tactic: refine (mem_span_iff M).trans ?_
-- 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
x : S
a : Set R
⊢ (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
have mp : (∃ (y : S),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
      ∃ (z : ↥M), x = mk' S 1 z • y) →
  ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
Tactic: constructor
-- 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
x : S
a : Set R
mp :
  (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) →
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
⊢ (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) ↔
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
have mpr : (∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z) →
  ∃ (y : S),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
      ∃ (z : ↥M), x = mk' S 1 z • y
Tactic: constructor
-- 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
x : S
a : Set R
⊢ (∃ (y : S),
      Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
        ∃ (z : ↥M), x = mk' S 1 z • y) →
    ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
have mp : (∃ (y : S), Membership.mem (γ := Submodule R S) (coeSubmodule S (Ideal.span a)) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y) →
  ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
Tactic: rw [← coeSubmodule_span]
-- 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
⊢ ∃ (y : R), Membership.mem (γ := Ideal R) (Ideal.span a) y ∧ ∃ (z : ↥M), x = mk' S y z
have mp : x = mk' S y z
Tactic: refine ⟨y, hy, 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
⊢ x = mk' S y z
have mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
Tactic: rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
⊢ x = mk' S y z
have mp₁ : HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
Tactic: rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
mp₁ : HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
⊢ x = mk' S y z
have mp₂ : HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
Tactic: rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
mp₁ : HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₂ : HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
⊢ x = mk' S y z
have mp₃ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z) = mk' S y z
Tactic: rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
mp₁ : HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₂ : HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₃ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z) = mk' S y z
⊢ x = mk' S y z
have mp₄ : mk' S (y * 1) z = mk' S y z
Tactic: rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : y ∈ (↑(Ideal.span a) : Set R)
z : ↥M
hz : x = HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S)
mp : HSMul.hSMul (β := S) (mk' S 1 z) ((Algebra.linearMap R S : (a : R) → S) y : S) = mk' S y z
mp₁ : HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₂ : HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S) = mk' S y z
mp₃ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z) = mk' S y z
mp₄ : mk' S (y * 1) z = mk' S y z
⊢ x = mk' S y z
have mp₅ : mk' S y z = mk' S y z
Tactic: rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
⊢ ∃ (y : S),
    Membership.mem (γ := Submodule R S) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' a)) y ∧
      ∃ (z : ↥M), x = mk' S 1 z • y
have mpr : x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
Tactic: refine ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, 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
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
⊢ x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
have mpr : mk' S y z = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
Tactic: rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
mpr : mk' S y z = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
⊢ x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
have mpr₁ : mk' S y z = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
Tactic: rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
mpr : mk' S y z = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₁ : mk' S y z = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
⊢ x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
have mpr₂ : mk' S y z = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z)
Tactic: rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, 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
x : S
a : Set R
y : R
hy : Membership.mem (γ := Ideal R) (Ideal.span a) y
z : ↥M
hz : x = mk' S y z
mpr : mk' S y z = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₁ : mk' S y z = HMul.hMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
mpr₂ : mk' S y z = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) y : S) (mk' S 1 z)
⊢ x = HSMul.hSMul (β := S) (mk' S 1 z) ((algebraMap R S : (a : R) → S) y : S)
have mpr₃ : mk' S y z = mk' S (y * 1) z
Tactic: rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]