-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_eq' {n : ℕ} (k : Fin n → ℕ) (x : Fin n → R) (hk : Function.Injective k)
    (hx : ∀ i, x i ≠ 0) : #(∑ i, C (x i) * X ^ k i).support = n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ (∑ i : Fin n, C (x i) * X ^ k i).support = image k univ

Tactic:
simp_rw [Finset.ext_iff, mem_support_iff, finset_sum_coeff, coeff_C_mul_X_pow, mem_image,
  mem_univ, true_and]

Result:
R : Type u_1
inst✝ : Semiring R
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

Proof state:
case refine_1.intro.intro
R : Type u_1
inst✝ : Semiring R
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

Tactic:
exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩

Result:
no goals

Proof state:
case refine_2.intro.refl
R : Type u_1
inst✝ : Semiring R
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

Tactic:
rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]

Result:
case refine_2.intro.refl
R : Type u_1
inst✝ : Semiring R
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
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ b ∈ univ, b ≠ j → (if k j = k b then x b else 0) = 0

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
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

Tactic:
obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h

Result:
case refine_1.intro.intro
R : Type u_1
inst✝ : Semiring R
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

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this : (∑ i : Fin n, C (x i) * X ^ k i).support = image k univ
⊢ #(∑ i : Fin n, C (x i) * X ^ k i).support = n

Tactic:
rw [this, univ.card_image_of_injective hk, card_fin]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
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

Tactic:
refine fun i => ⟨fun h => ?_, ?_⟩

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
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
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

Proof state:
case refine_2.intro.refl
R : Type u_1
inst✝ : Semiring R
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

Tactic:
exact hx j

Result:
no goals

Proof state:
case refine_2.intro.refl
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ b ∈ univ, b ≠ j → (if k j = k b then x b else 0) = 0

Tactic:
exact fun m _ hmj => if_neg fun h => hmj.symm (hk h)

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
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

Tactic:
rintro ⟨j, _, rfl⟩

Result:
case refine_2.intro.refl
R : Type u_1
inst✝ : Semiring R
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

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ #(∑ i : Fin n, C (x i) * X ^ k i).support = n

Tactic:
suffices (∑ i, C (x i) * X ^ k i).support = image k univ by
  rw [this, univ.card_image_of_injective hk, card_fin]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ (∑ i : Fin n, C (x i) * X ^ k i).support = image k univ