-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.mem_of_isLocalized_span {m : M} {N : Submodule R M}
    (h : ∀ r : s, f r m ∈ N.localized₀ (.powers r.1) (f r)) : m ∈ N

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
⊢ False

Tactic:
have ⟨u, hu⟩ := e

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
u : ↥(Submonoid.powers ↑r)
hu : u • t • m = u • 1 • a
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False

Tactic:
obtain ⟨a, ha, t, e⟩ := h r

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : mk' (f r) a t = (f r) m
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
u : ↥(Submonoid.powers ↑r)
hu : (u * t) • m = (u * 1) • a
⊢ ↑(u * t) ∈ ↑I

Tactic:
apply hu ▸ smul_mem _ _ ha

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
⊢ m ∈ N

Tactic:
let I : Ideal R := N.comap (LinearMap.toSpanSingleton R M m)

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ m ∈ N

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ m ∈ N

Tactic:
suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ I = ⊤