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

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
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
exfalso; apply H; subst m; exact orderBot.proof_1 n
State after:
no goals

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
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]
State after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0

State before:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
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
State after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ 0 = a

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ 0 = a
Tactic:
exfalso
State after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ False

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

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ m ≤ n
Tactic:
subst m
State after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
H : ¬0 ≤ n
⊢ 0 ≤ n

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

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

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : m ≤ n
h✝¹ : ¬m = 0
h✝ : 0 = m
⊢ 0 = a
Tactic:
try simp_all
State after:
no goals

State before:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n✝ n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : m ≤ n
h✝¹ : ¬m = 0
h✝ : 0 = m
⊢ 0 = a
Tactic:
simp_all
State after:
no goals