-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Module.eq_of_isLocalized_span (x y : M) (h : ∀ r : s, f r x = f r y) : x = y

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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r)
⊢ False

Tactic:
let r : s := ⟨r, hrs⟩

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ 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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
⊢ False

Tactic:
have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r)
⊢ 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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
this : eqIdeal R x y = ⊤
⊢ x = y

Tactic:
simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this

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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False

Tactic:
have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalizedModule.eq_iff_exists (.powers r.1) _).mp (h r)

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
n : ℕ
eq : ⟨(fun x => ↑r ^ x) n, ⋯⟩ • x = ⟨(fun x => ↑r ^ x) n, ⋯⟩ • y
⊢ 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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
⊢ eqIdeal R x y = ⊤

Tactic:
by_contra ne

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
⊢ 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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
⊢ x = y

Tactic:
suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
⊢ eqIdeal R x y = ⊤

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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
ne : ¬eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
n : ℕ
eq : ⟨(fun x => ↑r ^ x) n, ⋯⟩ • x = ⟨(fun x => ↑r ^ x) n, ⋯⟩ • y
⊢ False

Tactic:
exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Result:
no goals