-- Mathlib/RingTheory/Localization/Away/Basic.lean
/-- Specialized constructor for `IsLocalization.Away`. -/
lemma mk (r : R) (map_unit : IsUnit (algebraMap R S r))
    (surj : ∀ s, ∃ (n : ℕ) (a : R), s * algebraMap R S r ^ n = algebraMap R S a)
    (exists_of_eq : ∀ a b, algebraMap R S a = algebraMap R S b → ∃ (n : ℕ), r ^ n * a = r ^ n * b) :
    IsLocalization.Away r S where
  map_units'

Proof state:
case mk.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x => r ^ x) n, ⋯⟩)

Tactic:
simp only [map_pow]

Result:
case mk.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit ((algebraMap R S) r ^ n)

Proof state:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ z * (algebraMap R S) ↑(a, ⟨r ^ n, ⋯⟩).2 = (algebraMap R S) (a, ⟨r ^ n, ⋯⟩).1

Tactic:
simpa using hn

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
use ⟨a, ⟨r ^ n, n, rfl⟩⟩

Result:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ z * (algebraMap R S) ↑(a, ⟨r ^ n, ⋯⟩).2 = (algebraMap R S) (a, ⟨r ^ n, ⋯⟩).1

Proof state:
case mk.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit ((algebraMap R S) r ^ n)

Tactic:
exact IsUnit.pow _ map_unit

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
x y : R
h : (algebraMap R S) x = (algebraMap R S) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
obtain ⟨n, hn⟩ := exists_of_eq x y h

Result:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
x y : R
h : (algebraMap R S) x = (algebraMap R S) y
n : ℕ
hn : r ^ n * x = r ^ n * y
⊢ ∃ c, ↑c * x = ↑c * y

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
obtain ⟨n, a, hn⟩ := surj z

Result:
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Proof state:
case intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
x y : R
h : (algebraMap R S) x = (algebraMap R S) y
n : ℕ
hn : r ^ n * x = r ^ n * y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
use ⟨r ^ n, n, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
⊢ ∀ (y : ↥(Submonoid.powers r)), IsUnit ((algebraMap R S) ↑y)

Tactic:
rintro ⟨-, n, rfl⟩

Result:
case mk.intro
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x => r ^ x) n, ⋯⟩)