awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring Rₚ
inst_3 : CommSemiring Sₚ
inst_4 : Algebra R S
inst_5 : Algebra R Rₚ
inst_6 : Algebra R Sₚ
inst_7 : Algebra S Sₚ
inst_8 : Algebra Rₚ Sₚ
inst_9 : IsScalarTower R S Sₚ
inst_10 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst_11 : IsLocalization M Rₚ
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
have :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
have₁ :
  ∀
    (this :
      Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
        (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)),
    Module.Finite Rₚ Sₚ
have₂ :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
have₃ have₄ :
  ∀
    (this :
      Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
        (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)),
    Module.Finite Rₚ Sₚ
have₅ :
  ∀
    (this :
      Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
        (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯))
    (T : Finset S) (hT : Eq (α := Submodule R S) (Submodule.span R (↑T : Set S)) ⊤), Module.Finite Rₚ Sₚ
⊢ Module.Finite Rₚ Sₚ
have h : ∀
  (this :
    Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
      (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) sorry))
  (T : Finset S) (hT : Eq (α := Submodule R S) (Submodule.span R (↑T : Set S)) ⊤),
  Eq (α := Submodule Rₚ Sₚ) (Submodule.span Rₚ (↑(Finset.image (⇑(algebraMap S Sₚ) : (a : S) → Sₚ) T) : Set Sₚ)) ⊤
Tactic: classical
  have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
  -- We claim that if `S` is generated by `T` as an `R`-module,
  -- then `S'` is generated by `T` as an `R'`-module.
  obtain ⟨T, hT⟩ := hRS
  use T.image (algebraMap S Sₚ)
  simpa using span_eq_top_localization_localization Rₚ M Sₚ hT
Cleared hypotheses: hRS
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst_1 : CommSemiring Rₚ
inst_2 : Algebra R Rₚ
inst_3 : IsLocalization S Rₚ
M : Type w
inst_4 : AddCommMonoid M
inst_5 : Module R M
Mₚ : Type t
inst_6 : AddCommMonoid Mₚ
inst_7 : Module R Mₚ
inst_8 : Module Rₚ Mₚ
inst_9 : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst_10 : IsLocalizedModule S f
inst_11 : Module.Finite R M
⊢ Module.Finite Rₚ Mₚ
have obtain : ∀ (T : Finset M) (hT : Eq (α := Submodule R M) (Submodule.span R (↑T : Set M)) ⊤), Module.Finite Rₚ Mₚ
Tactic: obtain ⟨T, hT⟩ := ‹Module.Finite R M›
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst_1 : CommSemiring Rₚ
inst_2 : Algebra R Rₚ
inst_3 : IsLocalization S Rₚ
M : Type w
inst_4 : AddCommMonoid M
inst_5 : Module R M
Mₚ : Type t
inst_6 : AddCommMonoid Mₚ
inst_7 : Module R Mₚ
inst_8 : Module Rₚ Mₚ
inst_9 : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst_10 : IsLocalizedModule S f
inst_11 : Module.Finite R M
T : Finset M
hT : Eq (α := Submodule R M) (Submodule.span R (↑T : Set M)) ⊤
⊢ Module.Finite Rₚ Mₚ
have h : Eq (α := Submodule Rₚ Mₚ) (Submodule.span Rₚ (↑(Finset.image (⇑f : (a : M) → Mₚ) T) : Set Mₚ)) ⊤
Tactic: use T.image f
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst_1 : CommSemiring Rₚ
inst_2 : Algebra R Rₚ
inst_3 : IsLocalization S Rₚ
M : Type w
inst_4 : AddCommMonoid M
inst_5 : Module R M
Mₚ : Type t
inst_6 : AddCommMonoid Mₚ
inst_7 : Module R Mₚ
inst_8 : Module Rₚ Mₚ
inst_9 : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst_10 : IsLocalizedModule S f
inst_11 obtain : Module.Finite R M
⊢ Module.Finite Rₚ Mₚ
have obtain₁ : ∀ (T : Finset M) (hT : Eq (α := Submodule R M) (Submodule.span R (↑T : Set M)) ⊤), Module.Finite Rₚ Mₚ
Tactic: classical
  obtain ⟨T, hT⟩ := ‹Module.Finite R M›
  use T.image f
  simpa using span_eq_top_of_isLocalizedModule Rₚ S f hT
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst_1 : CommSemiring Rₚ
inst_2 : Algebra R Rₚ
inst_3 : IsLocalization S Rₚ
M : Type w
inst_4 : AddCommMonoid M
inst_5 : Module R M
Mₚ : Type t
inst_6 : AddCommMonoid Mₚ
inst_7 : Module R Mₚ
inst_8 : Module Rₚ Mₚ
inst_9 : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst_10 : IsLocalizedModule S f
inst_11 obtain : Module.Finite R M
obtain₁ : ∀ (T : Finset M) (hT : Eq (α := Submodule R M) (Submodule.span R (↑T : Set M)) ⊤), Module.Finite Rₚ Mₚ
⊢ Module.Finite Rₚ Mₚ
have h : ∀ (T : Finset M) (hT : Eq (α := Submodule R M) (Submodule.span R (↑T : Set M)) ⊤),
  Eq (α := Submodule Rₚ Mₚ) (Submodule.span Rₚ (↑(Finset.image (⇑f : (a : M) → Mₚ) T) : Set Mₚ)) ⊤
Tactic: classical
  obtain ⟨T, hT⟩ := ‹Module.Finite R M›
  use T.image f
  simpa using span_eq_top_of_isLocalizedModule Rₚ S f hT
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)
⊢ Module.Finite R M
have fg_top : Submodule.FG.{u, w} (R := R) (M := M) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)
⊢ Submodule.FG.{u, w} (R := R) (M := M) ⊤
have fg_top : ∀ (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))) ⊤),
  Submodule.FG.{u, w} (R := R) (M := M) ⊤
Tactic: choose s₁ s₂ using (fun g ↦ (H g).1)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)
⊢ Submodule.FG.{u, w} (R := R) (M := M) ⊤
have h : Eq (α := Submodule R M) (Submodule.span R (↑(t.attach.biUnion sf) : Set M)) ⊤
Tactic: use t.attach.biUnion sf
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)
⊢ Eq (α := Submodule R M) (Submodule.span R (↑(t.attach.biUnion sf) : Set M)) ⊤
have h : LE.le.{w} (α := Submodule R M) ⊤ (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M))
Tactic: rw [Submodule.span_attach_biUnion, eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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
have 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)
Tactic: refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)) (Submodule.span (Rₚ r) (↑(s₁ r) : Set (Mₚ r)))
    (IsLocalizedModule.mk' (S := S) (f r) x 1)
have rw : Membership.mem (γ := Submodule.{u_2, u_1} (Rₚ r) (Mₚ r)) ⊤ (IsLocalizedModule.mk' (S := S) (f r) x 1)
Tactic: rw [s₂ r]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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 : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
have 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₁) sorry •
        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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
have 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₁) sorry) : R) • x) :
    Mₚ r)
Tactic: rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
Cleared hypotheses: hn₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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 : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
have 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₂) sorry •
        (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) sorry) : R) • 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₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
have 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₂) sorry) : R) •
    (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₁) sorry) : R) • x)
Tactic: rw [Submonoid.smul_def] at hn₂
Cleared hypotheses: hn₂
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ n • x)
have h : Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
Tactic: use n₂ + n₁