-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem away_of_isUnit_of_bijective {R : Type*} (S : Type*) [CommSemiring R] [CommSemiring S]
    [Algebra R S] {r : R} (hr : IsUnit r) (H : Function.Bijective (algebraMap R S)) :
    IsLocalization.Away r S :=
  { map_units'

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [H.1.eq_iff]

Result:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
x y : R
⊢ x = y → ∃ c, ↑c * x = ↑c * y

Proof state:
case intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
z' : R
⊢ ∃ x, (algebraMap R S) z' * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
exact ⟨⟨z', 1⟩, by simp⟩

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
x y : R
⊢ x = y → ∃ c, ↑c * x = ↑c * y

Tactic:
rintro rfl

Result:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
x : R
⊢ ∃ c, ↑c * x = ↑c * x

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
obtain ⟨z', rfl⟩ := H.2 z

Result:
case intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
z' : R
⊢ ∃ x, (algebraMap R S) z' * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
⊢ ∀ (y : ↥(Submonoid.powers r)), IsUnit ((algebraMap R S) ↑y)

Tactic:
rintro ⟨_, n, rfl⟩

Result:
case mk.intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x => r ^ x) n, ⋯⟩)

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
x : R
⊢ ∃ c, ↑c * x = ↑c * x

Tactic:
exact ⟨1, rfl⟩

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
z' : R
⊢ (algebraMap R S) z' * (algebraMap R S) ↑(z', 1).2 = (algebraMap R S) (z', 1).1

Tactic:
simp

Result:
no goals

Proof state:
case mk.intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
hr : IsUnit r
H : Function.Bijective ⇑(algebraMap R S)
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x => r ^ x) n, ⋯⟩)

Tactic:
exact (algebraMap R S).isUnit_map (hr.pow _)

Result:
no goals