Theorem: MvPowerSeries.trunc_one' (DividedPowers/ForMathlib/RingTheory/MvPowerSeries/Trunc.lean)

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) 1) = MvPolynomial.coeff m 1
Tactic:
rw [coeff_trunc', coeff_one]
State after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then 1 else 0 else 0) = MvPolynomial.coeff m 1
Tactic:
split_ifs with H H'
State after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n 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✝ n 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✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ 0 = MvPolynomial.coeff m 1

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : m = 0
⊢ 1 = MvPolynomial.coeff m 1
Tactic:
subst m
State after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : 0 ≤ n
⊢ 1 = MvPolynomial.coeff 0 1

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : 0 ≤ n
⊢ 1 = MvPolynomial.coeff 0 1
Tactic:
simp
State after:
no goals

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ 0 = MvPolynomial.coeff m 1
Tactic:
symm
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ MvPolynomial.coeff m 1 = 0
Tactic:
rw [MvPolynomial.coeff_one]
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : m ≤ n
H' : ¬m = 0
⊢ (if 0 = m then 1 else 0) = 0
Tactic:
exact if_neg (Ne.symm H')
State after:
no goals

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ 0 = MvPolynomial.coeff m 1
Tactic:
symm
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ MvPolynomial.coeff m 1 = 0

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ MvPolynomial.coeff m 1 = 0
Tactic:
rw [MvPolynomial.coeff_one]
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ (if 0 = m then 1 else 0) = 0

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ (if 0 = m then 1 else 0) = 0
Tactic:
refine' if_neg _
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ ¬0 = m

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n m : σ →₀ ℕ
H : ¬m ≤ n
⊢ ¬0 = m
Tactic:
rintro rfl
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ False

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ False
Tactic:
apply H
State after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ 0 ≤ n

State before:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
H : ¬0 ≤ n
⊢ 0 ≤ n
Tactic:
exact orderBot.proof_1 n
State after:
no goals