-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem algebraMap_injective_of_span_eq_top (s : Set R) (span_eq : Ideal.span s = ⊤) :
    Function.Injective (algebraMap R <| Π a : s, Away a.1) := fun x y eq ↦ by
  suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this
  by_contra ne
  have ⟨r, hrs, disj⟩ := Ideal.exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalization.eq_iff_exists (.powers r.1) _).mp (congr_fun eq r)
  exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
⊢ False

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

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑(Module.eqIdeal R x y) ↑(Submonoid.powers r)
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
⊢ x = y

Tactic:
suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
⊢ Module.eqIdeal R x y = ⊤

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r : R
hrs : r ∈ s
disj : Disjoint ↑(Module.eqIdeal R x y) ↑(Submonoid.powers r)
⊢ False

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

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(Module.eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq✝ : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(Module.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

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
⊢ Module.eqIdeal R x y = ⊤

Tactic:
by_contra ne

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(Module.eqIdeal R x y) ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
⊢ False

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

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq✝ : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
ne : ¬Module.eqIdeal R x y = ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑(Module.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
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
x y : R
eq : (algebraMap R ((a : ↑s) → Away ↑a)) x = (algebraMap R ((a : ↑s) → Away ↑a)) y
this : Module.eqIdeal R x y = ⊤
⊢ x = y

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

Result:
no goals