-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_coeff_coeff (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) :
    coeff m (Polynomial.coeff (finSuccEquiv R n f) i) = coeff (m.cons i) f

Proof state:
case h1.e_a.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0

Tactic:
simp only [hjmi, if_false]

Result:
case h1.e_a.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = 0

Proof state:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x : Fin n, X x ^ j x.succ)).coeff i) =
    if j = cons i m then r else 0

Tactic:
rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]

Result:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = r * if j = cons i m then 1 else 0

Proof state:
case h1.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ coeff m (if j 0 = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = 0

Tactic:
simp only [eq_self_iff_true, if_true]

Result:
case h1.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ coeff m (∏ x : Fin n, X x ^ j x.succ) = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (j 0) j.tail
⊢ False

Tactic:
rw [cons_tail] at hjmi

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False

Proof state:
case h1.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ coeff m (∏ x : Fin n, X x ^ j x.succ) = 0

Tactic:
have hmj : m ≠ j.tail := by
  rintro rfl
  rw [cons_tail] at hjmi
  contradiction

Result:
case h1.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
hmj : m ≠ j.tail
⊢ coeff m (∏ x : Fin n, X x ^ j x.succ) = 0

Proof state:
case h1.e_a.inl
R : Type u
inst✝ : CommSemiring R
n : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = (cons i m) 0 then ∏ x : Fin n, X x ^ (cons i m) x.succ else 0) = if cons i m = cons i m then 1 else 0

Tactic:
simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul, Finsupp.prod_pow] using
  coeff_monomial m m (1 : R)

Result:
no goals

Proof state:
case h1.e_a.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = 0

Tactic:
obtain hij | rfl := ne_or_eq i (j 0)

Result:
case h1.e_a.inr.inl
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
hij : i ≠ j 0
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = 0

case h1.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ coeff m (if j 0 = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = 0

Proof state:
case h1.e_a.inr.inl
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
hij : i ≠ j 0
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = 0

Tactic:
simp only [hij, if_false, coeff_zero]

Result:
no goals

Proof state:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = r * if j = cons i m then 1 else 0

Tactic:
congr 1

Result:
case h1.e_a
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0

Proof state:
case h1.e_a.inr.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
hmj : m ≠ j.tail
⊢ coeff m (∏ x : Fin n, X x ^ j x.succ) = 0

Tactic:
simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using
  coeff_monomial m j.tail (1 : R)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ coeff m (((finSuccEquiv R n) f).coeff i) = coeff (cons i m) f

Tactic:
induction' f using MvPolynomial.induction_on' with j r p q hp hq generalizing i m

Result:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)

case h2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) p).coeff i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) q).coeff i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) (p + q)).coeff i) = coeff (cons i m) (p + q)

Proof state:
case h1.e_a
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0

Tactic:
obtain rfl | hjmi := eq_or_ne j (m.cons i)

Result:
case h1.e_a.inl
R : Type u
inst✝ : CommSemiring R
n : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = (cons i m) 0 then ∏ x : Fin n, X x ^ (cons i m) x.succ else 0) = if cons i m = cons i m then 1 else 0

case h1.e_a.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case h2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) p).coeff i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) q).coeff i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) (p + q)).coeff i) = coeff (cons i m) (p + q)

Tactic:
simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]

Result:
no goals

Proof state:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)

case h2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) p).coeff i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) q).coeff i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) (p + q)).coeff i) = coeff (cons i m) (p + q)

Tactic:
swap

Result:
case h2
R : Type u
inst✝ : CommSemiring R
n : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) p).coeff i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (((finSuccEquiv R n) q).coeff i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) (p + q)).coeff i) = coeff (cons i m) (p + q)

case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)