-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem eval₂_trunc_eq_sum_range {S : Type*} [Semiring S] (s : S) (G : R →+* S) (n) (f : R⟦X⟧) :
    (trunc n f).eval₂ G s = ∑ i ∈ range n, G (coeff R i f) * s ^ i

Proof state:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
x✝ : ℕ
h : x✝ ∈ range (n + 1)
⊢ G ((trunc (n + 1) f).coeff x✝) * s ^ x✝ = G ((coeff R x✝) f) * s ^ x✝

Tactic:
rw [mem_range] at h

Result:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
x✝ : ℕ
h : x✝ < n + 1
⊢ G ((trunc (n + 1) f).coeff x✝) * s ^ x✝ = G ((coeff R x✝) f) * s ^ x✝

Proof state:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
⊢ eval₂ G s (trunc (n + 1) f) = ∑ i ∈ range (n + 1), G ((coeff R i) f) * s ^ i

Tactic:
have := natDegree_trunc_lt f n

Result:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
⊢ eval₂ G s (trunc (n + 1) f) = ∑ i ∈ range (n + 1), G ((coeff R i) f) * s ^ i

Proof state:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
n : ℕ
f : R⟦X⟧
⊢ eval₂ G s (trunc n f) = ∑ i ∈ range n, G ((coeff R i) f) * s ^ i

Tactic:
cases n with
| zero =>
  rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
| succ n =>
  have := natDegree_trunc_lt f n
  rw [eval₂_eq_sum_range' (hn := this)]
  apply sum_congr rfl
  intro _ h
  rw [mem_range] at h
  congr
  rw [coeff_trunc, if_pos h]

Result:
no goals

Proof state:
case succ.e_a.h.e_6.h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
x✝ : ℕ
h : x✝ < n + 1
⊢ (trunc (n + 1) f).coeff x✝ = (coeff R x✝) f

Tactic:
rw [coeff_trunc, if_pos h]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
⊢ ∑ i ∈ range (n + 1), G ((trunc (n + 1) f).coeff i) * s ^ i = ∑ i ∈ range (n + 1), G ((coeff R i) f) * s ^ i

Tactic:
apply sum_congr rfl

Result:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
⊢ ∀ x ∈ range (n + 1), G ((trunc (n + 1) f).coeff x) * s ^ x = G ((coeff R x) f) * s ^ x

Proof state:
case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ eval₂ G s (trunc 0 f) = ∑ i ∈ range 0, G ((coeff R i) f) * s ^ i

Tactic:
rw [trunc_zero', range_zero, sum_empty, eval₂_zero]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
⊢ ∀ x ∈ range (n + 1), G ((trunc (n + 1) f).coeff x) * s ^ x = G ((coeff R x) f) * s ^ x

Tactic:
intro _ h

Result:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
x✝ : ℕ
h : x✝ ∈ range (n + 1)
⊢ G ((trunc (n + 1) f).coeff x✝) * s ^ x✝ = G ((coeff R x✝) f) * s ^ x✝

Proof state:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
x✝ : ℕ
h : x✝ < n + 1
⊢ G ((trunc (n + 1) f).coeff x✝) * s ^ x✝ = G ((coeff R x✝) f) * s ^ x✝

Tactic:
congr

Result:
case succ.e_a.h.e_6.h
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
x✝ : ℕ
h : x✝ < n + 1
⊢ (trunc (n + 1) f).coeff x✝ = (coeff R x✝) f

Proof state:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
⊢ eval₂ G s (trunc (n + 1) f) = ∑ i ∈ range (n + 1), G ((coeff R i) f) * s ^ i

Tactic:
rw [eval₂_eq_sum_range' (hn := this)]

Result:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : (trunc (n + 1) f).natDegree < n + 1
⊢ ∑ i ∈ range (n + 1), G ((trunc (n + 1) f).coeff i) * s ^ i = ∑ i ∈ range (n + 1), G ((coeff R i) f) * s ^ i