awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s' : Finset N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
empty :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑∅ : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (t • x)
insert :
  ∀ (a : N) (s : Finset N),
    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),
        ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑(Insert.insert a s) : Set N)) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)

Tactic:
induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]

Premises used: smul_smul, Insert.insert, algebraMap_smul, Submonoid.smul_def, mul_comm, Algebra.smul_def, Finset.coe_insert, smul_add, Submodule.mem_span_insert, 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'
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)
obtain₁ :
  ∀ (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)
obtain₂ 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' : Set N)) (t • x)
obtain₄ :
  ∀ (s' : Finset 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)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)

Tactic:
classical
  obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
  rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
  · exact ⟨t, Submodule.span_mono hss' ht⟩
  clear hx hss' s
  induction s' using Finset.induction_on generalizing x with
  | empty => use 1; simpa using hs'
  | insert a s _ hs =>
  simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
  rcases hs' with ⟨y, z, hz, rfl⟩
  rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
  apply congrArg (fun x ↦ x • a) at e
  simp only [algebraMap_smul] at e
  rcases hs _ hz with ⟨t, ht⟩
  refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩
  rw [smul_add, ← smul_smul, mul_comm, ← smul_smul, ← smul_smul, ← e, mul_comm, ← Algebra.smul_def]
  simp [Submonoid.smul_def]

Premises used: smul_smul, Insert.insert, algebraMap_smul, Submonoid.smul_def, Submodule.mem_span_finite_of_mem_span, mul_comm, Algebra.smul_def, Finset.coe_insert, smul_add, Submodule.mem_span_insert, rfl
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
R' : Type u_3
inst_2 : CommSemiring R'
inst_3 : Algebra R R'
inst_4 : Algebra R' S
inst_5 : Algebra R S
inst_6 : IsScalarTower R R' S
inst_7 : IsLocalization M R'
s : Set S
x : S
hx : Membership.mem (γ := Subalgebra R' S) (Algebra.adjoin R' s) x
⊢ Membership.mem (γ := Submodule R' S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R' S) → Submodule R' S) (Algebra.adjoin R' s) : Submodule R' S) x

Tactic:
change x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s) at hx

Premises used: Algebra.adjoin, Subalgebra.toSubmodule, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
R' : Type u_3
inst_2 : CommSemiring R'
inst_3 : Algebra R R'
inst_4 : Algebra R' S
inst_5 : Algebra R S
inst_6 : IsScalarTower R R' S
inst_7 : IsLocalization M R'
s : Set S
x : S
hx :
  Membership.mem (γ := Submodule R' S)
    ((Subalgebra.toSubmodule : (a : Subalgebra R' S) → Submodule R' S) (Algebra.adjoin R' s) : Submodule R' S) x
simp_rw :
  ∀ (hx : Membership.mem (γ := Submodule R' S) (Submodule.span R' (↑(Submonoid.closure s) : Set S)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R S) (Submodule.span R (↑(Submonoid.closure s) : Set S)) (t • x)
⊢ ∃ (t : ↥M),
    Membership.mem (γ := Submodule R S)
      ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R s) : Submodule R S) (t • x)

Tactic:
simp_rw [Algebra.adjoin_eq_span] at hx ⊢

Premises used: Algebra.adjoin_eq_span
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
R' : Type u_3
inst_2 : CommSemiring R'
inst_3 : Algebra R R'
inst_4 : Algebra R' S
inst_5 : Algebra R S
inst_6 : IsScalarTower R R' S
inst_7 : IsLocalization M R'
s : Set S
x : S
hx : Membership.mem (γ := Submodule R' S) (Submodule.span R' (↑(Submonoid.closure s) : Set S)) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R S) (Submodule.span R (↑(Submonoid.closure s) : Set S)) (t • x)

Tactic:
multiple_mem_span_of_mem_localization_span M R' _ _ hx

Premises used: Set.Mem, multiple_mem_span_of_mem_localization_span
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
R' : Type u_3
inst_2 : CommSemiring R'
inst_3 : Algebra R R'
inst_4 : Algebra R' S
inst_5 : Algebra R S
inst_6 : IsScalarTower R R' S
inst_7 : IsLocalization M R'
s : Set S
x : S
hx : Membership.mem (γ := Submodule R' S) (Submodule.span R' (↑(Submonoid.closure s) : Set S)) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R S) (Submodule.span R (↑(Submonoid.closure s) : Set S)) (t • x)

Tactic:
exact multiple_mem_span_of_mem_localization_span M R' _ _ hx

Premises used: multiple_mem_span_of_mem_localization_span
-- Module: Mathlib.RingTheory.Localization.Finiteness
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
h :
  Eq (α := R →+* Sₚ) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯) (algebraMap R Rₚ))
⊢ Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)

Tactic:
apply IsLocalization.ringHom_ext M

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Localization.Finiteness
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
⊢ Eq (α := R →+* Sₚ) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₚ Sₚ) (algebraMap R Rₚ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯) (algebraMap R Rₚ))

Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Premises used: IsLocalization.map_comp, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Localization.Finiteness
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
⊢ Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)

Tactic:
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]
-- Module: Mathlib.RingTheory.Localization.Finiteness
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
this :
  Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ)
    (IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
obtain : ∀ (T : Finset S) (hT : Eq (α := Submodule R S) (Submodule.span R (↑T : Set S)) ⊤), Module.Finite Rₚ Sₚ
⊢ Module.Finite Rₚ Sₚ

Tactic:
obtain ⟨T, hT⟩ := hRS
-- Module: Mathlib.RingTheory.Localization.Finiteness
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ₚ
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)) ⊤
h : Eq (α := Submodule Rₚ Sₚ) (Submodule.span Rₚ (↑(Finset.image (⇑(algebraMap S Sₚ) : (a : S) → Sₚ) T) : Set Sₚ)) ⊤
⊢ Module.Finite Rₚ Sₚ

