R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
have : (Set.range fun i : Fin d => x ^ (i : ℕ)) = (fun i : ℕ => x ^ i) '' ↑(Finset.range d) := by
  ext n
  simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
  exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ (∃ l, (∀ (x : ℕ), d ≤ x → ↑l x = 0) ∧ (Finset.sum l.support fun x_1 => ↑(algebraMap R S) (↑l x_1) * x ^ x_1) = y) ↔
    ∃ q, (∀ (m : ℕ), d ≤ m → ↑q m = 0) ∧ y = Finset.sum q.support fun x_1 => ↑(algebraMap R S) (↑q x_1) * x ^ x_1
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
simp only [this, Finsupp.mem_span_image_iff_total, degree_lt_iff_coeff_zero,
  exists_iff_exists_finsupp, coeff, aeval, eval₂RingHom', eval₂_eq_sum, Polynomial.sum, support,
  Finsupp.mem_supported', Finsupp.total, Finsupp.sum, Algebra.smul_def, eval₂_zero, exists_prop,
  LinearMap.id_coe, eval₂_one, id.def, not_lt, Finsupp.coe_lsum, LinearMap.coe_smulRight,
  Finset.mem_range, AlgHom.coe_mks, Finset.mem_coe]
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ (∃ l, (∀ (x : ℕ), d ≤ x → ↑l x = 0) ∧ (Finset.sum l.support fun x_1 => ↑(algebraMap R S) (↑l x_1) * x ^ x_1) = y) ↔
    ∃ q, (∀ (m : ℕ), d ≤ m → ↑q m = 0) ∧ (Finset.sum q.support fun x_1 => ↑(algebraMap R S) (↑q x_1) * x ^ x_1) = y
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ (∃ l, (∀ (x : ℕ), d ≤ x → ↑l x = 0) ∧ (Finset.sum l.support fun x_1 => ↑(algebraMap R S) (↑l x_1) * x ^ x_1) = y) ↔
    ∃ q, (∀ (m : ℕ), d ≤ m → ↑q m = 0) ∧ y = Finset.sum q.support fun x_1 => ↑(algebraMap R S) (↑q x_1) * x ^ x_1
simp_rw [@eq_comm _ y]
no goals
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
this : (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
⊢ (∃ l, (∀ (x : ℕ), d ≤ x → ↑l x = 0) ∧ (Finset.sum l.support fun x_1 => ↑(algebraMap R S) (↑l x_1) * x ^ x_1) = y) ↔
    ∃ q, (∀ (m : ℕ), d ≤ m → ↑q m = 0) ∧ (Finset.sum q.support fun x_1 => ↑(algebraMap R S) (↑q x_1) * x ^ x_1) = y
exact Iff.rfl
case h
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
n : S
⊢ (n ∈ Set.range fun i => x ^ ↑i) ↔ n ∈ (fun i => x ^ i) '' ↑(Finset.range d)
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
⊢ (Set.range fun i => x ^ ↑i) = (fun i => x ^ i) '' ↑(Finset.range d)
ext n
case h
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ ∃ x_1, x_1 < d ∧ x ^ x_1 = n
case h
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
n : S
⊢ (n ∈ Set.range fun i => x ^ ↑i) ↔ n ∈ (fun i => x ^ i) '' ↑(Finset.range d)
simp_rw [Set.mem_range, Set.mem_image, Finset.mem_coe, Finset.mem_range]
no goals
case h
R : Type u_2
S : Type u_1
T : Type ?u.12701
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.13004
B : Type ?u.13007
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.13429
inst✝ : Field K
x y : S
d : ℕ
n : S
⊢ (∃ y, x ^ ↑y = n) ↔ ∃ x_1, x_1 < d ∧ x ^ x_1 = n
exact ⟨fun ⟨⟨i, hi⟩, hy⟩ => ⟨i, hi, hy⟩, fun ⟨i, hi, hy⟩ => ⟨⟨i, hi⟩, hy⟩⟩