case intro.intro
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
⊢ IsFractional R₁⁰ (I / J)
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
⊢ IsFractional R₁⁰ (I / J)
obtain ⟨y, mem_J, not_mem_zero⟩ :=
  SetLike.exists_of_lt (show 0 < J by simpa only using bot_lt_iff_ne_bot.mpr h)
case intro.intro.intro
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ IsFractional R₁⁰ (I / J)
case intro.intro
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
⊢ IsFractional R₁⁰ (I / J)
obtain ⟨y', hy'⟩ := hJ y mem_J
case intro.intro.intro
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ aI * y' ∈ R₁⁰ ∧ ∀ (b : K), b ∈ I / J → IsInteger R₁ ((aI * y') • b)
case intro.intro.intro
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ IsFractional R₁⁰ (I / J)
use aI * y'
case intro.intro.intro.left
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ aI * y' ∈ R₁⁰

case intro.intro.intro.right
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ ∀ (b : K), b ∈ I / J → IsInteger R₁ ((aI * y') • b)
case intro.intro.intro
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ aI * y' ∈ R₁⁰ ∧ ∀ (b : K), b ∈ I / J → IsInteger R₁ ((aI * y') • b)
constructor
case intro.intro.intro.right
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ IsInteger R₁ ((aI * y') • b)
case intro.intro.intro.right
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ ∀ (b : K), b ∈ I / J → IsInteger R₁ ((aI * y') • b)
intro b hb
case h.e'_6
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * aJ • y)
case intro.intro.intro.right
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ IsInteger R₁ ((aI * y') • b)
convert hI _ (hb _ (Submodule.smul_mem _ aJ mem_J)) using 1
no goals
case h.e'_6
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * aJ • y)
rw [← hy', mul_comm b, ← Algebra.smul_def, mul_smul]
no goals
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
⊢ 0 < J
simpa only using bot_lt_iff_ne_bot.mpr h
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ y' ≠ 0
case intro.intro.intro.left
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ aI * y' ∈ R₁⁰
apply (nonZeroDivisors R₁).mul_mem haI (mem_nonZeroDivisors_iff_ne_zero.mpr _)
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ False
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
⊢ y' ≠ 0
intro y'_eq_zero
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
this : ↑(algebraMap R₁ K) aJ * y = 0
⊢ False
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ False
have : algebraMap R₁ K aJ * y = 0 := by
  rw [← Algebra.smul_def, ← hy', y'_eq_zero, RingHom.map_zero]
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
this : ↑(algebraMap R₁ K) aJ * y = 0
y_zero : y = 0
⊢ False
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
this : ↑(algebraMap R₁ K) aJ * y = 0
⊢ False
have y_zero :=
  (mul_eq_zero.mp this).resolve_left
    (mt ((injective_iff_map_eq_zero (algebraMap R₁ K)).1 (IsFractionRing.injective _ _) _)
      (mem_nonZeroDivisors_iff_ne_zero.mp haJ))
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
this : ↑(algebraMap R₁ K) aJ * y = 0
y_zero : y = 0
⊢ y ∈ 0
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
this : ↑(algebraMap R₁ K) aJ * y = 0
y_zero : y = 0
⊢ False
apply not_mem_zero
no goals
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
this : ↑(algebraMap R₁ K) aJ * y = 0
y_zero : y = 0
⊢ y ∈ 0
simpa
no goals
R : Type ?u.1138684
inst✝⁶ : CommRing R
S : Submonoid R
P : Type ?u.1138891
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝³ : CommRing R₁
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ (b : K), b ∈ I → IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ (b : K), b ∈ J → IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
not_mem_zero : ¬y ∈ 0
y' : R₁
hy' : ↑(algebraMap R₁ K) y' = aJ • y
y'_eq_zero : y' = 0
⊢ ↑(algebraMap R₁ K) aJ * y = 0
rw [← Algebra.smul_def, ← hy', y'_eq_zero, RingHom.map_zero]