-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem isFractionRing_iff_of_base_ringEquiv (h : R ≃+* P) :
    IsFractionRing R S ↔
      @IsFractionRing P _ S _ ((algebraMap R S).comp h.symm.toRingHom).toAlgebra

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ IsFractionRing R S ↔ IsFractionRing P S

Tactic:
delta IsFractionRing

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ IsLocalization (nonZeroDivisors R) S ↔ IsLocalization (nonZeroDivisors P) S

Proof state:
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P → (↑h).symm x ∈ nonZeroDivisors R

Tactic:
rintro hx z (hz : z * h.symm x = 0)

Result:
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * h.symm x = 0
⊢ z = 0

Proof state:
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.map h.toMonoidHom (nonZeroDivisors R)

Tactic:
erw [Submonoid.map_equiv_eq_comap_symm]

Result:
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.comap h.toMulEquiv.symm.toMonoidHom (nonZeroDivisors R)

Proof state:
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : h.symm x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ h.symm z = 0

Tactic:
apply hx

Result:
case h.e'_2.h.e'_3.h.mpr.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : h.symm x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ h.symm z * h.symm x = 0

Proof state:
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.comap h.toMulEquiv.symm.toMonoidHom (nonZeroDivisors R)

Tactic:
simp only [MulEquiv.coe_toMonoidHom, RingEquiv.toMulEquiv_eq_coe, Submonoid.mem_comap]

Result:
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ (↑h).symm x ∈ nonZeroDivisors R

Proof state:
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ (↑h).symm x ∈ nonZeroDivisors R → x ∈ nonZeroDivisors P

Tactic:
rintro (hx : h.symm x ∈ _) z hz

Result:
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : h.symm x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ z = 0

Proof state:
case h.e'_2.h.e'_3.h.mp.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * h.symm x = 0
⊢ h z * x = 0

Tactic:
simpa only [h.map_zero, h.apply_symm_apply, h.map_mul] using congr_arg h hz

Result:
no goals

Proof state:
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * h.symm x = 0
⊢ z = 0

Tactic:
rw [← h.map_eq_zero_iff]

Result:
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * h.symm x = 0
⊢ h z = 0

Proof state:
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : h.symm x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ z = 0

Tactic:
rw [← h.symm.map_eq_zero_iff]

Result:
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : h.symm x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ h.symm z = 0

Proof state:
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ (↑h).symm x ∈ nonZeroDivisors R

Tactic:
constructor

Result:
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P → (↑h).symm x ∈ nonZeroDivisors R

case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ (↑h).symm x ∈ nonZeroDivisors R → x ∈ nonZeroDivisors P

Proof state:
case h.e'_2.h.e'_3
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ nonZeroDivisors P = Submonoid.map h.toMonoidHom (nonZeroDivisors R)

Tactic:
ext x

Result:
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.map h.toMonoidHom (nonZeroDivisors R)

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ IsLocalization (nonZeroDivisors R) S ↔ IsLocalization (nonZeroDivisors P) S

Tactic:
convert isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h

Result:
case h.e'_2.h.e'_3
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ nonZeroDivisors P = Submonoid.map h.toMonoidHom (nonZeroDivisors R)

Proof state:
case h.e'_2.h.e'_3.h.mpr.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : h.symm x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ h.symm z * h.symm x = 0

Tactic:
rw [← h.symm.map_mul, hz, h.symm.map_zero]

Result:
no goals

Proof state:
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * h.symm x = 0
⊢ h z = 0

Tactic:
apply hx

Result:
case h.e'_2.h.e'_3.h.mp.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * h.symm x = 0
⊢ h z * x = 0