[GOAL]
⊢ StableUnderComposition fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
introv R hf hg
[GOAL]
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Surjective ↑f
hg : Function.Surjective ↑g
⊢ Function.Surjective ↑(comp g f)
[PROOFSTEP]
exact hg.comp hf
[GOAL]
⊢ RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
apply surjective_stableUnderComposition.respectsIso
[GOAL]
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective ↑(RingEquiv.toRingHom e)
[PROOFSTEP]
intros _ _ _ _ e
[GOAL]
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
e : R✝ ≃+* S✝
⊢ Function.Surjective ↑(RingEquiv.toRingHom e)
[PROOFSTEP]
exact e.surjective
[GOAL]
⊢ StableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
refine' StableUnderBaseChange.mk _ surjective_respectsIso _
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ↑(algebraMap R T) → Function.Surjective ↑includeLeftRingHom
[PROOFSTEP]
classical
introv h x
skip
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Function.Surjective ↑(algebraMap R T) → Function.Surjective ↑includeLeftRingHom
[PROOFSTEP]
introv h x
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, ↑includeLeftRingHom a = x
[PROOFSTEP]
skip
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, ↑includeLeftRingHom a = x
[PROOFSTEP]
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S ⊗[R] T
⊢ ∃ a, ↑includeLeftRingHom a = x
[PROOFSTEP]
induction x using TensorProduct.induction_on with
| zero => exact ⟨0, map_zero _⟩
| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
case zero
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
⊢ ∃ a, ↑includeLeftRingHom a = 0
[PROOFSTEP]

| zero => exact ⟨0, map_zero _⟩
[GOAL]
case zero
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
⊢ ∃ a, ↑includeLeftRingHom a = 0
[PROOFSTEP]
exact ⟨0, map_zero _⟩
[GOAL]
case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : T
⊢ ∃ a, ↑includeLeftRingHom a = x ⊗ₜ[R] y
[PROOFSTEP]

| tmul x y =>
  obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
  rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
[GOAL]
case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : T
⊢ ∃ a, ↑includeLeftRingHom a = x ⊗ₜ[R] y
[PROOFSTEP]
obtain ⟨y, rfl⟩ := h y
[GOAL]
case tmul.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : R
⊢ ∃ a, ↑includeLeftRingHom a = x ⊗ₜ[R] ↑(algebraMap R T) y
[PROOFSTEP]
use y • x
[GOAL]
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : R
⊢ ↑includeLeftRingHom (y • x) = x ⊗ₜ[R] ↑(algebraMap R T) y
[PROOFSTEP]
dsimp
[GOAL]
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x : S
y : R
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] ↑(algebraMap R T) y
[PROOFSTEP]
rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
[GOAL]
case add
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x y : S ⊗[R] T
ex : ∃ a, ↑includeLeftRingHom a = x
ey : ∃ a, ↑includeLeftRingHom a = y
⊢ ∃ a, ↑includeLeftRingHom a = x + y
[PROOFSTEP]

