[STATEMENT]
lemma fund_sym_step_poly:
  shows   "finite A \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> decr p \<Longrightarrow> lead_monom (fund_sym_step_poly p) = lead_monom p"
    and   "finite A \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> decr p \<Longrightarrow> lead_coeff (fund_sym_step_poly p) = lead_coeff p"
    and   "finite A \<Longrightarrow> p \<noteq> 0 \<Longrightarrow> decr p \<Longrightarrow> fund_sym_step_poly p =
             fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (fund_sym_step_monom p) x)"
    and   "vars (fund_sym_step_poly p) \<subseteq> vars p \<union> A"
    and   "symmetric_mpoly A (fund_sym_step_poly p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p) &&& (\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p)) &&& (\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)) &&& vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A &&& symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
 5. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
define g where "g = (\<lambda>i. if i < n then lookup (lead_monom p) (f i) else 0)"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>i. if i < n then lookup (lead_monom p) (f i) else 0)

goal (5 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
 5. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
define q where "q = (\<Prod>i<n. sym_mpoly A (Suc i) ^ (g i - g (Suc i)) :: 'a mpoly)"
[PROOF STATE]
proof (state)
this:
q = (\<Prod>i<n. sym_mpoly A (Suc i) ^ (g i - g (Suc i)))

goal (5 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
 5. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
define c where "c = monom (restrictpm (-A) (lead_monom p)) (lead_coeff p)"
[PROOF STATE]
proof (state)
this:
c = MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p)

goal (5 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
 5. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
have [simp]: "fund_sym_step_poly p = c * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.fund_sym_step_poly p = c * q
[PROOF STEP]
by (simp add: fund_sym_step_poly_def fund_sym_step_coeff_def c_def q_def f_def g_def)
[PROOF STATE]
proof (state)
this:
local.fund_sym_step_poly p = c * q

goal (5 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
 5. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
have "vars (c * q) \<subseteq> vars p \<union> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (c * q) \<subseteq> vars p \<union> A
[PROOF STEP]
using keys_lead_monom_subset[of p]
          vars_monom_subset[of "restrictpm (-A) (lead_monom p)" "lead_coeff p"]
[PROOF STATE]
proof (prove)
using this:
keys (lead_monom p) \<subseteq> vars p
vars (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p)) \<subseteq> keys (restrictpm (- A) (lead_monom p))

goal (1 subgoal):
 1. vars (c * q) \<subseteq> vars p \<union> A
[PROOF STEP]
unfolding c_def q_def
[PROOF STATE]
proof (prove)
using this:
keys (lead_monom p) \<subseteq> vars p
vars (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p)) \<subseteq> keys (restrictpm (- A) (lead_monom p))

goal (1 subgoal):
 1. vars (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p) * (\<Prod>i<n. sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) \<subseteq> vars p \<union> A
[PROOF STEP]
by (intro order.trans[OF vars_mult] order.trans[OF vars_prod] order.trans[OF vars_power]
              Un_least UN_least order.trans[OF vars_sym_mpoly_subset]) auto
[PROOF STATE]
proof (state)
this:
vars (c * q) \<subseteq> vars p \<union> A

goal (5 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
 5. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
thus "vars (fund_sym_step_poly p) \<subseteq> vars p \<union> A"
[PROOF STATE]
proof (prove)
using this:
vars (c * q) \<subseteq> vars p \<union> A

goal (1 subgoal):
 1. vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A

goal (4 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
have "symmetric_mpoly A (c * q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (c * q)
[PROOF STEP]
unfolding c_def q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p) * (\<Prod>i<n. sym_mpoly A (Suc i) ^ (g i - g (Suc i))))
[PROOF STEP]
by (intro symmetric_mpoly_mult symmetric_mpoly_monom symmetric_mpoly_prod
              symmetric_mpoly_power symmetric_sym_mpoly) auto
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (c * q)

goal (4 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
 4. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
thus "symmetric_mpoly A (fund_sym_step_poly p)"
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A (c * q)

goal (1 subgoal):
 1. symmetric_mpoly A (local.fund_sym_step_poly p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (local.fund_sym_step_poly p)

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
assume finite: "finite A" and [simp]: "p \<noteq> 0" and "decr p"
[PROOF STATE]
proof (state)
this:
finite A
p \<noteq> 0
decr p

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "set xs = A" "distinct xs" and [simp]: "length xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs = A &&& distinct xs) &&& length xs = n
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (set xs = A &&& distinct xs) &&& length xs = n
[PROOF STEP]
by (auto simp: xs_def n_def)
[PROOF STATE]
proof (state)
this:
set xs = A
distinct xs
length xs = n

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have [simp]: "lead_coeff c = lead_coeff p" "lead_monom c = restrictpm (- A) (lead_monom p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff c = Symmetric_Polynomials.lead_coeff p &&& lead_monom c = restrictpm (- A) (lead_monom p)
[PROOF STEP]
by (simp_all add: c_def lead_monom_monom)
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff c = Symmetric_Polynomials.lead_coeff p
lead_monom c = restrictpm (- A) (lead_monom p)

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
hence f_range [simp]: "f i \<in> A" if "i < n" for i
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff c = Symmetric_Polynomials.lead_coeff p
lead_monom c = restrictpm (- A) (lead_monom p)

goal (1 subgoal):
 1. f i \<in> A
[PROOF STEP]
using that \<open>set xs = A\<close>
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff c = Symmetric_Polynomials.lead_coeff p
lead_monom c = restrictpm (- A) (lead_monom p)
i < n
set xs = A

goal (1 subgoal):
 1. f i \<in> A
[PROOF STEP]
by (auto simp: f_def set_conv_nth)
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> f ?i \<in> A

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "sorted xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted xs
[PROOF STEP]
by (simp add: xs_def)
[PROOF STATE]
proof (state)
this:
sorted xs

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
hence f_mono: "f i \<le> f j" if "i \<le> j" "j < n" for i j
[PROOF STATE]
proof (prove)
using this:
sorted xs

goal (1 subgoal):
 1. f i \<le> f j
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
sorted xs
i \<le> j
j < n

goal (1 subgoal):
 1. f i \<le> f j
[PROOF STEP]
by (auto simp: f_def n_def intro: sorted_nth_mono)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i \<le> ?j; ?j < n\<rbrakk> \<Longrightarrow> f ?i \<le> f ?j

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
hence g_mono: "g i \<ge> g j" if "i \<le> j" for i j
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<le> ?j; ?j < n\<rbrakk> \<Longrightarrow> f ?i \<le> f ?j

goal (1 subgoal):
 1. g j \<le> g i
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<le> ?j; ?j < n\<rbrakk> \<Longrightarrow> f ?i \<le> f ?j

goal (1 subgoal):
 1. (if j < n then lookup (lead_monom p) (f j) else 0) \<le> (if i < n then lookup (lead_monom p) (f i) else 0)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<le> ?j; ?j < n\<rbrakk> \<Longrightarrow> f ?i \<le> f ?j
i \<le> j

goal (1 subgoal):
 1. (if j < n then lookup (lead_monom p) (f j) else 0) \<le> (if i < n then lookup (lead_monom p) (f i) else 0)
[PROOF STEP]
using \<open>decr p\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<le> ?j; ?j < n\<rbrakk> \<Longrightarrow> f ?i \<le> f ?j
i \<le> j
decr p

goal (1 subgoal):
 1. (if j < n then lookup (lead_monom p) (f j) else 0) \<le> (if i < n then lookup (lead_monom p) (f i) else 0)
[PROOF STEP]
by (auto simp: decr_def)
[PROOF STATE]
proof (state)
this:
?i \<le> ?j \<Longrightarrow> g ?j \<le> g ?i

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have *: "(\<Prod>i<n. lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)) :: 'a mpoly)) =
              (\<Prod>i<card A. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<card A. (1::'a))
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<card A. (1::'a))
[PROOF STEP]
by (intro prod.cong) (auto simp: n_def lead_coeff_power)
[PROOF STATE]
proof (state)
this:
(\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<card A. (1::'a))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
hence "lead_coeff q = (\<Prod>i<n. lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)) :: 'a mpoly))"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<card A. (1::'a))

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff q = (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))
[PROOF STEP]
by (simp add: lead_coeff_prod lead_coeff_power n_def q_def)
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff q = (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff q = (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "\<dots> = (\<Prod>i<n. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<n. (1::'a))
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<n. (1::'a))
[PROOF STEP]
by (intro prod.cong) (auto simp: lead_coeff_power n_def)
[PROOF STATE]
proof (state)
this:
(\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<n. (1::'a))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Symmetric_Polynomials.lead_coeff q = (\<Prod>i<n. (1::'a))
[PROOF STEP]
have [simp]: "lead_coeff q = 1"
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff q = (\<Prod>i<n. (1::'a))

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff q = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff q = (1::'a)

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "lead_monom q = (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i)) :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom q = (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i<n. Symmetric_Polynomials.lead_coeff (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Prod>i<card A. (1::'a))

goal (1 subgoal):
 1. lead_monom q = (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))
[PROOF STEP]
by (simp add: q_def lead_monom_prod lead_coeff_power n_def)
[PROOF STATE]
proof (state)
this:
lead_monom q = (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom q = (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i))))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "\<dots> = (\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i) :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i)))
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i)))
[PROOF STEP]
by (intro sum.cong) (auto simp: lead_monom_power n_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i)))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. lead_monom (sym_mpoly A (Suc i) ^ (g i - g (Suc i)))) = (\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i)))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "\<dots> = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i))) = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))
[PROOF STEP]
proof (intro sum.cong refl, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> of_nat (g x - g (Suc x)) * lead_monom (sym_mpoly A (Suc x)) = of_nat (g x - g (Suc x)) * monom_of_set (set (take (Suc x) xs))
[PROOF STEP]
case (1 i)
[PROOF STATE]
proof (state)
this:
i \<in> {..<n}

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> of_nat (g x - g (Suc x)) * lead_monom (sym_mpoly A (Suc x)) = of_nat (g x - g (Suc x)) * monom_of_set (set (take (Suc x) xs))
[PROOF STEP]
have "lead_monom (sym_mpoly A (Suc i) :: 'a mpoly) =
            lead_monom (sym_mpoly (set xs) (Suc i) :: 'a mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sym_mpoly A (Suc i)) = lead_monom (sym_mpoly (set xs) (Suc i))
[PROOF STEP]
by (simp add: \<open>set xs = A\<close>)
[PROOF STATE]
proof (state)
this:
lead_monom (sym_mpoly A (Suc i)) = lead_monom (sym_mpoly (set xs) (Suc i))

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> of_nat (g x - g (Suc x)) * lead_monom (sym_mpoly A (Suc x)) = of_nat (g x - g (Suc x)) * monom_of_set (set (take (Suc x) xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom (sym_mpoly A (Suc i)) = lead_monom (sym_mpoly (set xs) (Suc i))

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> of_nat (g x - g (Suc x)) * lead_monom (sym_mpoly A (Suc x)) = of_nat (g x - g (Suc x)) * monom_of_set (set (take (Suc x) xs))
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
i \<in> {..<n}
[PROOF STEP]
have "\<dots> = monom_of_set (set (take (Suc i) xs))"
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<n}

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) (Suc i)) = monom_of_set (set (take (Suc i) xs))
[PROOF STEP]
by (subst lead_monom_sym_mpoly) (auto simp: xs_def n_def)
[PROOF STATE]
proof (state)
this:
lead_monom (sym_mpoly (set xs) (Suc i)) = monom_of_set (set (take (Suc i) xs))

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> of_nat (g x - g (Suc x)) * lead_monom (sym_mpoly A (Suc x)) = of_nat (g x - g (Suc x)) * monom_of_set (set (take (Suc x) xs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lead_monom (sym_mpoly A (Suc i)) = monom_of_set (set (take (Suc i) xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lead_monom (sym_mpoly A (Suc i)) = monom_of_set (set (take (Suc i) xs))

goal (1 subgoal):
 1. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i)) = of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i)) = of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. of_nat (g i - g (Suc i)) * lead_monom (sym_mpoly A (Suc i))) = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lead_monom q = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))
[PROOF STEP]
have lead_monom_q:
    "lead_monom q = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))"
[PROOF STATE]
proof (prove)
using this:
lead_monom q = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))

