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

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

Tactic:
refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩

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

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

Proof state:
case h.e'_3.hf
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ Injective ⇑h.symm.toMulEquiv.symm.toMonoidHom

Tactic:
exact h.toEquiv.injective

Result:
no goals

Proof state:
case h.e'_6
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ inst✝¹ = ((algebraMap R S).comp (h.symm.toRingHom.comp h.symm.symm.toRingHom)).toAlgebra

Tactic:
simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom]

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

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

Tactic:
intro H

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

Proof state:
case h.e'_6.h
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
r : R
⊢ (algebraMap R S) r = (algebraMap R S) r

Tactic:
rw [RingHom.algebraMap_toAlgebra]

Result:
no goals

Proof state:
case h.e'_6.h
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ ∀ (r : R), (algebraMap R S) r = (algebraMap R S) r

Tactic:
intro r

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

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

Tactic:
erw [Submonoid.map_equiv_eq_comap_symm, Submonoid.comap_map_eq_of_injective]

Result:
case h.e'_3.hf
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ Injective ⇑h.symm.toMulEquiv.symm.toMonoidHom

Proof state:
case h.e'_6
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ inst✝¹ = (algebraMap R S).toAlgebra

Tactic:
apply Algebra.algebra_ext

Result:
case h.e'_6.h
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ ∀ (r : R), (algebraMap R S) r = (algebraMap R S) r

Proof state:
case h.e'_6
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ inst✝¹ = ((algebraMap P S).comp h.symm.symm.toRingHom).toAlgebra

Tactic:
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc]

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