-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma of_associated {r r' : R} (h : Associated r r') [IsLocalization.Away r S] :
    IsLocalization.Away r' S

Proof state:
case intro.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ IsUnit ((algebraMap R S) (r * ↑u))

Tactic:
simp [algebraMap_isUnit r, IsUnit.map _ u.isUnit]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) (a * ↑u ^ n)

Tactic:
simp [mul_pow, ← mul_assoc, hn]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]

Result:
no goals

Proof state:
case intro.refine_3.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
use n

Result:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r r' : R
h : Associated r r'
inst✝ : Away r S
⊢ Away r' S

Tactic:
obtain ⟨u, rfl⟩ := h

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ Away (r * ↑u) S

Proof state:
case intro.refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
obtain ⟨n, hn⟩ := exists_of_eq r hab

Result:
case intro.refine_3.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ Away (r * ↑u) S

Tactic:
refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)

Result:
case intro.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
⊢ IsUnit ((algebraMap R S) (r * ↑u))

case intro.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

case intro.refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Proof state:
case intro.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

Tactic:
obtain ⟨n, a, hn⟩ := surj r s

Result:
case intro.refine_2.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

Proof state:
case intro.refine_2.intro.intro
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ ∃ n a, s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) a

Tactic:
use n, a * u ^ n

Result:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
s : S
n : ℕ
a : R
hn : s * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ s * (algebraMap R S) (r * ↑u) ^ n = (algebraMap R S) (a * ↑u ^ n)