| add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
[GOAL]
case add
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x y : S ⊗[R] T
ex : ∃ a, ↑includeLeftRingHom a = x
ey : ∃ a, ↑includeLeftRingHom a = y
⊢ ∃ a, ↑includeLeftRingHom a = x + y
[PROOFSTEP]
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey
[GOAL]
case add.intro.intro
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ↑(algebraMap R T)
x y : S
⊢ ∃ a, ↑includeLeftRingHom a = ↑includeLeftRingHom x + ↑includeLeftRingHom y
[PROOFSTEP]
exact ⟨x + y, map_add _ x y⟩
[GOAL]
⊢ OfLocalizationSpan fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f
[PROOFSTEP]
introv R hs H
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
⊢ Function.Surjective ↑f
[PROOFSTEP]
skip
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
⊢ Function.Surjective ↑f
[PROOFSTEP]
letI := f.toAlgebra
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
⊢ Function.Surjective ↑f
[PROOFSTEP]
show Function.Surjective (Algebra.ofId R S)
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
⊢ Function.Surjective ↑(Algebra.ofId R S)
[PROOFSTEP]
rw [← Algebra.range_top_iff_surjective, eq_top_iff]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
⊢ ⊤ ≤ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
rintro x -
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
⊢ x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_total R s 1).mp (show _ ∈ Ideal.span s by rw [hs]; trivial)
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
⊢ 1 ∈ Ideal.span s
[PROOFSTEP]
rw [hs]
[GOAL]
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
⊢ 1 ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
case intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
fapply Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem _ l.support (fun x : s => f x) fun x : s => f (l x)
[GOAL]
case intro.e
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∑ i in l.support, ↑f (↑l i) * ↑f ↑i = 1
[PROOFSTEP]
dsimp only
[GOAL]
case intro.e
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∑ i in l.support, ↑f (↑l i) * ↑f ↑i = 1
[PROOFSTEP]
simp_rw [← _root_.map_mul, ← map_sum, ← f.map_one]
[GOAL]
case intro.e
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ↑f (∑ x in l.support, ↑l x * ↑x) = ↑f 1
[PROOFSTEP]
exact f.congr_arg hl
[GOAL]
case intro.hs
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∀ (i : ↑s), ↑f ↑i ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
exact fun _ => Set.mem_range_self _
[GOAL]
case intro.hl
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∀ (i : ↑s), ↑f (↑l i) ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
exact fun _ => Set.mem_range_self _
[GOAL]
case intro.H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
⊢ ∀ (i : ↑s), ∃ n, ↑f ↑i ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
intro r
[GOAL]
case intro.H
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨y, hy⟩ := H r (IsLocalization.mk' _ x (1 : Submonoid.powers (f r)))
[GOAL]
case intro.H.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
y : Localization.Away ↑r
hy : ↑(Localization.awayMap f ↑r) y = IsLocalization.mk' (Localization.Away (↑f ↑r)) x 1
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨z, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective (Submonoid.powers (r : R)) y
[GOAL]
case intro.H.intro.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n : ℕ
hy :
  ↑(Localization.awayMap f ↑r)
      (IsLocalization.mk' (Localization.Away ↑r) z
        { val := (fun x x_1 => x ^ x_1) (↑r) n,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) }) =
    IsLocalization.mk' (Localization.Away (↑f ↑r)) x 1
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
erw [IsLocalization.map_mk', IsLocalization.eq] at hy 
[GOAL]
case intro.H.intro.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n : ℕ
hy :
  ∃ c,
    ↑c * (↑1 * ↑f z) =
      ↑c *
        (↑{
              val :=
                ↑f
                  ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                      property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) },
              property :=
                (_ :
                  ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                        property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) } ∈
                    Submonoid.comap f (Submonoid.powers (↑f ↑r))) } *
          x)
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
obtain ⟨⟨_, m, rfl⟩, hm⟩ := hy
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑1 * ↑f z) =
    ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑{
            val :=
              ↑f
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                    property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) },
            property :=
              (_ :
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                      property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) } ∈
                  Submonoid.comap f (Submonoid.powers (↑f ↑r))) } *
        x)
⊢ ∃ n, ↑f ↑r ^ n • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
refine' ⟨m + n, _⟩
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑1 * ↑f z) =
    ↑{ val := (fun x x_1 => x ^ x_1) (↑f ↑r) m,
          property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑f ↑r) y = (fun x x_1 => x ^ x_1) (↑f ↑r) m) } *
      (↑{
            val :=
              ↑f
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                    property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) },
            property :=
              (_ :
                ↑{ val := (fun x x_1 => x ^ x_1) (↑r) n,
                      property := (_ : ∃ y, (fun x x_1 => x ^ x_1) (↑r) y = (fun x x_1 => x ^ x_1) (↑r) n) } ∈
                  Submonoid.comap f (Submonoid.powers (↑f ↑r))) } *
        x)
⊢ ↑f ↑r ^ (m + n) • x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
dsimp at hm ⊢
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm : ↑f ↑r ^ m * (1 * ↑f z) = ↑f ↑r ^ m * (↑f (↑r ^ n) * x)
⊢ ↑f ↑r ^ (m + n) * x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
simp_rw [_root_.one_mul, ← _root_.mul_assoc, ← map_pow, ← f.map_mul, ← pow_add, map_pow] at hm 
[GOAL]
case intro.H.intro.intro.intro.mk.intro.intro.mk.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ↑f) (Localization.awayMap f ↑r)
this : Algebra R S := toAlgebra f
x : S
l : ↑s →₀ R
hl : ↑(Finsupp.total (↑s) R R Subtype.val) l = 1
r : ↑s
z : R
n m : ℕ
hm : ↑f (↑r ^ m * z) = ↑f ↑r ^ (m + n) * x
⊢ ↑f ↑r ^ (m + n) * x ∈ AlgHom.range (Algebra.ofId R S)
[PROOFSTEP]
exact ⟨_, hm⟩