Tactic:
use T.image (algebraMap S Sₚ)

Premises used: Algebra.algebraMap, DFunLike.coe, Finset.image
-- Module: Mathlib.RingTheory.Localization.Finiteness
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ₚ
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)) ⊤
⊢ Eq (α := Submodule Rₚ Sₚ) (Submodule.span Rₚ (↑(Finset.image (⇑(algebraMap S Sₚ) : (a : S) → Sₚ) T) : Set Sₚ)) ⊤

Tactic:
simpa using span_eq_top_localization_localization Rₚ M Sₚ hT

Premises used: span_eq_top_localization_localization
-- Module: Mathlib.RingTheory.Localization.Finiteness
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ₚ
h :
  ∀
    (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)) ⊤),
    Eq (α := Submodule Rₚ Sₚ) (Submodule.span Rₚ (↑(Finset.image (⇑(algebraMap S Sₚ) : (a : S) → Sₚ) T) : Set Sₚ)) ⊤
⊢ Module.Finite Rₚ 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
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R_1 : Type u
inst : CommSemiring R_1
S_1 : Submonoid R_1
Rₚ : Type v
inst_1 : CommSemiring Rₚ
inst_2 : Algebra R_1 Rₚ
inst_3 : IsLocalization S_1 Rₚ
M : Type w
inst_4 : AddCommMonoid M
inst_5 : Module R_1 M
Mₚ : Type t
inst_6 : AddCommMonoid Mₚ
inst_7 : Module R_1 Mₚ
inst_8 : Module Rₚ Mₚ
inst_9 : IsScalarTower R_1 Rₚ Mₚ
f : M →ₗ[R_1] Mₚ
inst_10 : IsLocalizedModule S_1 f
R : Type u_1
S : Type u_2
inst_11 : CommSemiring R
P : Ideal R
inst_12 : CommSemiring S
inst_13 : Algebra R S
inst_14 : Module.Finite R S
inst_15 : P.IsPrime
⊢ Module.Finite.{u_1, u_2} (Localization.AtPrime P) (Localization (M := S) (Algebra.algebraMapSubmonoid S P.primeCompl))

Tactic:
.of_isLocalization R S P.primeCompl

Premises used: Module.Finite.of_isLocalization, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Localization.Finiteness
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
A : Type u_1
C : Type u_2
inst_11 : CommRing A
inst_12 : CommRing C
inst_13 : Algebra A C
inst_14 : Module.Finite A C
⊢ Module.Finite.{u_1, u_2} (FractionRing A) (Localization (M := C) (algebraMapSubmonoid.{u_1, u_2} (R := A) C A⁰))

Tactic:
.of_isLocalization A C A⁰

Premises used: nonZeroDivisors, Module.Finite.of_isLocalization
-- Module: Mathlib.RingTheory.Localization.Finiteness
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
obtain : ∀ (T : Finset M) (hT : Eq (α := Submodule R M) (Submodule.span R (↑T : Set M)) ⊤), Module.Finite Rₚ Mₚ
⊢ Module.Finite Rₚ Mₚ

Tactic:
obtain ⟨T, hT⟩ := ‹Module.Finite R M›

Premises used: Module.Finite
-- Module: Mathlib.RingTheory.Localization.Finiteness
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)) ⊤
h : Eq (α := Submodule Rₚ Mₚ) (Submodule.span Rₚ (↑(Finset.image (⇑f : (a : M) → Mₚ) T) : Set Mₚ)) ⊤
⊢ Module.Finite Rₚ Mₚ

Tactic:
use T.image f

Premises used: DFunLike.coe, Finset.image
-- Module: Mathlib.RingTheory.Localization.Finiteness
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)) ⊤
⊢ Eq (α := Submodule Rₚ Mₚ) (Submodule.span Rₚ (↑(Finset.image (⇑f : (a : M) → Mₚ) T) : Set Mₚ)) ⊤

Tactic:
simpa using span_eq_top_of_isLocalizedModule Rₚ S f hT

Premises used: span_eq_top_of_isLocalizedModule
-- Module: Mathlib.RingTheory.Localization.Finiteness
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ₚ
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ₚ)) ⊤
⊢ 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

Premises used: Module.Finite
-- Module: Mathlib.RingTheory.Localization.Finiteness
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 (Localization (M := R) S) (LocalizedModule S M)

Tactic:
of_isLocalizedModule S (LocalizedModule.mkLinearMap S M)

Premises used: Module.Finite.of_isLocalizedModule, LocalizedModule.mkLinearMap
-- 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)
fg_top : Submodule.FG.{u, w} (R := R) (M := M) ⊤
⊢ Module.Finite R M

Tactic:
constructor
-- 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)
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) ⊤
⊢ Submodule.FG.{u, w} (R := R) (M := M) ⊤

Tactic:
choose s₁ s₂ using (fun g ↦ (H g).1)

Premises used: Module.Finite.fg_top
-- 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 : Eq (α := Submodule R M) (Submodule.span R (↑(t.attach.biUnion sf) : Set M)) ⊤
⊢ Submodule.FG.{u, w} (R := R) (M := M) ⊤

Tactic:
use t.attach.biUnion sf

Premises used: Finset.biUnion, Finset.attach