-- Mathlib/RingTheory/Localization/Defs.lean
theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) :
    haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
    IsLocalization (M.map h.toMonoidHom) S

Proof state:
case map_units'.mk.intro.intro
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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : R
hy : y ∈ ↑M
⊢ IsUnit ((algebraMap P S) ↑⟨h.toMonoidHom y, ⋯⟩)

Tactic:
convert IsLocalization.map_units S ⟨y, hy⟩

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : R
hy : y ∈ ↑M
⊢ (algebraMap P S) ↑⟨h.toMonoidHom y, ⋯⟩ = (algebraMap R S) ↑⟨y, hy⟩

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ y * (algebraMap R S) (h.symm.toRingHom (h.toMonoidHom ↑s)) = (algebraMap R S) (h.symm.toRingHom (h x))

Tactic:
convert e <;> exact h.symm_apply_apply _

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply,
  IsLocalization.eq_iff_exists M S]

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (∃ c, ↑c * h.symm.toRingHom x = ↑c * h.symm.toRingHom y) → ∃ c, ↑c * x = ↑c * 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✝ : IsLocalization M S
h : R ≃+* P
⊢ IsLocalization (Submonoid.map h.toMonoidHom M) S

Tactic:
letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra

Result:
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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ IsLocalization (Submonoid.map h.toMonoidHom M) S

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (∃ c, ↑c * h.symm.toRingHom x = ↑c * h.symm.toRingHom y) → ∃ c, ↑c * x = ↑c * y

Tactic:
simp [← h.toEquiv.apply_eq_iff_eq]

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ ∀ {x y : P}, (algebraMap P S) x = (algebraMap P S) 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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : R
hy : y ∈ ↑M
⊢ (algebraMap P S) ↑⟨h.toMonoidHom y, ⋯⟩ = (algebraMap R S) ↑⟨y, hy⟩

Tactic:
dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : R
hy : y ∈ ↑M
⊢ (algebraMap R S) (h.symm.toRingHom (h.toMonoidHom y)) = (algebraMap R S) y

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : R
hy : y ∈ ↑M
⊢ (algebraMap R S) (h.symm.toRingHom (h.toMonoidHom y)) = (algebraMap R S) y

Tactic:
exact congr_arg _ (h.symm_apply_apply _)

Result:
no goals

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ IsLocalization (Submonoid.map h.toMonoidHom M) S

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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ ∀ (y : ↥(Submonoid.map h.toMonoidHom M)), IsUnit ((algebraMap P S) ↑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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ ∀ (z : S), ∃ x, z * (algebraMap P S) ↑x.2 = (algebraMap P S) 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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
⊢ ∀ {x y : P}, (algebraMap P S) x = (algebraMap P S) 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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
⊢ ∃ x, y * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M 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✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ x, y * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1