-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_coe_eq_self {n} {f : R[X]} (hn : natDegree f < n) : trunc n (f : R⟦X⟧) = f

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ ↑(trunc n ↑f) = ↑f

Tactic:
ext m

Result:
case h
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ (coeff R m) ↑(trunc n ↑f) = (coeff R m) ↑f

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = f.coeff m

Tactic:
symm

Result:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ f.coeff m = 0

Proof state:
case h
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ (coeff R m) ↑(trunc n ↑f) = (coeff R m) ↑f

Tactic:
rw [coeff_coe, coeff_trunc]

Result:
case h
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ (if m < n then (coeff R m) ↑f else 0) = (coeff R m) ↑f

Proof state:
case h
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ (if m < n then (coeff R m) ↑f else 0) = (coeff R m) ↑f

Tactic:
split

Result:
case h.isTrue
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h✝ : m < n
⊢ (coeff R m) ↑f = (coeff R m) ↑f

case h.isFalse
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h✝ : ¬m < n
⊢ 0 = (coeff R m) ↑f

Proof state:
case h.isFalse
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h✝ : ¬m < n
⊢ 0 = (coeff R m) ↑f

Tactic:
case isFalse h =>
  rw [not_lt] at h
  rw [coeff_coe]; symm
  exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = (coeff R m) ↑f

Tactic:
rw [coeff_coe]

Result:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = f.coeff m

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ f.coeff m = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h

Result:
no goals

Proof state:
case h.isTrue
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h✝ : m < n
⊢ (coeff R m) ↑f = (coeff R m) ↑f

case h.isFalse
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h✝ : ¬m < n
⊢ 0 = (coeff R m) ↑f

Tactic:
case isTrue h => rfl

Result:
case h.isFalse
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h✝ : ¬m < n
⊢ 0 = (coeff R m) ↑f

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : m < n
⊢ (coeff R m) ↑f = (coeff R m) ↑f

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : ¬m < n
⊢ 0 = (coeff R m) ↑f

Tactic:
rw [not_lt] at h

Result:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = (coeff R m) ↑f

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ trunc n ↑f = f

Tactic:
rw [← Polynomial.coe_inj]

Result:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ ↑(trunc n ↑f) = ↑f