-- Mathlib/Algebra/Polynomial/Eval/Subring.lean
theorem mem_map_rangeS {p : S[X]} : p ∈ (mapRingHom f).rangeS ↔ ∀ n, p.coeff n ∈ f.rangeS

Proof state:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ f.rangeS) → p ∈ (mapRingHom f).rangeS

Tactic:
intro h

Result:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ p ∈ (mapRingHom f).rangeS

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ (mapRingHom f) (C c * X ^ i) = C (p.coeff i) * X ^ i

Tactic:
rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]

Result:
no goals

Proof state:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
⊢ C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS

Tactic:
rcases h i with ⟨c, hc⟩

Result:
case mpr.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS

Proof state:
case mp.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ f (p.coeff n) ∈ f.rangeS

Tactic:
exact Set.mem_range_self _

Result:
no goals

Proof state:
case mp.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ ((mapRingHom f) p).coeff n ∈ f.rangeS

Tactic:
rw [coe_mapRingHom, coeff_map]

Result:
case mp.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ f (p.coeff n) ∈ f.rangeS

Proof state:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∀ c ∈ Finset.range (p.natDegree + 1), C (p.coeff c) * X ^ c ∈ (mapRingHom f).rangeS

Tactic:
intro i _hi

Result:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
⊢ C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS

Proof state:
case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).rangeS → ∀ (n : ℕ), p.coeff n ∈ f.rangeS

Tactic:
rintro ⟨p, rfl⟩ n

Result:
case mp.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ ((mapRingHom f) p).coeff n ∈ f.rangeS

Proof state:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∑ i ∈ Finset.range (p.natDegree + 1), C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS

Tactic:
refine (mapRingHom f).rangeS.sum_mem ?_

Result:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∀ c ∈ Finset.range (p.natDegree + 1), C (p.coeff c) * X ^ c ∈ (mapRingHom f).rangeS

Proof state:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ p ∈ (mapRingHom f).rangeS

Tactic:
rw [p.as_sum_range_C_mul_X_pow]

Result:
case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∑ i ∈ Finset.range (p.natDegree + 1), C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS

Proof state:
case mpr.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ C (p.coeff i) * X ^ i ∈ (mapRingHom f).rangeS

Tactic:
use C c * X ^ i

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ (mapRingHom f) (C c * X ^ i) = C (p.coeff i) * X ^ i

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS

Tactic:
constructor

Result:
case mp
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).rangeS → ∀ (n : ℕ), p.coeff n ∈ f.rangeS

case mpr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ f.rangeS) → p ∈ (mapRingHom f).rangeS