-- Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean
theorem spanCoeffs_ne_top : spanCoeffs k ≠ ⊤

Proof state:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv :
  (toSplittingField (Finset.image Prod.fst v.support))
      ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn => (subProdXSubC fn.1).coeff fn.2) v) =
    (toSplittingField (Finset.image Prod.fst v.support)) 1
⊢ False

Tactic:
rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv

Result:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : 0 = 1
⊢ False

case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
⊢ ∀ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 0

Proof state:
k : Type u
inst✝ : Field k
⊢ ¬∃ l ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ,
      (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn => (subProdXSubC fn.1).coeff fn.2) l = 1

Tactic:
rintro ⟨v, _, hv⟩

Result:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn => (subProdXSubC fn.1).coeff fn.2) v = 1
⊢ False

Proof state:
k : Type u
inst✝ : Field k
⊢ spanCoeffs k ≠ ⊤

Tactic:
rw [Ideal.ne_top_iff_one, spanCoeffs, Ideal.span, ← Set.image_univ,
  Finsupp.mem_span_image_iff_linearCombination]

Result:
k : Type u
inst✝ : Field k
⊢ ¬∃ l ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ,
      (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn => (subProdXSubC fn.1).coeff fn.2) l = 1

Proof state:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : (Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn => (subProdXSubC fn.1).coeff fn.2) v = 1
⊢ False

Tactic:
replace hv := congr_arg (toSplittingField <| v.support.image Prod.fst) hv

Result:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv :
  (toSplittingField (Finset.image Prod.fst v.support))
      ((Finsupp.linearCombination (MvPolynomial (Vars k) k) fun fn => (subProdXSubC fn.1).coeff fn.2) v) =
    (toSplittingField (Finset.image Prod.fst v.support)) 1
⊢ False

Proof state:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
⊢ ∀ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 0

Tactic:
intro j hj

Result:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
hj : j ∈ v.support
⊢ (toSplittingField (Finset.image Prod.fst v.support)) (v j • (subProdXSubC j.1).coeff j.2) = 0

Proof state:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : 0 = 1
⊢ False

Tactic:
exact zero_ne_one hv

Result:
no goals

Proof state:
case intro.intro
k : Type u
inst✝ : Field k
v : Monics k × ℕ →₀ MvPolynomial (Vars k) k
left✝ : v ∈ Finsupp.supported (MvPolynomial (Vars k) k) (MvPolynomial (Vars k) k) Set.univ
hv : ∑ x ∈ v.support, (toSplittingField (Finset.image Prod.fst v.support)) (v x • (subProdXSubC x.1).coeff x.2) = 1
j : Monics k × ℕ
hj : j ∈ v.support
⊢ (toSplittingField (Finset.image Prod.fst v.support)) (v j • (subProdXSubC j.1).coeff j.2) = 0

Tactic:
rw [smul_eq_mul, map_mul, toSplittingField_coeff (Finset.mem_image_of_mem _ hj), mul_zero]

Result:
no goals