[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
⊢ ∀ (y : { x // x ∈ nonZeroDivisors ℤ }), IsUnit (↑(algebraMap ℤ ℚ) ↑y)
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x : ℤ
hx : x ∈ nonZeroDivisors ℤ
⊢ IsUnit (↑(algebraMap ℤ ℚ) ↑{ val := x, property := hx })
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff_ne_zero] at hx 
[GOAL]
case mk
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x : ℤ
hx✝ : x ∈ nonZeroDivisors ℤ
hx : x ≠ 0
⊢ IsUnit (↑(algebraMap ℤ ℚ) ↑{ val := x, property := hx✝ })
[PROOFSTEP]
simpa only [eq_intCast, isUnit_iff_ne_zero, Int.cast_eq_zero, Ne.def, Subtype.coe_mk] using hx
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
⊢ ∀ (z : ℚ), ∃ x, z * ↑(algebraMap ℤ ℚ) ↑x.snd = ↑(algebraMap ℤ ℚ) x.fst
[PROOFSTEP]
rintro ⟨n, d, hd, h⟩
[GOAL]
case mk'
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : Nat.coprime (Int.natAbs n) d
⊢ ∃ x, mk' n d * ↑(algebraMap ℤ ℚ) ↑x.snd = ↑(algebraMap ℤ ℚ) x.fst
[PROOFSTEP]
refine' ⟨⟨n, ⟨d, _⟩⟩, Rat.mul_den_eq_num⟩
[GOAL]
case mk'
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : Nat.coprime (Int.natAbs n) d
⊢ ↑d ∈ nonZeroDivisors ℤ
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff_ne_zero, Int.coe_nat_ne_zero_iff_pos]
[GOAL]
case mk'
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : Nat.coprime (Int.natAbs n) d
⊢ 0 < d
[PROOFSTEP]
exact Nat.zero_lt_of_ne_zero hd
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
⊢ ∀ {x y : ℤ}, ↑(algebraMap ℤ ℚ) x = ↑(algebraMap ℤ ℚ) y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x y : ℤ
⊢ ↑(algebraMap ℤ ℚ) x = ↑(algebraMap ℤ ℚ) y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rw [eq_intCast, eq_intCast, Int.cast_inj]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x y : ℤ
⊢ x = y ↔ ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x y : ℤ
⊢ x = y → ∃ c, ↑c * x = ↑c * y
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x : ℤ
⊢ ∃ c, ↑c * x = ↑c * x
[PROOFSTEP]
use 1
[GOAL]
case mpr
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x y : ℤ
⊢ (∃ c, ↑c * x = ↑c * y) → x = y
[PROOFSTEP]
rintro ⟨⟨c, hc⟩, h⟩
[GOAL]
case mpr.intro.mk
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x y c : ℤ
hc : c ∈ nonZeroDivisors ℤ
h : ↑{ val := c, property := hc } * x = ↑{ val := c, property := hc } * y
⊢ x = y
[PROOFSTEP]
apply mul_left_cancel₀ _ h
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
x y c : ℤ
hc : c ∈ nonZeroDivisors ℤ
h : ↑{ val := c, property := hc } * x = ↑{ val := c, property := hc } * y
⊢ ↑{ val := c, property := hc } ≠ 0
[PROOFSTEP]
rwa [mem_nonZeroDivisors_iff_ne_zero] at hc 
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type u_3
inst✝⁷ : CommRing P
A : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_5
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x * IsFractionRing.inv A x = 1
[PROOFSTEP]
rw [IsFractionRing.inv, dif_neg hx, ←
  IsUnit.mul_left_inj
    (map_units K
      ⟨(sec _ x).1,
        mem_nonZeroDivisors_iff_ne_zero.2 fun h0 => hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
  one_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type u_3
inst✝⁷ : CommRing P
A : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_5
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x *
      (mk' K ↑(sec (nonZeroDivisors A) x).snd
          { val := (sec (nonZeroDivisors A) x).fst,
            property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) } *
        ↑(algebraMap A K)
          ↑{ val := (sec (nonZeroDivisors A) x).fst,
              property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) }) =
    ↑(algebraMap A K)
      ↑{ val := (sec (nonZeroDivisors A) x).fst, property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) }
