case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)

case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) f) i) = coeff (cons i m) f
induction' f using MvPolynomial.induction_on' with j r p q hp hq generalizing i m
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)

case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)

case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
swap
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (Polynomial.coeff (Polynomial.X ^ ↑j 0 * ↑Polynomial.C (∏ x : Fin n, X x ^ ↑j (Fin.succ x))) i) =
    if j = cons i m then r else 0
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)
simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, prod_pow,
  Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
  Fin.cases_succ, ← map_prod, ← RingHom.map_pow, Function.comp_apply]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = r * if j = cons i m then 1 else 0
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (Polynomial.coeff (Polynomial.X ^ ↑j 0 * ↑Polynomial.C (∏ x : Fin n, X x ^ ↑j (Fin.succ x))) i) =
    if j = cons i m then r else 0
rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]
case h1.e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = if j = cons i m then 1 else 0
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = r * if j = cons i m then 1 else 0
congr 1
case h1.e_a.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑(cons i m) 0 then ∏ x : Fin n, X x ^ ↑(cons i m) (Fin.succ x) else 0) =
    if cons i m = cons i m then 1 else 0

case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
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 (Fin.succ x) else 0) = if j = cons i m then 1 else 0
case h1.e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = if j = cons i m then 1 else 0
obtain rfl | hjmi := eq_or_ne j (m.cons i)
no goals
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
simp only [(finSuccEquiv R n).map_add, Polynomial.coeff_add, coeff_add, hp, hq]
no goals
case h1.e_a.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑(cons i m) 0 then ∏ x : Fin n, X x ^ ↑(cons i m) (Fin.succ x) else 0) =
    if cons i m = cons i m then 1 else 0
simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul, prod_pow] using
  coeff_monomial m m (1 : R)
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
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 (Fin.succ x) else 0) = 0
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
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 (Fin.succ x) else 0) = if j = cons i m then 1 else 0
simp only [hjmi, if_false]
case h1.e_a.inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
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 (Fin.succ x) else 0) = 0

case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
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 (Fin.succ x) else 0) = 0
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
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 (Fin.succ x) else 0) = 0
obtain hij | rfl := ne_or_eq i (j 0)
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
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 (Fin.succ x) else 0) = 0
simp only [eq_self_iff_true, if_true]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
hmj : m ≠ tail j
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
have hmj : m ≠ j.tail := by
  rintro rfl
  rw [cons_tail] at hjmi
  contradiction
no goals
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
hmj : m ≠ tail j
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
simpa only [monomial_eq, C_1, one_mul, prod_pow, Finsupp.tail_apply, if_neg hmj.symm] using
  coeff_monomial m j.tail (1 : R)
no goals
case h1.e_a.inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
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 (Fin.succ x) else 0) = 0
simp only [hij, if_false, coeff_zero]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (↑j 0) (tail j)
⊢ False
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ m ≠ tail j
rintro rfl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (↑j 0) (tail j)
⊢ False
rw [cons_tail] at hjmi
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1032018
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
contradiction