awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
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)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S)
have 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)
Tactic: rwa [map_sub, sub_eq_zero] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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') ⋯
⊢ ∃ (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)
have g_apply : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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
⊢ ∃ (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)
have hx₁ : (↑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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨y', hy', e : algebraMap R S y' = y⟩ := y.prop
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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')
have simp_rw : HSMul.hSMul (β := S) y' 1 • (↑s : Set S') = y' • (↑s : Set S')
Tactic: simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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')
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
have simp_rw₁ : y' • HSMul.hSMul.{u_2, u_4, u_4} (α := S) 1 (↑s : Set S') = y' • (↑s : Set S')
Tactic: simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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)
⊢ ∃ (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)
have 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')
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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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')
⊢ ∃ (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)
have hx₂ : 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₁
Cleared hypotheses: hx₁, hy', e, this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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')
⊢ ∃ (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)
have 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)))
Tactic: replace hx₁ := congr_arg (Submodule.span R) hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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)))
⊢ ∃ (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)
have 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))
Tactic: rw [Submodule.span_smul] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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))
⊢ ∃ (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)
have 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'))
Tactic: replace hx : _ ∈ y' • Submodule.span R (s : Set S') := Set.smul_mem_smul_set hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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'))
⊢ ∃ (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)
have 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')
Tactic: rw [hx₁, ← g_apply, ← map_smul g, g_apply, ← Algebra.linearMap_apply, ← AlgHom.coe_toLinearMap,
    ← Submodule.map_span] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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')
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨x', hx', hx'' : algebraMap _ _ _ = _⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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')
⊢ ∃ (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)
have 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) sorry) :
            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) sorry) :
            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)
Tactic: obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ :=
    (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx''