-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc_C (n : σ →₀ ℕ) (hnn : n ≠ 0) (a : R) : trunc R n (C σ R a) = MvPolynomial.C a :=
  MvPolynomial.ext _ _ fun m ↦ by
    classical
    rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C]
    split_ifs with H <;> first |rfl|try simp_all only [ne_eq, not_true_eq_false]
    exfalso; apply H; subst m; exact Ne.bot_lt hnn

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
hnn : ¬n = 0
H : ¬0 < n
⊢ 0 < n

Tactic:
exact Ne.bot_lt hnn

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)

Tactic:
rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ (if m < n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ (if m < n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0

Tactic:
split_ifs with H <;> first |rfl|try simp_all only [ne_eq, not_true_eq_false]

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a

Tactic:
simp_all only [ne_eq, not_true_eq_false]

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ False

Tactic:
apply H

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ m < n

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ m < n

Tactic:
subst m

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
hnn : ¬n = 0
H : ¬0 < n
⊢ 0 < n

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a

Tactic:
try simp_all only [ne_eq, not_true_eq_false]

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)

Tactic:
classical
rw [coeff_trunc, coeff_C, MvPolynomial.coeff_C]
split_ifs with H <;> first |rfl|try simp_all only [ne_eq, not_true_eq_false]
exfalso; apply H; subst m; exact Ne.bot_lt hnn

Result:
no goals

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ 0 = a

Tactic:
exfalso

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
hnn : ¬n = m
H : ¬m < n
h✝ : 0 = m
⊢ False

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
a : R
m : σ →₀ ℕ
H : ¬m < n
h✝ : ¬0 = m
⊢ 0 = 0

Tactic:
rfl

Result:
no goals