-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma away_of_isIdempotentElem_of_mul {R S} [CommSemiring R] [CommSemiring S] [Algebra R S]
    {e : R} (he : IsIdempotentElem e)
    (H : ∀ x y, algebraMap R S x = algebraMap R S y ↔ e * x = e * y)
    (H' : Function.Surjective (algebraMap R S)) :
    IsLocalization.Away e S where
  map_units' r

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(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:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ (algebraMap R S) e = 1

Tactic:
rw [← (algebraMap R S).map_one, H, mul_one, he]

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : S
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

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

Result:
case intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : R
⊢ ∃ x, (algebraMap R S) z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Proof state:
case intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(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
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
r : ↥(Submonoid.powers e)
⊢ IsUnit ((algebraMap R S) ↑r)

Tactic:
obtain ⟨r, n, rfl⟩ := r

Result:
case mk.intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x => e ^ x) n, ⋯⟩)

Proof state:
case mk.intro
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ IsUnit ((algebraMap R S) ↑⟨(fun x => e ^ x) n, ⋯⟩)

Tactic:
simp [show algebraMap R S e = 1 by rw [← (algebraMap R S).map_one, H, mul_one, he]]

Result:
no goals