R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this : Nontrivial T
⊢ IsFractionRing S T
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
⊢ IsFractionRing S T
haveI := IsFractionRing.nontrivial R T
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
⊢ IsFractionRing S T
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this : Nontrivial T
⊢ IsFractionRing S T
haveI := (algebraMap S T).domain_nontrivial
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
⊢ M ≤ nonZeroDivisors R
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
⊢ IsFractionRing S T
apply isFractionRing_of_isLocalization M S T
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ∈ nonZeroDivisors R
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
⊢ M ≤ nonZeroDivisors R
intro x hx
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ≠ 0
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ∈ nonZeroDivisors R
rw [mem_nonZeroDivisors_iff_ne_zero]
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ False
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
⊢ x ≠ 0
intro hx'
case a
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ 0 = 1
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ False
apply @zero_ne_one S
case a
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ∃ m, ↑m * 1 = 0
case a
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ 0 = 1
rw [← (algebraMap R S).map_one, ← @mk'_one R _ M, @comm _ Eq, mk'_eq_zero_iff]
no goals
case a
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ∃ m, ↑m * 1 = 0
exact ⟨⟨x, hx⟩, by simp [hx']⟩
no goals
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S✝ : Type ?u.712246
inst✝¹¹ : CommRing S✝
inst✝¹⁰ : Algebra R S✝
P : Type ?u.712502
inst✝⁹ : CommRing P
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ↑{ val := x, property := hx } * 1 = 0
simp [hx']