[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : LinearIndependent R b
⊢ LinearIndependent Rₛ b
[PROOFSTEP]
rw [linearIndependent_iff'] at hli ⊢
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
⊢ ∀ (s : Finset ι) (g : ι → Rₛ), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
[PROOFSTEP]
intro s g hg i hi
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i : ι
hi : i ∈ s
⊢ g i = 0
[PROOFSTEP]
choose! a g' hg' using IsLocalization.exist_integer_multiples S s g
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
⊢ g i = 0
[PROOFSTEP]
specialize hli s g' _ i hi
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
⊢ ∑ i in s, g' i • b i = 0
[PROOFSTEP]
rw [← @smul_zero _ M _ _ (a : R), ← hg, Finset.smul_sum]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
⊢ ∑ i in s, g' i • b i = ∑ x in s, ↑a • g x • b x
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i hi => _
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
hli : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i✝ : ι
hi✝ : i✝ ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
i : ι
hi : i ∈ s
⊢ g' i • b i = ↑a • g i • b i
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_smul Rₛ, hg' i hi, smul_assoc]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
hli : g' i = 0
⊢ g i = 0
[PROOFSTEP]
refine' (IsLocalization.map_units Rₛ a).mul_right_eq_zero.mp _
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing Rₛ
inst✝⁴ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_4
b : ι → M
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • b i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
hli : g' i = 0
⊢ ↑(algebraMap R Rₛ) ↑a * g i = 0
[PROOFSTEP]
rw [← Algebra.smul_def, ← map_zero (algebraMap R Rₛ), ← hli, hg' i hi]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : LinearIndependent R v
⊢ LinearIndependent Rₛ (↑(algebraMap A Aₛ) ∘ v)
[PROOFSTEP]
rw [linearIndependent_iff'] at hv ⊢
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
⊢ ∀ (s : Finset ι) (g : ι → Rₛ), ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0 → ∀ (i : ι), i ∈ s → g i = 0
[PROOFSTEP]
intro s g hg i hi
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
⊢ g i = 0
[PROOFSTEP]
choose! a g' hg' using IsLocalization.exist_integer_multiples S s g
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
⊢ g i = 0
[PROOFSTEP]
have h0 : algebraMap A Aₛ (∑ i in s, g' i • v i) = 0 :=
  by
  apply_fun (· • ·) (a : R) at hg
  rw [smul_zero, Finset.smul_sum] at hg
  rw [map_sum, ← hg]
  refine' Finset.sum_congr rfl fun i hi => _
  rw [← smul_assoc, ← hg' i hi, Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← Algebra.smul_def,
    algebraMap_smul, Function.comp_apply]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
⊢ ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
[PROOFSTEP]
apply_fun (· • ·) (a : R) at hg
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
hg : ↑a • ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = ↑a • 0
⊢ ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
[PROOFSTEP]
rw [smul_zero, Finset.smul_sum] at hg
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
hg : ∑ x in s, ↑a • g x • (↑(algebraMap A Aₛ) ∘ v) x = 0
⊢ ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
[PROOFSTEP]
rw [map_sum, ← hg]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
hg : ∑ x in s, ↑a • g x • (↑(algebraMap A Aₛ) ∘ v) x = 0
⊢ ∑ x in s, ↑(algebraMap A Aₛ) (g' x • v x) = ∑ x in s, ↑a • g x • (↑(algebraMap A Aₛ) ∘ v) x
[PROOFSTEP]
refine' Finset.sum_congr rfl fun i hi => _
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
i✝ : ι
hi✝ : i✝ ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
hg : ∑ x in s, ↑a • g x • (↑(algebraMap A Aₛ) ∘ v) x = 0
i : ι
hi : i ∈ s
⊢ ↑(algebraMap A Aₛ) (g' i • v i) = ↑a • g i • (↑(algebraMap A Aₛ) ∘ v) i
[PROOFSTEP]
rw [← smul_assoc, ← hg' i hi, Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← Algebra.smul_def,
  algebraMap_smul, Function.comp_apply]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
h0 : ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
⊢ g i = 0
[PROOFSTEP]
obtain ⟨⟨_, r, hrS, rfl⟩, hr : algebraMap R A r * _ = 0⟩ :=
  (IsLocalization.map_eq_zero_iff (Algebra.algebraMapSubmonoid A S) _ _).1 h0
[GOAL]
case intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
h0 : ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
r : R
hrS : r ∈ ↑S
hr : ↑(algebraMap R A) r * ∑ i in s, g' i • v i = 0
⊢ g i = 0
[PROOFSTEP]
simp_rw [Finset.mul_sum, ← Algebra.smul_def, smul_smul] at hr
[GOAL]
case intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
h0 : ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
r : R
hrS : r ∈ ↑S
hr : ∑ x in s, (r * g' x) • v x = 0
⊢ g i = 0
[PROOFSTEP]
specialize hv s _ hr i hi
[GOAL]
case intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
h0 : ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
r : R
hrS : r ∈ ↑S
hr : ∑ x in s, (r * g' x) • v x = 0
hv : r * g' i = 0
⊢ g i = 0
[PROOFSTEP]
rw [← (IsLocalization.map_units Rₛ a).mul_right_eq_zero, ← Algebra.smul_def, ← hg' i hi]
[GOAL]
case intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
v : ι → A
s : Finset ι
g : ι → Rₛ
hg : ∑ i in s, g i • (↑(algebraMap A Aₛ) ∘ v) i = 0
i : ι
hi : i ∈ s
a : { x // x ∈ S }
g' : ι → R
hg' : ∀ (i : ι), i ∈ s → ↑(algebraMap R Rₛ) (g' i) = ↑a • g i
h0 : ↑(algebraMap A Aₛ) (∑ i in s, g' i • v i) = 0
r : R
hrS : r ∈ ↑S
hr : ∑ x in s, (r * g' x) • v x = 0
hv : r * g' i = 0
⊢ ↑(algebraMap R Rₛ) (g' i) = 0
[PROOFSTEP]
exact (IsLocalization.map_eq_zero_iff S _ _).2 ⟨⟨r, hrS⟩, hv⟩
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
⊢ span Rₛ (↑(algebraMap A Aₛ) '' v) = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
⊢ ⊤ ≤ span Rₛ (↑(algebraMap A Aₛ) '' v)
[PROOFSTEP]
rintro a' -
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a' : Aₛ
⊢ a' ∈ span Rₛ (↑(algebraMap A Aₛ) '' v)
[PROOFSTEP]
obtain ⟨a, ⟨_, s, hs, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid A S) a'
[GOAL]
case intro.intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a : A
s : R
hs : s ∈ ↑S
⊢ IsLocalization.mk' Aₛ a
      { val := ↑(algebraMap R A) s, property := (_ : ∃ a, a ∈ ↑S ∧ ↑(algebraMap R A) a = ↑(algebraMap R A) s) } ∈
    span Rₛ (↑(algebraMap A Aₛ) '' v)
[PROOFSTEP]
rw [IsLocalization.mk'_eq_mul_mk'_one, mul_comm, ← map_one (algebraMap R A)]
[GOAL]
case intro.intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a : A
s : R
hs : s ∈ ↑S
⊢ IsLocalization.mk' Aₛ (↑(algebraMap R A) 1)
        { val := ↑(algebraMap R A) s, property := (_ : ∃ a, a ∈ ↑S ∧ ↑(algebraMap R A) a = ↑(algebraMap R A) s) } *
      ↑(algebraMap A Aₛ) a ∈
    span Rₛ (↑(algebraMap A Aₛ) '' v)
[PROOFSTEP]
erw [← IsLocalization.algebraMap_mk' A Rₛ Aₛ (1 : R) ⟨s, hs⟩]
  -- `erw` needed to unify `⟨s, hs⟩`
[GOAL]
case intro.intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a : A
s : R
hs : s ∈ ↑S
⊢ ↑(algebraMap Rₛ Aₛ) (IsLocalization.mk' Rₛ 1 { val := s, property := hs }) * ↑(algebraMap A Aₛ) a ∈
    span Rₛ (↑(algebraMap A Aₛ) '' v)
[PROOFSTEP]
rw [← Algebra.smul_def]
[GOAL]
case intro.intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a : A
s : R
hs : s ∈ ↑S
⊢ IsLocalization.mk' Rₛ 1 { val := s, property := hs } • ↑(algebraMap A Aₛ) a ∈ span Rₛ (↑(algebraMap A Aₛ) '' v)
[PROOFSTEP]
refine' smul_mem _ _ (span_subset_span R Rₛ _ _)
[GOAL]
case intro.intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a : A
s : R
hs : s ∈ ↑S
⊢ ↑(algebraMap A Aₛ) a ∈ ↑(span R (↑(algebraMap A Aₛ) '' v))
[PROOFSTEP]
rw [← Algebra.coe_linearMap, ← LinearMap.coe_restrictScalars R, ← LinearMap.map_span]
[GOAL]
case intro.intro.mk.intro.intro
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
v : Set A
hv : span R v = ⊤
a : A
s : R
hs : s ∈ ↑S
⊢ ↑(↑R (Algebra.linearMap A Aₛ)) a ∈ ↑(map (↑R (Algebra.linearMap A Aₛ)) (span R v))
[PROOFSTEP]
exact mem_map_of_mem (hv.symm ▸ mem_top)
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
⊢ ⊤ ≤ span Rₛ (Set.range (↑(algebraMap A Aₛ) ∘ ↑b))
[PROOFSTEP]
rw [Set.range_comp, SpanEqTop.localization_localization Rₛ S Aₛ b.span_eq]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x : A
i : ι
⊢ ↑(↑(localizationLocalization Rₛ S Aₛ b).repr (↑(algebraMap A Aₛ) x)) i =
    ↑(↑(localizationLocalization Rₛ S Aₛ b).repr
          (Finsupp.sum (↑b.repr x) fun j c => ↑(algebraMap R Rₛ) c • ↑(algebraMap A Aₛ) (↑b j)))
      i
[PROOFSTEP]
simp_rw [IsScalarTower.algebraMap_smul, Algebra.smul_def, IsScalarTower.algebraMap_apply R A Aₛ, ← _root_.map_mul, ←
  map_finsupp_sum, ← Algebra.smul_def, ← Finsupp.total_apply, Basis.total_repr]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x : A
i : ι
⊢ ↑(↑(localizationLocalization Rₛ S Aₛ b).repr
          (Finsupp.sum (↑b.repr x) fun j c => ↑(algebraMap R Rₛ) c • ↑(algebraMap A Aₛ) (↑b j)))
      i =
    Finsupp.sum (↑b.repr x) fun j c => ↑(algebraMap R Rₛ) c • ↑(Finsupp.single j 1) i
[PROOFSTEP]
simp_rw [← b.localizationLocalization_apply Rₛ S Aₛ, map_finsupp_sum, LinearEquiv.map_smul, Basis.repr_self,
  Finsupp.sum_apply, Finsupp.smul_apply]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x : A
i j : ι
x✝ : j ∈ (↑b.repr x).support
hj : j ≠ i
⊢ (fun j c => ↑(algebraMap R Rₛ) c • ↑(Finsupp.single j 1) i) j (↑(↑b.repr x) j) = 0
[PROOFSTEP]
simp [hj]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x : A
i : ι
hi : ¬i ∈ (↑b.repr x).support
⊢ (fun j c => ↑(algebraMap R Rₛ) c • ↑(Finsupp.single j 1) i) i (↑(↑b.repr x) i) = 0
[PROOFSTEP]
simp [Finsupp.not_mem_support_iff.mp hi]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x : A
i : ι
⊢ (fun j c => ↑(algebraMap R Rₛ) c • ↑(Finsupp.single j 1) i) i (↑(↑b.repr x) i) = ↑(algebraMap R Rₛ) (↑(↑b.repr x) i)
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
⊢ span R (Set.range ↑(localizationLocalization Rₛ S Aₛ b)) = span R (↑(IsScalarTower.toAlgHom R A Aₛ) '' Set.range ↑b)
[PROOFSTEP]
congr
[GOAL]
case e_s
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
⊢ Set.range ↑(localizationLocalization Rₛ S Aₛ b) = ↑(IsScalarTower.toAlgHom R A Aₛ) '' Set.range ↑b
[PROOFSTEP]
ext
[GOAL]
case e_s.h
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
x✝ : Aₛ
⊢ x✝ ∈ Set.range ↑(localizationLocalization Rₛ S Aₛ b) ↔ x✝ ∈ ↑(IsScalarTower.toAlgHom R A Aₛ) '' Set.range ↑b
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
⊢ span R (↑(IsScalarTower.toAlgHom R A Aₛ) '' Set.range ↑b) =
    map (IsScalarTower.toAlgHom R A Aₛ) (span R (Set.range ↑b))
[PROOFSTEP]
rw [Submodule.map_span]
[GOAL]
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₛ
inst✝⁸ : Algebra R Rₛ
S : Submonoid R
hT : IsLocalization S Rₛ
A : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
Aₛ : Type u_4
inst✝⁵ : CommRing Aₛ
inst✝⁴ : Algebra A Aₛ
inst✝³ : Algebra Rₛ Aₛ
inst✝² : Algebra R Aₛ
inst✝¹ : IsScalarTower R Rₛ Aₛ
inst✝ : IsScalarTower R A Aₛ
hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
ι : Type u_5
b : Basis ι R A
⊢ map (IsScalarTower.toAlgHom R A Aₛ) (span R (Set.range ↑b)) = LinearMap.range (IsScalarTower.toAlgHom R A Aₛ)
[PROOFSTEP]
rw [b.span_eq, Submodule.map_top]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
⊢ ∀ (r : A) (x : M),
    AddHom.toFun { toFun := ↑f, map_add' := (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) } (r • x) =
      ↑(RingHom.id A) r • AddHom.toFun { toFun := ↑f, map_add' := (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) } x
[PROOFSTEP]
intro r m
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
r : A
m : M
⊢ AddHom.toFun { toFun := ↑f, map_add' := (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) } (r • m) =
    ↑(RingHom.id A) r • AddHom.toFun { toFun := ↑f, map_add' := (_ : ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y) } m
[PROOFSTEP]
simp only [RingHom.id_apply]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
r : A
m : M
⊢ ↑f (r • m) = r • ↑f m
[PROOFSTEP]
rcases mk'_surjective S r with ⟨r, s, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ ↑f (mk' A r s • m) = mk' A r s • ↑f m
[PROOFSTEP]
calc
  f (mk' A r s • m) = ((s : R) • mk' A 1 s) • f (mk' A r s • m) := by simp
  _ = (mk' A 1 s) • (s : R) • f (mk' A r s • m) := by rw [smul_comm, smul_assoc]
  _ = (mk' A 1 s) • f ((s : R) • mk' A r s • m) := by simp
  _ = (mk' A 1 s) • f (r • m) := by rw [← smul_assoc, smul_mk'_self, algebraMap_smul]
  _ = (mk' A 1 s) • r • f m := by simp
  _ = mk' A r s • f m := by rw [smul_comm, ← smul_assoc, smul_mk'_one]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ ↑f (mk' A r s • m) = (↑s • mk' A 1 s) • ↑f (mk' A r s • m)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ (↑s • mk' A 1 s) • ↑f (mk' A r s • m) = mk' A 1 s • ↑s • ↑f (mk' A r s • m)
[PROOFSTEP]
rw [smul_comm, smul_assoc]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ mk' A 1 s • ↑s • ↑f (mk' A r s • m) = mk' A 1 s • ↑f (↑s • mk' A r s • m)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ mk' A 1 s • ↑f (↑s • mk' A r s • m) = mk' A 1 s • ↑f (r • m)
[PROOFSTEP]
rw [← smul_assoc, smul_mk'_self, algebraMap_smul]
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ mk' A 1 s • ↑f (r • m) = mk' A 1 s • r • ↑f m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹¹ : CommRing R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_3
N : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M →ₗ[R] N
m : M
r : R
s : { x // x ∈ S }
⊢ mk' A 1 s • r • ↑f m = mk' A r s • ↑f m
[PROOFSTEP]
rw [smul_comm, ← smul_assoc, smul_mk'_one]