case intro.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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
b' : P
b'_mem : b' ∈ I
hb' : ↑(AlgHom.toLinearMap g) b' = b
⊢ IsInteger R (a • b)
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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
⊢ IsInteger R (a • b)
obtain ⟨b', b'_mem, hb'⟩ := Submodule.mem_map.mp hb
case intro.intro.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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
b' : P
b'_mem : b' ∈ I
hb' : ↑(AlgHom.toLinearMap g) b' = b
x : R
hx : ↑(algebraMap R P) x = a • b'
⊢ IsInteger R (a • b)
case intro.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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
b' : P
b'_mem : b' ∈ I
hb' : ↑(AlgHom.toLinearMap g) b' = b
⊢ IsInteger R (a • b)
obtain ⟨x, hx⟩ := hI b' b'_mem
case intro.intro.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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
b' : P
b'_mem : b' ∈ I
hb' : ↑(AlgHom.toLinearMap g) b' = b
x : R
hx : ↑(algebraMap R P) x = a • b'
⊢ ↑(algebraMap R P') x = a • b
case intro.intro.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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
b' : P
b'_mem : b' ∈ I
hb' : ↑(AlgHom.toLinearMap g) b' = b
x : R
hx : ↑(algebraMap R P) x = a • b'
⊢ IsInteger R (a • b)
use x
no goals
case intro.intro.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
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
loc' : IsLocalization S P'
P'' : Type ?u.518529
inst✝¹ : CommRing P''
inst✝ : Algebra R P''
loc'' : IsLocalization S P''
g : P →ₐ[R] P'
I : Submodule R P
a : R
a_nonzero : a ∈ S
hI : ∀ (b : P), b ∈ I → IsInteger R (a • b)
b : P'
hb : b ∈ Submodule.map (AlgHom.toLinearMap g) I
b' : P
b'_mem : b' ∈ I
hb' : ↑(AlgHom.toLinearMap g) b' = b
x : R
hx : ↑(algebraMap R P) x = a • b'
⊢ ↑(algebraMap R P') x = a • b
erw [← g.commutes, hx, g.map_smul, hb']