R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ support (∑ i : Fin n, ↑C (x i) * X ^ k i) = image k univ
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ card (support (∑ i : Fin n, ↑C (x i) * X ^ k i)) = n
suffices (∑ i, C (x i) * X ^ k i).support = image k univ by
  rw [this, univ.card_image_of_injective hk, card_fin]
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ ∃ a_1, k a_1 = a
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ support (∑ i : Fin n, ↑C (x i) * X ^ k i) = image k univ
simp_rw [Finset.ext_iff, mem_support_iff, finset_sum_coeff, coeff_C_mul_X_pow, mem_image,
  mem_univ, true_and]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h : (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
⊢ ∃ a, k a = i

case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
⊢ (∃ a, k a = i) → (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) ≠ 0 ↔ ∃ a_1, k a_1 = a
refine' fun i => ⟨fun h => _, _⟩
no goals
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this : support (∑ i : Fin n, ↑C (x i) * X ^ k i) = image k univ
⊢ card (support (∑ i : Fin n, ↑C (x i) * X ^ k i)) = n
rw [this, univ.card_image_of_injective hk, card_fin]
case refine'_1.intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h✝ : (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
j : Fin n
left✝ : j ∈ univ
h : (if i = k j then x j else 0) ≠ 0
⊢ ∃ a, k a = i
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h : (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
⊢ ∃ a, k a = i
obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h
no goals
case refine'_1.intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h✝ : (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
j : Fin n
left✝ : j ∈ univ
h : (if i = k j then x j else 0) ≠ 0
⊢ ∃ a, k a = i
exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ (∑ x_1 : Fin n, if k j = k x_1 then x x_1 else 0) ≠ 0
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
⊢ (∃ a, k a = i) → (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) ≠ 0
rintro ⟨j, _, rfl⟩
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0

case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ (b : Fin n), b ∈ univ → b ≠ j → (if k j = k b then x b else 0) = 0
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ (∑ x_1 : Fin n, if k j = k x_1 then x x_1 else 0) ≠ 0
rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]
no goals
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0
exact hx j
no goals
case refine'_2.intro.refl
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ (b : Fin n), b ∈ univ → b ≠ j → (if k j = k b then x b else 0) = 0
exact fun m _ hmj => if_neg fun h => hmj.symm (hk h)