R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x * ↑(algebraMap R S) ↑(sec M x).snd = ↑(algebraMap R S) (sec M x).fst
⊢ (sec M x).fst ≠ 0
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
⊢ (sec M x).fst ≠ 0
have hsec := sec_spec M x
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x * ↑(algebraMap R S) ↑(sec M x).snd = ↑(algebraMap R S) (sec M x).fst
hfst : (sec M x).fst = 0
⊢ False
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x * ↑(algebraMap R S) ↑(sec M x).snd = ↑(algebraMap R S) (sec M x).fst
⊢ (sec M x).fst ≠ 0
intro hfst
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x = 0 ∨ ↑(sec M x).snd = 0
hfst : (sec M x).fst = 0
⊢ False

case hf
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x = 0 ∨ ↑(algebraMap R S) ↑(sec M x).snd = 0
hfst : (sec M x).fst = 0
⊢ Injective ↑(algebraMap R S)
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x * ↑(algebraMap R S) ↑(sec M x).snd = ↑(algebraMap R S) (sec M x).fst
hfst : (sec M x).fst = 0
⊢ False
rw [hfst, map_zero, mul_eq_zero, _root_.map_eq_zero_iff] at hsec
no goals
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x = 0 ∨ ↑(sec M x).snd = 0
hfst : (sec M x).fst = 0
⊢ False
exact Or.elim hsec hx (sec_snd_ne_zero hM x)
no goals
case hf
R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Type ?u.3066574
inst✝³ : CommRing P
K : Type ?u.3066580
inst✝² : IsLocalization M S
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors S
hM : M ≤ nonZeroDivisors R
x : S
hx : x ≠ 0
hsec : x = 0 ∨ ↑(algebraMap R S) ↑(sec M x).snd = 0
hfst : (sec M x).fst = 0
⊢ Injective ↑(algebraMap R S)
exact IsLocalization.injective S hM