-- Mathlib/RingTheory/Localization/LocalizationLocalization.lean
theorem isFractionRing_of_isLocalization (S T : Type*) [CommRing S] [CommRing T] [Algebra R S]
    [Algebra R T] [Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsFractionRing R T]
    (hM : M ≤ nonZeroDivisors R) : IsFractionRing S T

Proof state:
case h.a.a
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * x = 0

Tactic:
rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
  zero_mul]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ (algebraMap R S) ↑s * ↑⟨x, hx⟩ ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
rw [mul_comm, Subtype.coe_mk, e]

Result:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ (algebraMap R S) (y, s).1 ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Proof state:
case h.a
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z = 0

Tactic:
apply hx

Result:
case h.a.a
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * x = 0

Proof state:
case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ ∀ (x : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
rintro ⟨x, hx⟩

Result:
case refine_2.mk
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
⊢ ∃ m, m * ↑⟨x, hx⟩ ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ IsFractionRing S T

Tactic:
refine @isLocalization_of_is_exists_mul_mem _ _ _ _ _ _ _ this ?_ ?_

Result:
case refine_1
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S

case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
⊢ ∀ (x : ↥(nonZeroDivisors S)), ∃ m, m * ↑x ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Proof state:
case h.a
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z = (algebraMap R S) 0

Tactic:
rw [map_zero]

Result:
case h.a
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
hx : x ∈ nonZeroDivisors S
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z = 0