R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
⊢ ∀ (a : S), ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M))) a = 0 → a = 0
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
⊢ Injective ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M)))
rw [injective_iff_map_eq_zero]
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
z : S
hz : ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M))) z = 0
⊢ z = 0
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
⊢ ∀ (a : S), ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M))) a = 0 → a = 0
intro z hz
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
hz : ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M))) (mk' S a b) = 0
⊢ mk' S a b = 0
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
z : S
hz : ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M))) z = 0
⊢ z = 0
obtain ⟨a, b, rfl⟩ := mk'_surjective M z
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
hz : ∃ m, ↑m * ↑g a = 0
⊢ mk' S a b = 0
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
hz : ↑(map Q g (_ : M ≤ Submonoid.comap g (Submonoid.map g M))) (mk' S a b) = 0
⊢ mk' S a b = 0
rw [map_mk', mk'_eq_zero_iff] at hz
case intro.intro.intro.mk
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
hm : ↑{ val := m', property := hm' } * ↑g a = 0
⊢ mk' S a b = 0
case intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
hz : ∃ m, ↑m * ↑g a = 0
⊢ mk' S a b = 0
obtain ⟨⟨m', hm'⟩, hm⟩ := hz
case intro.intro.intro.mk
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm'✝ : m' ∈ Submonoid.map g M
hm' : ∃ x, x ∈ M ∧ ↑g x = m'
hm : ↑{ val := m', property := hm'✝ } * ↑g a = 0
⊢ mk' S a b = 0
case intro.intro.intro.mk
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
hm : ↑{ val := m', property := hm' } * ↑g a = 0
⊢ mk' S a b = 0
rw [Submonoid.mem_map] at hm'
case intro.intro.intro.mk.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
hm : ↑{ val := m', property := hm' } * ↑g a = 0
n : R
hn : n ∈ M
hnm : ↑g n = m'
⊢ mk' S a b = 0
case intro.intro.intro.mk
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm'✝ : m' ∈ Submonoid.map g M
hm' : ∃ x, x ∈ M ∧ ↑g x = m'
hm : ↑{ val := m', property := hm'✝ } * ↑g a = 0
⊢ mk' S a b = 0
obtain ⟨n, hn, hnm⟩ := hm'
case intro.intro.intro.mk.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
n : R
hm : ↑g (n * a) = ↑g 0
hn : n ∈ M
hnm : ↑g n = m'
⊢ mk' S a b = 0
case intro.intro.intro.mk.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
hm : ↑{ val := m', property := hm' } * ↑g a = 0
n : R
hn : n ∈ M
hnm : ↑g n = m'
⊢ mk' S a b = 0
rw [Subtype.coe_mk, ← hnm, ← map_mul, ← map_zero g] at hm
case intro.intro.intro.mk.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
n : R
hm : ↑g (n * a) = ↑g 0
hn : n ∈ M
hnm : ↑g n = m'
⊢ ∃ m, ↑m * a = 0
case intro.intro.intro.mk.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
n : R
hm : ↑g (n * a) = ↑g 0
hn : n ∈ M
hnm : ↑g n = m'
⊢ mk' S a b = 0
rw [mk'_eq_zero_iff]
no goals
case intro.intro.intro.mk.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type u_2
inst✝³ : CommRing P
K : Type ?u.3071941
inst✝² : IsLocalization M S
Q : Type u_3
inst✝¹ : CommRing Q
g : R →+* P
inst✝ : Algebra P Q
hg : Injective ↑g
i : IsLocalization (Submonoid.map g M) Q
a : R
b : { x // x ∈ M }
m' : P
hm' : m' ∈ Submonoid.map g M
n : R
hm : ↑g (n * a) = ↑g 0
hn : n ∈ M
hnm : ↑g n = m'
⊢ ∃ m, ↑m * a = 0
exact ⟨⟨n, hn⟩, hg hm⟩