awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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))
hx :
  HSMul.hSMul (β := S') y' ((algebraMap S S' : (a : S) → S') x : S') ∈
    HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S'))
⊢ Membership.mem (α := S')
    (Submodule.map g.toLinearMap
      (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)))
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')

Tactic:
rw [hx₁, ← g_apply, ← map_smul g, g_apply, ← Algebra.linearMap_apply, ← AlgHom.coe_toLinearMap,
    ← Submodule.map_span] at hx

Premises used: AlgHom.coe_toLinearMap, Algebra.linearMap_apply, Submodule.map_span, map_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'
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))
hx :
  Membership.mem (α := S')
    (Submodule.map g.toLinearMap
      (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)))
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
obtain :
  ∀ (x' : S)
    (hx' :
      x' ∈
        (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) :
          Set S))
    (hx'' :
      Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
        ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : 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 ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx

Premises used: Algebra.algebraMap, DFunLike.coe
-- 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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
obtain :
  ∀ (a : R) (ha₁ : a ∈ (↑M : Set R))
    (ha₂ :
      HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
                  ((algebraMap R S : (a : R) → S) a) ⋯) :
              S) :
            S)
          x' =
        HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
                  ((algebraMap R S : (a : R) → S) a) ⋯) :
              S) :
            S)
          (y' • 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)
⊢ ∃ (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 ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ :=
    (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx''

Premises used: Algebra.algebraMap, Submonoid.map, Iff.mp, rfl, IsLocalization.eq_iff_exists
-- 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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
h :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    ((Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • 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:
use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M)

Premises used: Subtype.mk
-- 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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) (a • x')

Tactic:
(Submodule.span R
          (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s :
            Set S)).smul_mem
      a hx'

Premises used: Algebra.algebraMap, IsLocalization.finsetIntegerMultiple, Submonoid.map, SetLike.coe, Submodule.span, Submodule.smul_mem
-- 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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
h : (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x = a • x'
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    ((Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x)

Tactic:
convert!
    (Submodule.span R
          (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s :
            Set S)).smul_mem
      a hx' using 1

Premises used: Algebra.algebraMap, IsLocalization.finsetIntegerMultiple, Submonoid.map, SetLike.coe, Submodule.span, Submodule.smul_mem
-- 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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x) =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x'

Tactic:
ha₂.symm

Premises used: Eq.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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
h :
  (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
h₁ :
  a • x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x'
⊢ (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x = a • x'

Tactic:
convert! ha₂.symm using 1

Premises used: Eq.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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
h :
  (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) • (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') : R) • x =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S) (y' • x)
⊢ (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)

Tactic:
rw [Subtype.coe_mk, Submonoid.smul_def, Submonoid.coe_mul, ← smul_smul]

Premises used: Subtype.coe_mk, smul_smul, Submonoid.smul_def, Submonoid.coe_mul
-- 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'
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))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) • (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') : R) • x =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S) (y' • x)

Tactic:
Algebra.smul_def _ _

Premises used: Algebra.smul_def