goal (1 subgoal):
 1. lead_monom q = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lead_monom q = (\<Sum>i<n. of_nat (g i - g (Suc i)) * monom_of_set (set (take (Suc i) xs)))

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "lead_monom (c * q) = lead_monom c + lead_monom q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (c * q) = lead_monom c + lead_monom q
[PROOF STEP]
by (simp add: lead_monom_mult)
[PROOF STATE]
proof (state)
this:
lead_monom (c * q) = lead_monom c + lead_monom q

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom (c * q) = lead_monom c + lead_monom q

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "\<dots> = lead_monom p" (is "?S = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom c + lead_monom q = lead_monom p
[PROOF STEP]
proof (intro poly_mapping_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (lead_monom c + lead_monom q) k = lookup (lead_monom p) k
[PROOF STEP]
fix i :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (lead_monom c + lead_monom q) k = lookup (lead_monom p) k
[PROOF STEP]
show "lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
proof (cases "i \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
 2. i \<notin> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> A

goal (2 subgoals):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
 2. i \<notin> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
hence "lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i +
               (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)"
        (is "_ = _ + ?S")
[PROOF STATE]
proof (prove)
using this:
i \<notin> A

goal (1 subgoal):
 1. lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i + (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)
[PROOF STEP]
by (simp add: lookup_add lead_monom_q lookup_sum)
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i + (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)

goal (2 subgoals):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
 2. i \<notin> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i + (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)

goal (2 subgoals):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
 2. i \<notin> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
i \<notin> A
[PROOF STEP]
have "?S = 0"
[PROOF STATE]
proof (prove)
using this:
i \<notin> A

goal (1 subgoal):
 1. (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i) = 0
[PROOF STEP]
by (intro sum.neutral) (auto simp: lookup_monom_of_set \<open>set xs = A\<close> dest!: in_set_takeD)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i) = 0

goal (2 subgoals):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
 2. i \<notin> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i + 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i + 0

goal (1 subgoal):
 1. lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> A

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
with \<open>set xs = A\<close>
[PROOF STATE]
proof (chain)
picking this:
set xs = A
i \<in> A
[PROOF STEP]
obtain m where m: "i = xs ! m" "m < n"
[PROOF STATE]
proof (prove)
using this:
set xs = A
i \<in> A

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i = xs ! m; m < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
i = xs ! m
m < n

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "lookup (lead_monom c + lead_monom q) i =
              (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lead_monom c + lead_monom q) i = (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i \<in> A

goal (1 subgoal):
 1. lookup (lead_monom c + lead_monom q) i = (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)
[PROOF STEP]
by (simp add: lookup_add lookup_sum lead_monom_q)
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i)

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "\<dots> = (\<Sum>j | j < n \<and> i \<in> set (take (Suc j) xs). g j - g (Suc j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i) = (\<Sum>j | j < n \<and> i \<in> set (take (Suc j) xs). g j - g (Suc j))
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i) = (\<Sum>j | j < n \<and> i \<in> set (take (Suc j) xs). g j - g (Suc j))

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. (g j - g (Suc j)) * lookup (monom_of_set (set (take (Suc j) xs))) i) = (\<Sum>j | j < n \<and> i \<in> set (take (Suc j) xs). g j - g (Suc j))

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "{j. j < n \<and> i \<in> set (take (Suc j) xs)} = {m..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {j. j < n \<and> i \<in> set (take (Suc j) xs)} = {m..<n}
[PROOF STEP]
using m \<open>distinct xs\<close>
[PROOF STATE]
proof (prove)
using this:
i = xs ! m
m < n
distinct xs

goal (1 subgoal):
 1. {j. j < n \<and> i \<in> set (take (Suc j) xs)} = {m..<n}
[PROOF STEP]
by (force simp: set_conv_nth nth_eq_iff_index_eq)
[PROOF STATE]
proof (state)
this:
{j. j < n \<and> i \<in> set (take (Suc j) xs)} = {m..<n}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{j. j < n \<and> i \<in> set (take (Suc j) xs)} = {m..<n}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "(\<Sum>j\<in>\<dots>. g j - g (Suc j)) = (\<Sum>j\<in>\<dots>. g j) - (\<Sum>j\<in>\<dots>. g (Suc j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = m..<n. g j - g (Suc j)) = sum g {m..<n} - (\<Sum>j = m..<n. g (Suc j))
[PROOF STEP]
by (subst sum_subtractf_nat) (auto intro!: g_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = m..<n. g j - g (Suc j)) = sum g {m..<n} - (\<Sum>j = m..<n. g (Suc j))

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = m..<n. g j - g (Suc j)) = sum g {m..<n} - (\<Sum>j = m..<n. g (Suc j))

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "(\<Sum>j\<in>{m..<n}. g (Suc j)) = (\<Sum>j\<in>{m<..n}. g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = m..<n. g (Suc j)) = sum g {m<..n}
[PROOF STEP]
by (intro sum.reindex_bij_witness[of _ "\<lambda>j. j - 1" Suc]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>j = m..<n. g (Suc j)) = sum g {m<..n}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = m..<n. g (Suc j)) = sum g {m<..n}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "\<dots> = (\<Sum>j\<in>{m<..<n}. g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g {m<..n} = sum g {m<..<n}
[PROOF STEP]
by (intro sum.mono_neutral_right) (auto simp: g_def)
[PROOF STATE]
proof (state)
this:
sum g {m<..n} = sum g {m<..<n}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum g {m<..n} = sum g {m<..<n}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "(\<Sum>j\<in>{m..<n}. g j) - \<dots> = (\<Sum>j\<in>{m..<n}-{m<..<n}. g j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g {m..<n} - sum g {m<..<n} = sum g ({m..<n} - {m<..<n})
[PROOF STEP]
by (intro sum_diff_nat [symmetric]) auto
[PROOF STATE]
proof (state)
this:
sum g {m..<n} - sum g {m<..<n} = sum g ({m..<n} - {m<..<n})

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum g {m..<n} - sum g {m<..<n} = sum g ({m..<n} - {m<..<n})

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "{m..<n}-{m<..<n} = {m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m..<n} - {m<..<n} = {m}
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
i = xs ! m
m < n

