awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Membership.mem (γ := Submodule R M) (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
have h : Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ (n₂ + n₁) • x)
Tactic: apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) 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₁ : ℕ
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₂ + n₁) • x)
have h : Membership.mem (γ := Submodule R M) (Submodule.span R (↑(sf r) : Set M)) ((↑r : R) ^ n₂ • (↑r : R) ^ n₁ • x)
Tactic: rw [pow_add, mul_smul]
-- 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: classical
  constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  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)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact 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)
fg_top : Submodule.FG.{u, w} (R := R) (M := M) ⊤
⊢ Module.Finite R 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: classical
  constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  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)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact 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)
fg_top : Submodule.FG.{u, w} (R := R) (M := M) ⊤
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) ⊤
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) ⊤
⊢ Module.Finite R M
have h : ∀ (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))) ⊤),
  let 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)) ⊤
Tactic: classical
  constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  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)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact 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)
fg_top : Submodule.FG.{u, w} (R := R) (M := M) ⊤
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) ⊤
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) ⊤
h :
  ∀ (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))) ⊤),
    let 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)) ⊤
⊢ Module.Finite R M
have h₁ : ∀ (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))) ⊤),
  let sf : (x : ↥t) → Finset M := fun (x : ↥t) ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers (↑x : R)) (f x) (s₁ x);
  LE.le.{w} (α := Submodule R M) ⊤ (⨆ (x : ↥t), Submodule.span R (↑(sf x) : Set M))
Tactic: classical
  constructor
  choose s₁ s₂ using (fun g ↦ (H g).1)
  let sf := fun x : t ↦
    IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers x.val) (f x) (s₁ x)
  use t.attach.biUnion sf
  rw [Submodule.span_attach_biUnion, eq_top_iff]
  rintro x -
  refine Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (t : Set R) ht _ (fun r ↦ ?_)
  set S : Submonoid R := Submonoid.powers r.val
  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)
  rw [Submonoid.smul_def, ← IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_one] at hn₁
  obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalizedModule.smul_mem_finsetIntegerMultiple_span
    S (f r) _ (s₁ r) hn₁
  rw [Submonoid.smul_def] at hn₂
  use n₂ + n₁
  apply le_iSup (fun x : t ↦ Submodule.span R (sf x : Set M)) r
  rw [pow_add, mul_smul]
  exact 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 : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
⊢ Module.Finite R M
have rw : ∀ (ht : ∃ (s' : Finset R), (↑s' : Set R) ⊆ t ∧ Eq (α := Ideal R) (Ideal.span (↑s' : Set R)) ⊤)
  {Mₚ : (↑t : Type u) → Type u_1} [inst_9 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)]
  [inst_10 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)] {Rₚ : (↑t : Type u) → Type u_2}
  [inst_11 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)] [inst_12 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)]
  [h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)]
  [inst_13 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)]
  [∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)]
  (f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g))
  [h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)]
  (H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)), Module.Finite R M
Tactic: rw [Ideal.span_eq_top_iff_finite] at ht
Cleared hypotheses: ht, Mₚ, inst_3, inst_4, Rₚ, inst_5, inst_6, h₁, inst_7, inst_8, f, h₂, H
-- 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 : Set R
ht : ∃ (s' : Finset R), (↑s' : Set R) ⊆ t ∧ Eq (α := Ideal R) (Ideal.span (↑s' : Set R)) ⊤
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
⊢ Module.Finite R M
have obtain : ∀ (t' : Finset R) (hc : (↑t' : Set R) ⊆ t) (ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤), Module.Finite R M
Tactic: obtain ⟨t', hc, ht'⟩ := ht
Cleared hypotheses: ht
-- 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 : Set R
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
t' : Finset R
hc : (↑t' : Set R) ⊆ t
ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤
⊢ Module.Finite R M
have this : ∀ (g : ↥t'), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) sorry))
Tactic: have (g : t') : IsLocalization.Away g.val (Rₚ ⟨g.val, hc g.property⟩) :=
    h₁ ⟨g.val, hc g.property⟩
-- 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 : Set R
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
t' : Finset R
hc : (↑t' : Set R) ⊆ t
ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤
this : ∀ (g : ↥t'), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯))
⊢ Module.Finite R M
have this₁ : ∀ (g : ↥t'),
  IsLocalizedModule.Away.{u, w, u_1} (M := M) (M' := Mₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) sorry)) (↑g : R)
    ((fun (g : ↥t') ↦
        (f (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) sorry) :
          LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) sorry))))
      g)
Tactic: have (g : t') : IsLocalizedModule.Away g.val
    ((fun g ↦ f ⟨g.val, hc g.property⟩) g) := h₂ ⟨g.val, hc g.property⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
h : N.FG
⊢ FG (localized' R' S f N)
have rw : ∀ (h : ∃ (S : Set M), S.Finite ∧ span R S = N),
  ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)
Tactic: rw [fg_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
h : ∃ (S : Set M), S.Finite ∧ span R S = N
⊢ ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)
have rcases : ∀ (s : Set M) (hfin : s.Finite) (hspan : span R s = N),
  ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)
Tactic: rcases h with ⟨s, hfin, hspan⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
s : Set M
hfin : s.Finite
hspan : span R s = N
⊢ Eq (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (localized' R' S f N)
have rw : Eq (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (localized' R' S f (span R s))
Tactic: rw [← hspan, localized'_span]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
s : Set M
hfin : s.Finite
hspan : span R s = N
rw : Eq (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (localized' R' S f (span R s))
⊢ Eq (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (localized' R' S f N)
have rw₁ : Eq.{u_2 + 1} (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (span R' ((⇑f : (a : M) → M') '' s))
Tactic: rw [← hspan, localized'_span]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
t : Set R
ht : Eq (α := Ideal R) (span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    FG (R := Localization.Away (↑g : R))
      (map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) I)
⊢ I.FG
have apply : Module.Finite R ↥I
Tactic: apply Module.Finite.iff_fg.mp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
f : R →+* S
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    Ideal.FG
      (ker (F :=
        RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
        (Localization.awayMap f (↑g : R)))
⊢ Ideal.FG (ker f)
have apply : ∀ (g : (↑t : Type u)),
  Ideal.FG (R := Localization.Away (↑g : R))
    (Ideal.map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) (ker f))
Tactic: apply Ideal.fg_of_localizationSpan t ht