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))
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:
exact Algebra.smul_def _ _

Premises used: Algebra.smul_def
-- 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)
⊢ 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'

Tactic:
Algebra.smul_def _ _

Premises used: Algebra.smul_def
-- 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)
⊢ 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'

Tactic:
exact Algebra.smul_def _ _

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
obtain :
  ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
    (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)

Tactic:
obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx

Premises used: Submodule.mem_span_finite_of_mem_span
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
s' : Finset N
hss' : (↑s' : Set N) ⊆ s
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
rsuffices :
  ∀ (t : ↥M) (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
rsuffices₁ : ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)

Tactic:
rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)

Premises used: SetLike.coe, Submodule.span
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
s' : Finset N
hss' : (↑s' : Set N) ⊆ s
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)

Tactic:
⟨t, Submodule.span_mono hss' ht⟩

Premises used: Submodule.span_mono, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
s' : Finset N
hss' : (↑s' : Set N) ⊆ s
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)

Tactic:
exact ⟨t, Submodule.span_mono hss' ht⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
x : N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑∅ : Set N)) x
h : Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (HSMul.hSMul.{u_1, u_5, u_5} (α := ↥M) 1 x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (t • x)

Tactic:
use 1
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
x : N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑∅ : Set N)) x
⊢ Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (HSMul.hSMul.{u_1, u_5, u_5} (α := ↥M) 1 x)

Tactic:
simpa using hs'
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
x : N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑(Insert.insert a s) : Set N)) x
insert :
  ∀
    (hs' :
      ∃ (a_1 : R') (z : N), Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z ∧ x = a_1 • a + z),
    ∃ (t : ↥M) (a_1 : R) (z : N),
      Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z ∧ t • x = a_1 • a + z
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑(Insert.insert a s) : Set N)) (t • x)

Tactic:
simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢

Premises used: Finset.coe_insert, Submodule.mem_span_insert
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
x : N
hs' : ∃ (a_1 : R') (z : N), Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z ∧ x = a_1 • a + z
insert :
  ∀ (y : R') (z : N) (hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z),
    ∃ (t : ↥M) (a_1 : R) (z_1 : N),
      Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
⊢ ∃ (t : ↥M) (a_1 : R) (z : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z ∧ t • x = a_1 • a + z

Tactic:
rcases hs' with ⟨y, z, hz, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
insert :
  ∀ (y' : R) (s' : ↥M)
    (e :
      HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
        (algebraMap R R' : (a : R) → R') (y', s').1),
    ∃ (t : ↥M) (a_1 : R) (z_1 : N),
      Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1

Tactic:
rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
⊢ HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') • a =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R') ((algebraMap R R' : (a : R) → R') (y', s').1 : R') a

Tactic:
apply congrArg (fun x ↦ x • a) at e

Premises used: congrArg, HSMul.hSMul
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') • a =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R') ((algebraMap R R' : (a : R) → R') (y', s').1 : R') a
⊢ HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a

Tactic:
simp only [algebraMap_smul] at e

Premises used: algebraMap_smul
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
insert :
  ∀ (t : ↥M) (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)),
    ∃ (t : ↥M) (a_1 : R) (z_1 : N),
      Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1

Tactic:
rcases hs _ hz with ⟨t, ht⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1

Tactic:
⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩

Premises used: HMul.hMul, SetLike.coe, And.intro, Exists.intro, Submodule.span, Subtype.val, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)
insert : (t * s') • (y • a + z) = ((↑t : R) * y') • a + (↑s' : R) • t • z
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1

Tactic:
refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)
insert : t • s' • y • a + s' • t • z = (↑t : R) • ((↑s' : R) • y) • a + (↑s' : R) • t • z
⊢ (t * s') • (y • a + z) = ((↑t : R) * y') • a + (↑s' : R) • t • z

Tactic:
rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]

Premises used: smul_smul, mul_comm, Algebra.smul_def, smul_add
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)
⊢ t • s' • y • a + s' • t • z = (↑t : R) • ((↑s' : R) • y) • a + (↑s' : R) • t • z

Tactic:
simp [Submonoid.smul_def]

Premises used: Submonoid.smul_def