case refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ (m : P), m ∈ I → ∀ (n : P), n ∈ J → IsInteger R ((aI * aJ) • (m * n))

case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ (x y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ IsInteger R ((aI * aJ) • b)
refine Submodule.mul_induction_on hb ?_ ?_
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
⊢ IsInteger R ((aI * aJ) • (m * n))
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ (m : P), m ∈ I → ∀ (n : P), n ∈ J → IsInteger R ((aI * aJ) • (m * n))
intro m hm n hn
case refine_1.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : ↑(algebraMap R P) n' = aJ • n
⊢ IsInteger R ((aI * aJ) • (m * n))
case refine_1
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
⊢ IsInteger R ((aI * aJ) • (m * n))
obtain ⟨n', hn'⟩ := hJ n hn
case refine_1.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : ↑(algebraMap R P) n' = aJ • n
⊢ IsInteger R (aI • n' • m)
case refine_1.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : ↑(algebraMap R P) n' = aJ • n
⊢ IsInteger R ((aI * aJ) • (m * n))
rw [mul_smul, mul_comm m, ← smul_mul_assoc, ← hn', ← Algebra.smul_def]
case refine_1.intro.a
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : ↑(algebraMap R P) n' = aJ • n
⊢ n' • m ∈ I
case refine_1.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : ↑(algebraMap R P) n' = aJ • n
⊢ IsInteger R (aI • n' • m)
apply hI
no goals
case refine_1.intro.a
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
m : P
hm : m ∈ I
n : P
hn : n ∈ J
n' : R
hn' : ↑(algebraMap R P) n' = aJ • n
⊢ n' • m ∈ I
exact Submodule.smul_mem _ _ hm
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • (x + y))
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
⊢ ∀ (x y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))
intro x y hx hy
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • x + (aI * aJ) • y)
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • (x + y))
rw [smul_add]
no goals
case refine_2
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (aI • b)
aJ : R
haJ : aJ ∈ S
hJ : ∀ (b : P), b ∈ J → IsInteger R (aJ • b)
b : P
hb : b ∈ I * J
x y : P
hx : IsInteger R ((aI * aJ) • x)
hy : IsInteger R ((aI * aJ) • y)
⊢ IsInteger R ((aI * aJ) • x + (aI * aJ) • y)
apply isInteger_add hx hy