awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
rw : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
rw₁ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + -mk' S x₂ y₂
rw₂ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S x₁ y₁ + mk' S (-x₂) y₂
rw₃ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S (x₁ * (↑y₂ : R) + -x₂ * (↑y₁ : R)) (y₁ * y₂)
rw₄ rw₅ : mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂) = mk' S (x₁ * (↑y₂ : R) + -(x₂ * (↑y₁ : R))) (y₁ * y₂)
⊢ mk' S (x₁ * (↑y₂ : R) - x₂ * (↑y₁ : R)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← mk'_neg, ← mk'_add, neg_mul]

Premises used: sub_eq_add_neg, IsLocalization.mk'_neg, neg_mul, IsLocalization.mk'_add
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
rw :
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
      Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
        ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑f : (a : S) → T)

Tactic:
rw [IsLocalization.injective_iff_map_algebraMap_eq M]

Premises used: IsLocalization.injective_iff_map_algebraMap_eq
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
⊢ ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
      Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
        ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)

Tactic:
fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
refine :
  ∀ (x y : R)
    (hz :
      Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
        ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
⊢ ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
      Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
        ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)

Tactic:
refine fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
x y : R
hz :
  Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
    ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
⊢ Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) (x - y) : S) : T) (0 : T)

Tactic:
rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
x y : R
hz : Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) (x - y) : S) : T) (0 : T)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x - y) : S) (0 : S)

Tactic:
apply h at hz
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommRing T
f : S →+* T
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T) (0 : T) →
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) (0 : S)
x y : R
hz : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (x - y) : S) (0 : S)
rwa :
  ∀
    (hz :
      HSub.hSub (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) = 0),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hz : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)

Tactic:
rwa [map_sub, sub_eq_zero] at hz

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
IsLocalization.injectiveₛ S fun _x hx ↦ isRegular_iff_mem_nonZeroDivisors.mpr (hM hx)

Premises used: Iff.mpr, IsLocalization.injectiveₛ, isRegular_iff_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x_1 : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x_1 : S')
c : R
x : S
⊢ (algebraMap S S' : (a : S) → S') (c • x) = HSMul.hSMul (β := S') c ((algebraMap S S' : (a : S) → S') x : S')

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
⊢ ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')

Tactic:
have g_apply : ∀ x, g x = algebraMap S S' x := fun _ => rfl
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
⊢ (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)

Tactic:
have hx₁ : (y : S) • (s : Set S') = g '' _ :=
    (IsLocalization.finsetIntegerMultiple_image _ s).symm
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
obtain :
  ∀ (y' : R) (hy' : y' ∈ (↑M : Set R)) (e : (algebraMap R S : (a : R) → S) y' = (↑y : S)),
    ∃ (m : ↥M),
      Membership.mem (γ := Submodule R S)
        (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
        (m • x)
⊢ ∃ (m : ↥M),
    Membership.mem (γ := Submodule R S)
      (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) (m • x)

Tactic:
obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
simp_rw : HSMul.hSMul (β := S) y' 1 • (↑s : Set S') = y' • (↑s : Set S')
simp_rw₁ : y' • HSMul.hSMul.{u_2, u_4, u_4} (α := S) 1 (↑s : Set S') = y' • (↑s : Set S')
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')

Tactic:
simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Premises used: smul_assoc, one_smul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')

Tactic:
have : algebraMap R S y' • (s : Set S') = y' • (s : Set S') := by
    simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
⊢ y' • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)

Tactic:
rw [← e, this] at hx₁
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₂ :
  y' • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
⊢ y' ∈ (↑M : Set R)

Tactic:
rw [← e, this] at hx₁
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₂ :
  y' • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
hy'₁ : y' ∈ (↑M : Set R)
⊢ (algebraMap R S : (a : R) → S) y' = (↑y : S)

Tactic:
rw [← e, this] at hx₁
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
hx₁ :
  (↑y : S) • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₂ :
  y' • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
hy'₁ : y' ∈ (↑M : Set R)
e₁ : (algebraMap R S : (a : R) → S) y' = (↑y : S)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')

Tactic:
rw [← e, this] at hx₁
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hx₁ :
  y' • (↑s : Set S') =
    (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
⊢ Eq (α := Submodule R S') (Submodule.span R (y' • (↑s : Set S')))
    (Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)))

Tactic:
replace hx₁ := congr_arg (Submodule.span R) hx₁
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  Eq (α := Submodule R S') (Submodule.span R (y' • (↑s : Set S')))
    (Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)))
⊢ HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))

Tactic:
rw [Submodule.span_smul] at hx₁

Premises used: Submodule.span_smul
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
hx :
  Membership.mem (α := S') (γ := Submodule R S') (Submodule.span R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
⊢ HSMul.hSMul (β := S') y' ((algebraMap S S' : (a : S) → S') x : S') ∈
    HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S'))

Tactic:
replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx