Indicator eq 1 of neg empty empty of pos nonempty

lemma indicator_eq_1_of_neg_empty_empty_of_pos_nonempty  {pos : Finset F}  (h_pos : pos.Nonempty) :  indicator pos ∅ = 1 := by  unfold indicator  rw [Finset.nonempty_iff_ne_empty] at h_pos  apply Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq (pos ∪ ∅) _ _  · apply lt_of_le_of_lt (Polynomial.degree_sub_le _ _) (max_lt _ _)    · convert Lagrange.degree_interpolate_lt _ _      aesop    · simpa using Finset.card_pos.mpr (Finset.nonempty_of_ne_empty h_pos)  · have {x} {y} (hy : y ∈ pos.erase x) :      (x - y)⁻¹ * (x - y) = 1 :=        inv_mul_cancel₀ (sub_ne_zero_of_ne (by aesop))    aesop      (add simp        [Polynomial.eval_prod,          Finset.prod_eq_zero_iff,          Lagrange.basis,          Lagrange.basisDivisor,          Finset.prod_eq_one])      (add safe [(by rw        [Polynomial.eval_finsetSum,        Finset.sum_eq_single x])])