goal (1 subgoal):
 1. {m..<n} - {m<..<n} = {m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{m..<n} - {m<..<n} = {m}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{m..<n} - {m<..<n} = {m}

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
have "(\<Sum>j\<in>\<dots>. g j) = lookup (lead_monom p) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum g {m} = lookup (lead_monom p) i
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
i = xs ! m
m < n

goal (1 subgoal):
 1. sum g {m} = lookup (lead_monom p) i
[PROOF STEP]
by (auto simp: g_def not_less le_Suc_eq f_def)
[PROOF STATE]
proof (state)
this:
sum g {m} = lookup (lead_monom p) i

goal (1 subgoal):
 1. i \<in> A \<Longrightarrow> lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i

goal (1 subgoal):
 1. lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lookup (lead_monom c + lead_monom q) i = lookup (lead_monom p) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lead_monom c + lead_monom q = lead_monom p

goal (3 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 3. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lead_monom (c * q) = lead_monom p
[PROOF STEP]
show "lead_monom (fund_sym_step_poly p) = lead_monom p"
[PROOF STATE]
proof (prove)
using this:
lead_monom (c * q) = lead_monom p

goal (1 subgoal):
 1. lead_monom (local.fund_sym_step_poly p) = lead_monom p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lead_monom (local.fund_sym_step_poly p) = lead_monom p

goal (2 subgoals):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
 2. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
show "lead_coeff (fund_sym_step_poly p) = lead_coeff p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
[PROOF STEP]
by (simp add: lead_coeff_mult)
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have *: "lookup (fund_sym_step_monom p) k = (if k \<in> {1..n} then g (k - 1) - g k else 0)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (local.fund_sym_step_monom p) k = (if k \<in> {1..n} then g (k - 1) - g k else 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lookup (local.fund_sym_step_monom p) k = (if k \<in> {1..n} then g (k - 1) - g k else 0)
[PROOF STEP]
have "lookup (fund_sym_step_monom p) k =
            (\<Sum>x\<in>(if k \<in> {1..n} then {k - 1} else {}). g (k - 1) - g k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (local.fund_sym_step_monom p) k = (\<Sum>x\<in>(if k \<in> {1..n} then {k - 1} else {}). g (k - 1) - g k)
[PROOF STEP]
unfolding fund_sym_step_monom_def lookup_sum Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x<n. lookup (Poly_Mapping.single (Suc x) ((if x < n then lookup (lead_monom p) (f x) else 0) - (if Suc x < n then lookup (lead_monom p) (f (Suc x)) else 0))) k) = (\<Sum>x\<in>(if k \<in> {1..n} then {k - 1} else {}). g (k - 1) - g k)
[PROOF STEP]
by (intro sum.mono_neutral_cong_right)
         (auto simp: g_def lookup_single when_def split: if_splits)
[PROOF STATE]
proof (state)
this:
lookup (local.fund_sym_step_monom p) k = (\<Sum>x\<in>(if k \<in> {1..n} then {k - 1} else {}). g (k - 1) - g k)

goal (1 subgoal):
 1. lookup (local.fund_sym_step_monom p) k = (if k \<in> {1..n} then g (k - 1) - g k else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (local.fund_sym_step_monom p) k = (\<Sum>x\<in>(if k \<in> {1..n} then {k - 1} else {}). g (k - 1) - g k)

goal (1 subgoal):
 1. lookup (local.fund_sym_step_monom p) k = (if k \<in> {1..n} then g (k - 1) - g k else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (local.fund_sym_step_monom p) k = (if k \<in> {1..n} then g (k - 1) - g k else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lookup (local.fund_sym_step_monom p) ?k = (if ?k \<in> {1..n} then g (?k - 1) - g ?k else 0)

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
hence "(\<Prod>x. sym_mpoly A x ^ lookup (fund_sym_step_monom p) x :: 'a mpoly) =
           (\<Prod>x\<in>{1..n}. sym_mpoly A x ^ lookup (fund_sym_step_monom p) x)"
[PROOF STATE]
proof (prove)
using this:
lookup (local.fund_sym_step_monom p) ?k = (if ?k \<in> {1..n} then g (?k - 1) - g ?k else 0)

goal (1 subgoal):
 1. (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = (\<Prod>x = 1..n. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
by (intro Prod_any.expand_superset) auto
[PROOF STATE]
proof (state)
this:
(\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = (\<Prod>x = 1..n. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = (\<Prod>x = 1..n. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "\<dots> = (\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (fund_sym_step_monom p) (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x = 1..n. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = (\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (local.fund_sym_step_monom p) (Suc x))
[PROOF STEP]
by (intro prod.reindex_bij_witness[of _ Suc "\<lambda>i. i - 1"]) auto
[PROOF STATE]
proof (state)
this:
(\<Prod>x = 1..n. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = (\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (local.fund_sym_step_monom p) (Suc x))

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>x = 1..n. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = (\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (local.fund_sym_step_monom p) (Suc x))

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
have "\<dots> = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (local.fund_sym_step_monom p) (Suc x)) = q
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (local.fund_sym_step_monom p) (Suc x)) = (\<Prod>i<n. sym_mpoly A (Suc i) ^ (g i - g (Suc i)))
[PROOF STEP]
by (intro prod.cong) (auto simp: *)
[PROOF STATE]
proof (state)
this:
(\<Prod>x<n. sym_mpoly A (Suc x) ^ lookup (local.fund_sym_step_monom p) (Suc x)) = q

goal (1 subgoal):
 1. \<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = q
[PROOF STEP]
show "fund_sym_step_poly p =
                  fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (fund_sym_step_monom p) x)"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x) = q

goal (1 subgoal):
 1. local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
[PROOF STEP]
by (simp add: c_def q_def f_def g_def fund_sym_step_monom_def fund_sym_step_coeff_def)
[PROOF STATE]
proof (state)
this:
local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_fund_sym_step_poly_less:
  assumes "finite A" and "lead_monom p \<noteq> 0" and "decr p"
  shows   "lead_monom (p - fund_sym_step_poly p) < lead_monom p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
proof (cases "p = fund_sym_step_poly p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
 2. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p = local.fund_sym_step_poly p

goal (2 subgoals):
 1. p = local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
 2. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = local.fund_sym_step_poly p

goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p = local.fund_sym_step_poly p
finite A
lead_monom p \<noteq> 0
decr p

goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
lead_monom (p - local.fund_sym_step_poly p) < lead_monom p

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> local.fund_sym_step_poly p

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
lead_monom p \<noteq> 0
decr p
[PROOF STEP]
have [simp]: "p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
finite A
lead_monom p \<noteq> 0
decr p

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
let ?q = "fund_sym_step_poly p" and ?m = "lead_monom p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
have "coeff (p - ?q) ?m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)
[PROOF STEP]
using fund_sym_step_poly[of p] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
symmetric_mpoly A (local.fund_sym_step_poly p)
finite A
lead_monom p \<noteq> 0
decr p

goal (1 subgoal):
 1. MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)
[PROOF STEP]
by (simp add: lead_coeff_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
have "lead_coeff (p - ?q) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (p - local.fund_sym_step_poly p) \<noteq> (0::'a)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
p \<noteq> local.fund_sym_step_poly p

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (p - local.fund_sym_step_poly p) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (p - local.fund_sym_step_poly p) \<noteq> (0::'a)

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)
Symmetric_Polynomials.lead_coeff (p - local.fund_sym_step_poly p) \<noteq> (0::'a)
[PROOF STEP]
have "lead_monom (p - ?q) \<noteq> ?m"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)
Symmetric_Polynomials.lead_coeff (p - local.fund_sym_step_poly p) \<noteq> (0::'a)

goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) \<noteq> lead_monom p
[PROOF STEP]
unfolding lead_coeff_def
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom p) = (0::'a)
MPoly_Type.coeff (p - local.fund_sym_step_poly p) (lead_monom (p - local.fund_sym_step_poly p)) \<noteq> (0::'a)

goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) \<noteq> lead_monom p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lead_monom (p - local.fund_sym_step_poly p) \<noteq> lead_monom p

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lead_monom (p - local.fund_sym_step_poly p) \<noteq> lead_monom p

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
have "lead_monom (p - ?q) \<le> ?m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) \<le> lead_monom p
[PROOF STEP]
using fund_sym_step_poly[of p] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
symmetric_mpoly A (local.fund_sym_step_poly p)
finite A
lead_monom p \<noteq> 0
decr p

goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) \<le> lead_monom p
[PROOF STEP]
by (intro order.trans[OF lead_monom_diff] max.boundedI) auto
[PROOF STATE]
proof (state)
this:
lead_monom (p - local.fund_sym_step_poly p) \<le> lead_monom p

goal (1 subgoal):
 1. p \<noteq> local.fund_sym_step_poly p \<Longrightarrow> lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lead_monom (p - local.fund_sym_step_poly p) \<noteq> lead_monom p
lead_monom (p - local.fund_sym_step_poly p) \<le> lead_monom p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lead_monom (p - local.fund_sym_step_poly p) \<noteq> lead_monom p
lead_monom (p - local.fund_sym_step_poly p) \<le> lead_monom p

goal (1 subgoal):
 1. lead_monom (p - local.fund_sym_step_poly p) < lead_monom p
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
lead_monom (p - local.fund_sym_step_poly p) < lead_monom p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_dom_aux:
  assumes "finite B" "vars p \<subseteq> B" "A \<subseteq> B"
  shows   "fund_sym_poly_wit_dom p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
A \<subseteq> B

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
proof (induction p rule: lead_monom_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>vars p \<subseteq> B; \<And>p'. \<lbrakk>vars p' \<subseteq> B; lead_monom p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p'; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
case (less p)
[PROOF STATE]
proof (state)
this:
vars p \<subseteq> B
\<lbrakk>vars ?p' \<subseteq> B; lead_monom ?p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom ?p'
A \<subseteq> B

goal (1 subgoal):
 1. \<And>p. \<lbrakk>vars p \<subseteq> B; \<And>p'. \<lbrakk>vars p' \<subseteq> B; lead_monom p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p'; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
have [simp]: "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
by (rule finite_subset[of _ B]) fact+
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. \<And>p. \<lbrakk>vars p \<subseteq> B; \<And>p'. \<lbrakk>vars p' \<subseteq> B; lead_monom p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p'; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
proof (cases "lead_monom p = 0 \<or> \<not>symmetric_mpoly A p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p) \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p)

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p) \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
hence [simp]: "p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p)

goal (1 subgoal):
 1. p \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p) \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
note decr = lookup_lead_monom_decreasing[of A p]
[PROOF STATE]
proof (state)
this:
\<lbrakk>symmetric_mpoly A p; ?i \<in> A; ?j \<in> A; ?i \<le> ?j\<rbrakk> \<Longrightarrow> lookup (lead_monom p) ?j \<le> lookup (lead_monom p) ?i

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p) \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
have "vars (p - fund_sym_step_poly p) \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
using fund_sym_step_poly[of p] decr False less.prems less.hyps \<open>A \<subseteq> B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
symmetric_mpoly A (local.fund_sym_step_poly p)
\<lbrakk>symmetric_mpoly A p; ?i \<in> A; ?j \<in> A; ?i \<le> ?j\<rbrakk> \<Longrightarrow> lookup (lead_monom p) ?j \<le> lookup (lead_monom p) ?i
\<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p)
A \<subseteq> B
vars p \<subseteq> B
A \<subseteq> B

goal (1 subgoal):
 1. vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
by (intro order.trans[OF vars_diff]) auto
[PROOF STATE]
proof (state)
this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p) \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
hence "fund_sym_poly_wit_dom (p - local.fund_sym_step_poly p)"
[PROOF STATE]
proof (prove)
using this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom (p - local.fund_sym_step_poly p)
[PROOF STEP]
using False less.prems less.hyps decr
[PROOF STATE]
proof (prove)
using this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B
\<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p)
A \<subseteq> B
vars p \<subseteq> B
\<lbrakk>symmetric_mpoly A p; ?i \<in> A; ?j \<in> A; ?i \<le> ?j\<rbrakk> \<Longrightarrow> lookup (lead_monom p) ?j \<le> lookup (lead_monom p) ?i

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom (p - local.fund_sym_step_poly p)
[PROOF STEP]
by (intro less.IH fund_sym_step_poly symmetric_mpoly_diff
                lead_monom_fund_sym_step_poly_less) (auto simp: decr_def)
[PROOF STATE]
proof (state)
this:
local.fund_sym_poly_wit_dom (p - local.fund_sym_step_poly p)

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> symmetric_mpoly A p) \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
local.fund_sym_poly_wit_dom (p - local.fund_sym_step_poly p)

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
using fund_sym_poly_wit.domintros
[PROOF STATE]
proof (prove)
using this:
local.fund_sym_poly_wit_dom (p - local.fund_sym_step_poly p)
(\<And>x. \<lbrakk>symmetric_mpoly A ?p; lead_monom ?p \<noteq> 0; \<not> local.fund_sym_poly_wit_dom (?p - local.fund_sym_step_poly ?p); x \<in> vars ?p; x \<in> A\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> local.fund_sym_poly_wit_dom ?p

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.fund_sym_poly_wit_dom p

goal (1 subgoal):
 1. lead_monom p = 0 \<or> \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
qed (auto intro: fund_sym_poly_wit.domintros)
[PROOF STATE]
proof (state)
this:
local.fund_sym_poly_wit_dom p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_dom [intro]: "fund_sym_poly_wit_dom p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
consider "\<not>symmetric_mpoly A p" | "vars p \<inter> A = {}"  | "symmetric_mpoly A p" "A \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> symmetric_mpoly A p \<Longrightarrow> thesis; vars p \<inter> A = {} \<Longrightarrow> thesis; \<lbrakk>symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using symmetric_mpoly_imp_orthogonal_or_subset[of A p]
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p \<Longrightarrow> vars p \<inter> A = {} \<or> A \<subseteq> vars p

goal (1 subgoal):
 1. \<lbrakk>\<not> symmetric_mpoly A p \<Longrightarrow> thesis; vars p \<inter> A = {} \<Longrightarrow> thesis; \<lbrakk>symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> symmetric_mpoly A p \<Longrightarrow> ?thesis; vars p \<inter> A = {} \<Longrightarrow> ?thesis; \<lbrakk>symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> symmetric_mpoly A p \<Longrightarrow> ?thesis; vars p \<inter> A = {} \<Longrightarrow> ?thesis; \<lbrakk>symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. vars p \<inter> A = {} \<Longrightarrow> local.fund_sym_poly_wit_dom p
 3. \<lbrakk>symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
assume "symmetric_mpoly A p" "A \<subseteq> vars p"
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A p
A \<subseteq> vars p

goal (3 subgoals):
 1. \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. vars p \<inter> A = {} \<Longrightarrow> local.fund_sym_poly_wit_dom p
 3. \<lbrakk>symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
A \<subseteq> vars p

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
using fund_sym_poly_wit_dom_aux[of "vars p" p]
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
A \<subseteq> vars p
\<lbrakk>finite (vars p); vars p \<subseteq> vars p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> local.fund_sym_poly_wit_dom p

goal (1 subgoal):
 1. local.fund_sym_poly_wit_dom p
[PROOF STEP]
by (auto simp: vars_finite)
[PROOF STATE]
proof (state)
this:
local.fund_sym_poly_wit_dom p

goal (2 subgoals):
 1. \<not> symmetric_mpoly A p \<Longrightarrow> local.fund_sym_poly_wit_dom p
 2. vars p \<inter> A = {} \<Longrightarrow> local.fund_sym_poly_wit_dom p
[PROOF STEP]
qed (auto intro: fund_sym_poly_wit.domintros)
[PROOF STATE]
proof (state)
this:
local.fund_sym_poly_wit_dom p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_coeffs_aux:
  assumes "finite B" "vars p \<subseteq> B" "symmetric_mpoly A p" "A \<subseteq> B"
  shows   "vars (coeff (fund_sym_poly_wit p) m) \<subseteq> B - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
proof (induction p rule: fund_sym_poly_wit.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<lbrakk>\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}); finite B; vars (p - local.fund_sym_step_poly p) \<subseteq> B; symmetric_mpoly A (p - local.fund_sym_step_poly p); A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
case (1 p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}); finite B; vars (p - local.fund_sym_step_poly p) \<subseteq> B; symmetric_mpoly A (p - local.fund_sym_step_poly p); A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<lbrakk>\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}); finite B; vars (p - local.fund_sym_step_poly p) \<subseteq> B; symmetric_mpoly A (p - local.fund_sym_step_poly p); A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
proof (cases "lead_monom p = 0 \<or> vars p \<inter> A = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (lead_monom p = 0 \<or> vars p \<inter> A = {})

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
have "vars (p - fund_sym_step_poly p) \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
using "1.prems" fund_sym_step_poly[of p]
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
symmetric_mpoly A (local.fund_sym_step_poly p)

goal (1 subgoal):
 1. vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
by (intro order.trans[OF vars_diff]) auto
[PROOF STATE]
proof (state)
this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
with 1 False
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}); finite B; vars (p - local.fund_sym_step_poly p) \<subseteq> B; symmetric_mpoly A (p - local.fund_sym_step_poly p); A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
\<not> (lead_monom p = 0 \<or> vars p \<inter> A = {})
vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
have "vars (coeff (fund_sym_poly_wit (p - fund_sym_step_poly p)) m) \<subseteq> B - A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}); finite B; vars (p - local.fund_sym_step_poly p) \<subseteq> B; symmetric_mpoly A (p - local.fund_sym_step_poly p); A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
\<not> (lead_monom p = 0 \<or> vars p \<inter> A = {})
vars (p - local.fund_sym_step_poly p) \<subseteq> B

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A
[PROOF STEP]
by (intro 1 symmetric_mpoly_diff fund_sym_step_poly) auto
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
hence "vars (coeff (fund_sym_poly_wit (p - fund_sym_step_poly p) +
                monom (fund_sym_step_monom p) (fund_sym_step_coeff p)) m) \<subseteq> B - A"
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p) + MPoly_Type.monom (local.fund_sym_step_monom p) (local.fund_sym_step_coeff p)) m) \<subseteq> B - A
[PROOF STEP]
unfolding coeff_add coeff_monom
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m + (local.fund_sym_step_coeff p when m = local.fund_sym_step_monom p)) \<subseteq> B - A
[PROOF STEP]
using vars_fund_sym_step_coeff[of p] "1.prems"
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) \<subseteq> B - A
vars (local.fund_sym_step_coeff p) \<subseteq> vars p - A
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m + (local.fund_sym_step_coeff p when m = local.fund_sym_step_monom p)) \<subseteq> B - A
[PROOF STEP]
by (intro order.trans[OF vars_add] Un_least order.trans[OF vars_monom_subset])
         (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p) + MPoly_Type.monom (local.fund_sym_step_monom p) (local.fund_sym_step_coeff p)) m) \<subseteq> B - A

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p) + MPoly_Type.monom (local.fund_sym_step_monom p) (local.fund_sym_step_coeff p)) m) \<subseteq> B - A

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
using "1.prems" False
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p) + MPoly_Type.monom (local.fund_sym_step_monom p) (local.fund_sym_step_coeff p)) m) \<subseteq> B - A
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
\<not> (lead_monom p = 0 \<or> vars p \<inter> A = {})

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
unfolding fund_sym_poly_wit.simps[of p]
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p) + MPoly_Type.monom (local.fund_sym_step_monom p) (local.fund_sym_step_coeff p)) m) \<subseteq> B - A
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
\<not> (lead_monom p = 0 \<or> vars p \<inter> A = {})

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (if \<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {} then Const p else local.fund_sym_poly_wit (p - local.fund_sym_step_poly p) + MPoly_Type.monom (local.fund_sym_step_monom p) (local.fund_sym_step_coeff p)) m) \<subseteq> B - A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A

