-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc_one (n : σ →₀ ℕ) (hnn : n ≠ 0) : trunc R n 1 = 1 :=
  MvPolynomial.ext _ _ fun m ↦ by
    classical
    rw [coeff_trunc, coeff_one]
    split_ifs with H H'
    · subst m
      simp
    · symm
      rw [MvPolynomial.coeff_one]
      exact if_neg (Ne.symm H')
    · symm
      rw [MvPolynomial.coeff_one]
      refine if_neg ?_
      rintro rfl
      apply H
      exact Ne.bot_lt hnn

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

Tactic:
rintro rfl

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
H : ¬0 < n
⊢ False

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
H : 0 < n
⊢ 1 = MvPolynomial.coeff 0 1

Tactic:
simp

Result:
no goals

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

Tactic:
rw [MvPolynomial.coeff_one]

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

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1

Tactic:
subst m

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
H : 0 < n
⊢ 1 = MvPolynomial.coeff 0 1

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1

Tactic:
symm

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0

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

Tactic:
exact Ne.bot_lt hnn

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0

Tactic:
rw [MvPolynomial.coeff_one]

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0

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

Tactic:
refine if_neg ?_

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

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

Tactic:
rw [coeff_trunc, coeff_one]

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

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

Tactic:
apply H

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

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

Tactic:
symm

Result:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ MvPolynomial.coeff m 1 = 0

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

Tactic:
split_ifs with H H'

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : ¬m < n
⊢ 0 = MvPolynomial.coeff m 1

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
hnn : n ≠ 0
m : σ →₀ ℕ
H : m < n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0

Tactic:
exact if_neg (Ne.symm H')

Result:
no goals