-- Mathlib/RingTheory/Localization/Basic.lean
theorem isLocalization_of_algEquiv [Algebra R P] [IsLocalization M S] (h : S ≃ₐ[R] P) :
    IsLocalization M P

Proof state:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ {x y : R}, (algebraMap R P) x = (algebraMap R P) y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro x y

Result:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ (algebraMap R P) x = (algebraMap R P) y → ∃ c, ↑c * x = ↑c * y

Proof state:
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (y : ↥M), IsUnit ((algebraMap R P) ↑y)

Tactic:
intro y

Result:
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ IsUnit ((algebraMap R P) ↑y)

Proof state:
case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (z : P), ∃ x, z * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
intro y

Result:
case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Proof state:
case h.e'_3
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ (algebraMap R P) ↑y = ↑(↑h).toRingHom ((algebraMap R S) ↑y)

Tactic:
exact (h.commutes y).symm

Result:
no goals

Proof state:
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : y * (algebraMap R P) ↑s = (algebraMap R P) x
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
exact ⟨⟨x, s⟩, e⟩

Result:
no goals

Proof state:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ (algebraMap R P) x = (algebraMap R P) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ←
  h.symm.commutes]

Result:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) →
    h.symm ((algebraMap R P) x) = h.symm ((algebraMap R P) y)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ IsLocalization M P

Tactic:
constructor

Result:
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (y : ↥M), IsUnit ((algebraMap R P) ↑y)

case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (z : P), ∃ x, z * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ {x y : R}, (algebraMap R P) x = (algebraMap R P) y → ∃ c, ↑c * x = ↑c * y

Proof state:
case surj'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)

Result:
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : h.symm y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Proof state:
case map_units'
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ IsUnit ((algebraMap R P) ↑y)

Tactic:
convert (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom

Result:
case h.e'_3
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ (algebraMap R P) ↑y = ↑(↑h).toRingHom ((algebraMap R S) ↑y)

Proof state:
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : h.symm y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
apply_fun (show S → P from h) at e

Result:
case surj'.intro.mk
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  (let_fun this := ⇑h;
      this)
      (h.symm y * (algebraMap R S) ↑(x, s).2) =
    (let_fun this := ⇑h;
      this)
      ((algebraMap R S) (x, s).1)
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Proof state:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) →
    h.symm ((algebraMap R P) x) = h.symm ((algebraMap R P) y)

Tactic:
exact id

Result:
no goals