awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
h : LE.le.{w} (α := Submodule R M) ⊤ (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M))
⊢ Eq (α := Submodule R M) (Submodule.span R (↑(t.attach.biUnion sf) : Set M)) ⊤

Tactic:
rw [Submodule.span_attach_biUnion, eq_top_iff]

Premises used: eq_top_iff, Submodule.span_attach_biUnion
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
⊢ Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) x

Tactic:
Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem, SetLike.coe
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
h :
  ∀ (r : (↑(↑t : Set R) : Type u)),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
⊢ Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) x

Tactic:
refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem, SetLike.coe
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
rw : Membership.mem (γ := Submodule.{u_2, u_1} (Rₚ r) (Mₚ r)) ⊤ (IsLocalizedModule.mk' (S := S) (f r) x 1)
⊢ Membership.mem (γ := Submodule.{u_2, u_1} (Rₚ r) (Mₚ r)) (Submodule.span (Rₚ r) (↑(s₁ r) : Set (Mₚ r)))
    (IsLocalizedModule.mk' (S := S) (f r) x 1)

Tactic:
rw [s₂ r]
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
⊢ Membership.mem (γ := Submodule.{u_2, u_1} (Rₚ r) (Mₚ r)) ⊤ (IsLocalizedModule.mk' (S := S) (f r) x 1)

Tactic:
trivial
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
h :
  ∀ (n₁ : ℕ)
    (hn₁ :
      Membership.mem (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯ •
          IsLocalizedModule.mk' (S := S) (f r) x 1)),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)

Tactic:
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ := multiple_mem_span_of_mem_localization_span S (Rₚ r)
    (s₁ r : Set (Mₚ r)) (IsLocalizedModule.mk' (f r) x (1 : S)) (by rw [s₂ r]; trivial)

Premises used: multiple_mem_span_of_mem_localization_span, SetLike.coe, OfNat.ofNat, rfl, IsLocalizedModule.mk'
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯ •
      IsLocalizedModule.mk' (S := S) (f r) x 1)
⊢ Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)

Tactic:
rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁

Premises used: IsLocalizedModule.mk'_one, Submonoid.smul_def, IsLocalizedModule.mk'_smul
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
h :
  ∀ (n₂ : ℕ)
    (hn₂ :
      Membership.mem (γ := Submodule R M)
        (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
        (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)

Tactic:
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁

Premises used: IsLocalizedModule.smul_mem_finsetIntegerMultiple_span, rfl
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    (Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)

Tactic:
rw [Submonoid.smul_def] at hn₂

Premises used: Submonoid.smul_def
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)
h : Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)

Tactic:
use n₂ + n₁
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)
h : Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r

Premises used: le_iSup, SetLike.coe, Submodule.span
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)
h : Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ n₂ • (↑r : R) ^ n₁ • x)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
rw [pow_add, mul_smul]

Premises used: pow_add, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ n₂ • (↑r : R) ^ n₁ • x)

Tactic:
hn₂

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
Mₚ : ↥t → Type u_1
inst_3 : (g : ↥t) → AddCommMonoid (Mₚ g)
inst_4 : (g : ↥t) → Module.{u, u_1} R (Mₚ g)
Rₚ : ↥t → Type u_2
inst_5 : (g : ↥t) → CommSemiring (Rₚ g)
inst_6 : (g : ↥t) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : ↥t), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : ↥t) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : ↥t), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : ↥t) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : ↥t), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : ↥t), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Eq (α := Submodule.{u_2, u_1} (Rₚ g) (Mₚ g)) (Submodule.span (Rₚ g) (↑(s₁ g) : Set (Mₚ g))) ⊤
sf : (x : ↥t) → Finset M :=
  fun (x : ↥t) ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x)
x : M
r : (↑(↑t : Set R) : Type u)
S : Submonoid R := Submonoid.powers (↑r : R)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Mₚ r) (γ := Submodule R (Mₚ r)) (Submodule.span R (↑(s₁ r) : Set (Mₚ r)))
    ((f r : (a : M) → Mₚ r) ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x) :
      Mₚ r)
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r)) : Set M))
    ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯) : R) •
      (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) ⋯) : R) • x)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ n₂ • (↑r : R) ^ n₁ • x)

Tactic:
exact hn₂