goal (1 subgoal):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A
[PROOF STEP]
qed (insert "1.prems",
       auto simp: fund_sym_poly_wit.simps[of p] mpoly_coeff_Const lead_monom_eq_0_iff)
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> B - A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_coeffs:
  assumes "symmetric_mpoly A p"
  shows   "vars (coeff (fund_sym_poly_wit p) m) \<subseteq> vars p - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
proof (cases "A \<subseteq> vars p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
 2. \<not> A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A \<subseteq> vars p

goal (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
 2. \<not> A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
with fund_sym_poly_wit_coeffs_aux[of "vars p" p m] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite (vars p); vars p \<subseteq> vars p; symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
symmetric_mpoly A p
A \<subseteq> vars p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (vars p); vars p \<subseteq> vars p; symmetric_mpoly A p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
symmetric_mpoly A p
A \<subseteq> vars p

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
by (auto simp: vars_finite)
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A

goal (1 subgoal):
 1. \<not> A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> A \<subseteq> vars p

goal (1 subgoal):
 1. \<not> A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
hence "vars p \<inter> A = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> A \<subseteq> vars p

goal (1 subgoal):
 1. vars p \<inter> A = {}
[PROOF STEP]
using symmetric_mpoly_imp_orthogonal_or_subset[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<not> A \<subseteq> vars p
vars p \<inter> A = {} \<or> A \<subseteq> vars p

goal (1 subgoal):
 1. vars p \<inter> A = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars p \<inter> A = {}

goal (1 subgoal):
 1. \<not> A \<subseteq> vars p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> A = {}

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A
[PROOF STEP]
by (auto simp: fund_sym_poly_wit.simps[of p] mpoly_coeff_Const)
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) \<subseteq> vars p - A

goal:
No subgoals!
[PROOF STEP]
qed