[PROOFSTEP]
rw [mk'_spec, ← eq_mk'_iff_mul_eq]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type u_3
inst✝⁷ : CommRing P
A : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_5
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
hx : x ≠ 0
⊢ x =
    mk'
      ((fun x => K)
        ↑{ val := (sec (nonZeroDivisors A) x).fst,
            property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) })
      (↑{ val := (sec (nonZeroDivisors A) x).fst,
          property := (_ : (sec (nonZeroDivisors A) x).fst ∈ nonZeroDivisors A) })
      (sec (nonZeroDivisors A) x).snd
[PROOFSTEP]
exact (mk'_sec _ x).symm
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type u_3
inst✝⁷ : CommRing P
A : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_5
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
src✝¹ : IsDomain K := IsFractionRing.isDomain A
src✝ : CommRing K := inferInstanceAs (CommRing K)
⊢ 0⁻¹ = 0
[PROOFSTEP]
change IsFractionRing.inv A (0 : K) = 0
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type u_3
inst✝⁷ : CommRing P
A : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_5
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
src✝¹ : IsDomain K := IsFractionRing.isDomain A
src✝ : CommRing K := inferInstanceAs (CommRing K)
⊢ IsFractionRing.inv A 0 = 0
[PROOFSTEP]
rw [IsFractionRing.inv]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Type u_3
inst✝⁷ : CommRing P
A : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
K : Type u_5
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
src✝¹ : IsDomain K := IsFractionRing.isDomain A
src✝ : CommRing K := inferInstanceAs (CommRing K)
⊢ (if h : 0 = 0 then 0
    else
      mk' K ↑(sec (nonZeroDivisors A) 0).snd
        { val := (sec (nonZeroDivisors A) 0).fst,
          property := (_ : (sec (nonZeroDivisors A) 0).fst ∈ nonZeroDivisors A) }) =
    0
[PROOFSTEP]
exact dif_pos rfl
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
z : K
x y : A
hy : y ∈ nonZeroDivisors A
h : mk' K x { val := y, property := hy } = z
⊢ ↑(algebraMap A K) x / ↑(algebraMap A K) y = z
[PROOFSTEP]
rwa [mk'_eq_div] at h 
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
⊢ mk' K x y = 0 ↔ x = 0
[PROOFSTEP]
refine' ⟨fun hxy => _, fun h => by rw [h, mk'_zero]⟩
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
h : x = 0
⊢ mk' K x y = 0
[PROOFSTEP]
rw [h, mk'_zero]
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
hxy : mk' K x y = 0
⊢ x = 0
[PROOFSTEP]
simp_rw [mk'_eq_zero_iff, mul_left_coe_nonZeroDivisors_eq_zero_iff] at hxy 
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : { x // x ∈ nonZeroDivisors R }
hxy : ∃ m, x = 0
⊢ x = 0
[PROOFSTEP]
exact (exists_const _).mp hxy
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
x : A
y : { x // x ∈ nonZeroDivisors A }
⊢ mk' K x y = 1 ↔ x = ↑y
[PROOFSTEP]
refine' ⟨_, fun hxy => by rw [hxy, mk'_self']⟩
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
x : A
y : { x // x ∈ nonZeroDivisors A }
hxy : x = ↑y
⊢ mk' K x y = 1
[PROOFSTEP]
rw [hxy, mk'_self']
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
x : A
y : { x // x ∈ nonZeroDivisors A }
⊢ mk' K x y = 1 → x = ↑y
[PROOFSTEP]
intro hxy
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
x : A
y : { x // x ∈ nonZeroDivisors A }
hxy : mk' K x y = 1
⊢ x = ↑y
[PROOFSTEP]
have hy : (algebraMap A K) ↑y ≠ (0 : K) := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
x : A
y : { x // x ∈ nonZeroDivisors A }
hxy : mk' K x y = 1
hy : ↑(algebraMap A K) ↑y ≠ 0
⊢ x = ↑y
[PROOFSTEP]
rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy 
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
x : A
y : { x // x ∈ nonZeroDivisors A }
hxy : ↑(algebraMap A K) x = ↑(algebraMap A K) ↑y
hy : ↑(algebraMap A K) ↑y ≠ 0
⊢ x = ↑y
[PROOFSTEP]
exact IsFractionRing.injective A K hxy
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ↑g
x : A
y : { x // x ∈ nonZeroDivisors A }
⊢ ↑(lift hg) (mk' K x y) = ↑g x / ↑g ↑y
[PROOFSTEP]
simp only [mk'_eq_div, map_div₀, lift_algebraMap]
[GOAL]
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
h : A ≃+* B
⊢ Submonoid.map (RingEquiv.toMonoidHom h) (?m.392285 h) = ?m.392287 h
[PROOFSTEP]
ext b
[GOAL]
case h
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
h : A ≃+* B
b : B
⊢ b ∈ Submonoid.map (RingEquiv.toMonoidHom h) (?m.392285 h) ↔ b ∈ ?m.392287 h
[PROOFSTEP]
show b ∈ h.toEquiv '' _ ↔ _
[GOAL]
case h
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
h : A ≃+* B
b : B
⊢ b ∈ ↑h.toEquiv '' ↑(?m.392285 h) ↔ b ∈ ?m.392287 h
[PROOFSTEP]
erw [h.toEquiv.image_eq_preimage, Set.preimage, Set.mem_setOf_eq, mem_nonZeroDivisors_iff_ne_zero,
  mem_nonZeroDivisors_iff_ne_zero]
[GOAL]
case h
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
inst✝⁸ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁷ : CommRing B
inst✝⁶ : IsDomain B
inst✝⁵ : Field K
L : Type u_7
inst✝⁴ : Field L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
g : A →+* L
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
h : A ≃+* B
b : B
⊢ ↑h.symm b ≠ 0 ↔ b ≠ 0
[PROOFSTEP]
exact h.symm.map_ne_zero_iff
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
⊢ IsFractionRing R S ↔ IsFractionRing P S
[PROOFSTEP]
delta IsFractionRing
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
⊢ IsLocalization (nonZeroDivisors R) S ↔ IsLocalization (nonZeroDivisors P) S
[PROOFSTEP]
convert isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h
[GOAL]
case h.e'_2.h.e'_3
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
⊢ nonZeroDivisors P = Submonoid.map (RingEquiv.toMonoidHom h) (nonZeroDivisors R)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ x ∈ Submonoid.map (RingEquiv.toMonoidHom h) (nonZeroDivisors R)
[PROOFSTEP]
erw [Submonoid.map_equiv_eq_comap_symm]
[GOAL]
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔
    x ∈ Submonoid.comap (MulEquiv.toMonoidHom (MulEquiv.symm (RingEquiv.toMulEquiv h))) (nonZeroDivisors R)
[PROOFSTEP]
simp only [MulEquiv.coe_toMonoidHom, RingEquiv.toMulEquiv_eq_coe, Submonoid.mem_comap]
[GOAL]
case h.e'_2.h.e'_3.h
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P ↔ ↑(MulEquiv.symm ↑h) x ∈ nonZeroDivisors R
[PROOFSTEP]
constructor
[GOAL]
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
⊢ x ∈ nonZeroDivisors P → ↑(MulEquiv.symm ↑h) x ∈ nonZeroDivisors R
[PROOFSTEP]
rintro hx z (hz : z * h.symm x = 0)
[GOAL]
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * ↑(RingEquiv.symm h) x = 0
⊢ z = 0
[PROOFSTEP]
rw [← h.map_eq_zero_iff]
[GOAL]
case h.e'_2.h.e'_3.h.mp
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * ↑(RingEquiv.symm h) x = 0
⊢ ↑h z = 0
[PROOFSTEP]
apply hx
[GOAL]
case h.e'_2.h.e'_3.h.mp.a
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
hx : x ∈ nonZeroDivisors P
z : R
hz : z * ↑(RingEquiv.symm h) x = 0
⊢ ↑h z * x = 0
[PROOFSTEP]
simpa only [h.map_zero, h.apply_symm_apply, h.map_mul] using congr_arg h hz
[GOAL]
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
⊢ ↑(MulEquiv.symm ↑h) x ∈ nonZeroDivisors R → x ∈ nonZeroDivisors P
[PROOFSTEP]
rintro (hx : h.symm x ∈ _) z hz
[GOAL]
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
hx : ↑(RingEquiv.symm h) x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ z = 0
[PROOFSTEP]
rw [← h.symm.map_eq_zero_iff]
[GOAL]
case h.e'_2.h.e'_3.h.mpr
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
hx : ↑(RingEquiv.symm h) x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ ↑(RingEquiv.symm h) z = 0
[PROOFSTEP]
apply hx
[GOAL]
case h.e'_2.h.e'_3.h.mpr.a
R : Type u_1
inst✝¹¹ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommRing P
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
K : Type u_5
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : IsDomain B
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
h : R ≃+* P
x : P
hx : ↑(RingEquiv.symm h) x ∈ nonZeroDivisors R
z : P
hz : z * x = 0
⊢ ↑(RingEquiv.symm h) z * ↑(RingEquiv.symm h) x = 0
[PROOFSTEP]
rw [← h.symm.map_mul, hz, h.symm.map_zero]
[GOAL]
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ Nontrivial S
[PROOFSTEP]
apply nontrivial_of_ne
[GOAL]
case h
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ ?x ≠ ?y
case 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_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
case y
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
[PROOFSTEP]
intro h
[GOAL]
case h
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
h : ?x = ?y
⊢ False
case 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_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
case y
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
[PROOFSTEP]
apply @zero_ne_one R
[GOAL]
case h.a
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
h : ?x = ?y
⊢ 0 = 1
case 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_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
case y
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝¹⁵ : CommRing S✝
inst✝¹⁴ : Algebra R✝ S✝
P : Type u_3
inst✝¹³ : CommRing P
A : Type u_4
inst✝¹² : CommRing A
inst✝¹¹ : IsDomain A
K : Type u_5
B : Type u_6
inst✝¹⁰ : CommRing B
inst✝⁹ : IsDomain B
inst✝⁸ : Field K
L : Type u_7
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : IsFractionRing A K
g : A →+* L
R : Type u_8
S : Type u_9
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsFractionRing R S
⊢ S
[PROOFSTEP]
exact
  IsLocalization.injective S (le_of_eq rfl) (((algebraMap R S).map_zero.trans h).trans (algebraMap R S).map_one.symm)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommRing P
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type u_5
r : A
s : { x // x ∈ nonZeroDivisors A }
⊢ Localization.mk r s = ↑(algebraMap A (FractionRing A)) r / ↑(algebraMap A (FractionRing A)) ↑s
[PROOFSTEP]
rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]
[GOAL]
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
inst✝² : IsDomain A
K : Type u_5
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ NoZeroSMulDivisors R (FractionRing A)
[PROOFSTEP]
apply NoZeroSMulDivisors.of_algebraMap_injective
[GOAL]
case h
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
inst✝² : IsDomain A
K : Type u_5
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ Function.Injective ↑(algebraMap R (FractionRing A))
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq R A]
[GOAL]
case h
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
inst✝² : IsDomain A
K : Type u_5
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ Function.Injective ↑(RingHom.comp (algebraMap A (FractionRing A)) (algebraMap R A))
[PROOFSTEP]
apply
  Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective A (FractionRing A))
    (NoZeroSMulDivisors.algebraMap_injective R A)
