[STATEMENT]
lemma fund_sym_poly_wit_vars: "vars (fund_sym_poly_wit p) \<subseteq> {1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
proof (cases "symmetric_mpoly A p \<and> A \<subseteq> vars p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. symmetric_mpoly A p \<and> A \<subseteq> vars p \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A p \<and> A \<subseteq> vars p

goal (2 subgoals):
 1. symmetric_mpoly A p \<and> A \<subseteq> vars p \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
define B where "B = vars p"
[PROOF STATE]
proof (state)
this:
B = vars p

goal (2 subgoals):
 1. symmetric_mpoly A p \<and> A \<subseteq> vars p \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
have "finite B" "vars p \<subseteq> B" "symmetric_mpoly A p" "A \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finite B &&& vars p \<subseteq> B) &&& symmetric_mpoly A p &&& A \<subseteq> B
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p \<and> A \<subseteq> vars p

goal (1 subgoal):
 1. (finite B &&& vars p \<subseteq> B) &&& symmetric_mpoly A p &&& A \<subseteq> B
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p \<and> A \<subseteq> vars p

goal (1 subgoal):
 1. (finite (vars p) &&& vars p \<subseteq> vars p) &&& symmetric_mpoly A p &&& A \<subseteq> vars p
[PROOF STEP]
by (auto simp: vars_finite)
[PROOF STATE]
proof (state)
this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B

goal (2 subgoals):
 1. symmetric_mpoly A p \<and> A \<subseteq> vars p \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B

goal (1 subgoal):
 1. vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[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 (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) \<subseteq> {1..n}; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[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 (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) \<subseteq> {1..n}
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 (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) \<subseteq> {1..n}; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[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 (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[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 (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[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 (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
hence "vars (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) \<subseteq> {1..n}"
[PROOF STATE]
proof (prove)
using this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B

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

goal (1 subgoal):
 1. vars (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) \<subseteq> {1..n}
[PROOF STEP]
by (intro 1 symmetric_mpoly_diff fund_sym_step_poly) (auto simp: lead_monom_eq_0_iff)
[PROOF STATE]
proof (state)
this:
vars (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) \<subseteq> {1..n}

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

goal (1 subgoal):
 1. vars (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)) \<subseteq> {1..n}
[PROOF STEP]
by (intro order.trans[OF vars_add] Un_least order.trans[OF vars_monom_subset]
                  keys_fund_sym_step_monom) auto
[PROOF STATE]
proof (state)
this:
vars (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)) \<subseteq> {1..n}

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vars (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)) \<subseteq> {1..n}

goal (1 subgoal):
 1. vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
using "1.prems" False
[PROOF STATE]
proof (prove)
using this:
vars (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)) \<subseteq> {1..n}
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 (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
unfolding fund_sym_poly_wit.simps[of p]
[PROOF STATE]
proof (prove)
using this:
vars (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)) \<subseteq> {1..n}
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 (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)) \<subseteq> {1..n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}

goal (1 subgoal):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[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 (local.fund_sym_poly_wit p) \<subseteq> {1..n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}

goal (1 subgoal):
 1. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p)

goal (1 subgoal):
 1. \<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p) \<Longrightarrow> vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p)
[PROOF STEP]
consider "\<not>symmetric_mpoly A p" | "symmetric_mpoly A p" "vars p \<inter> A = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p)

goal (1 subgoal):
 1. \<lbrakk>\<not> symmetric_mpoly A p \<Longrightarrow> thesis; \<lbrakk>symmetric_mpoly A p; vars p \<inter> A = {}\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using symmetric_mpoly_imp_orthogonal_or_subset[of A p]
[PROOF STATE]
proof (prove)
using this:
\<not> (symmetric_mpoly A p \<and> A \<subseteq> vars p)
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; \<lbrakk>symmetric_mpoly A p; vars p \<inter> A = {}\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> symmetric_mpoly A p \<Longrightarrow> ?thesis; \<lbrakk>symmetric_mpoly A p; vars p \<inter> A = {}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
[PROOF STEP]
by cases (auto simp: fund_sym_poly_wit.simps[of p])
[PROOF STATE]
proof (state)
this:
vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_insertion_aux:
  assumes "finite B" "vars p \<subseteq> B" "symmetric_mpoly A p" "A \<subseteq> B"
  shows   "insertion (sym_mpoly A) (fund_sym_poly_wit p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[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. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[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> insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[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> insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
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> insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
from "1.prems"
[PROOF STATE]
proof (chain)
picking this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
[PROOF STEP]
have "decr p"
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B

goal (1 subgoal):
 1. decr p
[PROOF STEP]
using lookup_lead_monom_decreasing[of A p]
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<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. decr p
[PROOF STEP]
by (auto simp: decr_def)
[PROOF STATE]
proof (state)
this:
decr p

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> insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p; finite B; vars p \<subseteq> B; symmetric_mpoly A p; A \<subseteq> B\<rbrakk> \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[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> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[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> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = 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 "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> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
hence "insertion (sym_mpoly A) (fund_sym_poly_wit (p - fund_sym_step_poly p)) =
            p - 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. insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
[PROOF STEP]
using 1 False
[PROOF STATE]
proof (prove)
using this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B
\<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> insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
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. insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
[PROOF STEP]
by (intro 1 symmetric_mpoly_diff fund_sym_step_poly) auto
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p

goal (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
have "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)
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]
using "1.prems" finite_subset[of A B] False \<open>decr p\<close>
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
symmetric_mpoly A p
A \<subseteq> B
\<lbrakk>A \<subseteq> B; finite B\<rbrakk> \<Longrightarrow> finite A
\<not> (lead_monom p = 0 \<or> vars p \<inter> A = {})
decr p

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 (intro fund_sym_step_poly) auto
[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 (2 subgoals):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> (lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
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 ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
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 (1 subgoal):
 1. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
unfolding fund_sym_poly_wit.simps[of p]
[PROOF STATE]
proof (prove)
using this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) = p - local.fund_sym_step_poly p
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 (1 subgoal):
 1. insertion (sym_mpoly A) (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)) = p
[PROOF STEP]
by (auto simp: insertion_add)
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p

goal (1 subgoal):
 1. lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
qed (auto simp: fund_sym_poly_wit.simps[of p])
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_insertion:
  assumes "symmetric_mpoly A p"
  shows   "insertion (sym_mpoly A) (fund_sym_poly_wit p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
proof (cases "A \<subseteq> vars p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> A \<subseteq> vars p

goal (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[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 (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
 2. \<not> A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> A = {}

goal (1 subgoal):
 1. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
by (auto simp: fund_sym_poly_wit.simps[of p])
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p

goal (1 subgoal):
 1. A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A \<subseteq> vars p

goal (1 subgoal):
 1. A \<subseteq> vars p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
with fund_sym_poly_wit_insertion_aux[of "vars p" p] 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> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
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> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
symmetric_mpoly A p
A \<subseteq> vars p

goal (1 subgoal):
 1. insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
[PROOF STEP]
by (auto simp: vars_finite)
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fund_sym_poly_wit_coeff:
  assumes "\<forall>m. coeff p m \<in> C" "ring_closed C"
  shows   "\<forall>m m'. coeff (coeff (fund_sym_poly_wit p) m) m' \<in> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>m. MPoly_Type.coeff p m \<in> C

goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[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 = {}); \<forall>m. MPoly_Type.coeff (p - local.fund_sym_step_poly p) m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C; \<forall>m. MPoly_Type.coeff p m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[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 = {}); \<forall>m. MPoly_Type.coeff (p - local.fund_sym_step_poly p) m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C
\<forall>m. MPoly_Type.coeff p m \<in> C

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<lbrakk>\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}); \<forall>m. MPoly_Type.coeff (p - local.fund_sym_step_poly p) m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C; \<forall>m. MPoly_Type.coeff p m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
interpret ring_closed C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_closed C
[PROOF STEP]
by fact
[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 = {}); \<forall>m. MPoly_Type.coeff (p - local.fund_sym_step_poly p) m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C; \<forall>m. MPoly_Type.coeff p m \<in> C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
proof (cases "\<not>symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
 2. \<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}

goal (2 subgoals):
 1. \<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {} \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
 2. \<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}

goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
using "1.prems"
[PROOF STATE]
proof (prove)
using this:
\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}
\<forall>m. MPoly_Type.coeff p m \<in> C

goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
by (auto simp: fund_sym_poly_wit.simps[of p] mpoly_coeff_Const)
[PROOF STATE]
proof (state)
this:
\<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C

goal (1 subgoal):
 1. \<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {})

goal (1 subgoal):
 1. \<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
have *: "\<forall>m m'. coeff (coeff (fund_sym_poly_wit (p - fund_sym_step_poly p)) m) m' \<in> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C
[PROOF STEP]
using False "1.prems" assms coeff_fund_sym_step_poly [of p]
[PROOF STATE]
proof (prove)
using this:
\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {})
\<forall>m. MPoly_Type.coeff p m \<in> C
\<forall>m. MPoly_Type.coeff p m \<in> C
ring_closed C
\<lbrakk>\<forall>m. MPoly_Type.coeff p m \<in> ?C; ring_closed ?C\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (local.fund_sym_step_poly p) ?m \<in> ?C

goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C
[PROOF STEP]
by (intro 1) auto
[PROOF STATE]
proof (state)
this:
\<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C

goal (1 subgoal):
 1. \<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {}) \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
proof (intro allI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
case (1 m m')
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
using * False coeff_fund_sym_step_coeff[of p m'] "1.prems"
[PROOF STATE]
proof (prove)
using this:
\<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit (p - local.fund_sym_step_poly p)) m) m' \<in> C
\<not> (\<not> symmetric_mpoly A p \<or> lead_monom p = 0 \<or> vars p \<inter> A = {})
MPoly_Type.coeff (local.fund_sym_step_coeff p) m' \<in> {Symmetric_Polynomials.lead_coeff p, 0::'a}
\<forall>m. MPoly_Type.coeff p m \<in> C

goal (1 subgoal):
 1. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C
[PROOF STEP]
by (auto simp: fund_sym_poly_wit.simps[of p] coeff_monom lead_coeff_def when_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (local.fund_sym_poly_wit p) m) m' \<in> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_sym_mpoly_prod:
  assumes "finite A"
  shows   "lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i :: 'a mpoly) =
             (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
have "(\<Prod>i=1..n. lead_coeff (sym_mpoly A i ^ h i :: 'a mpoly)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i = 1..n. Symmetric_Polynomials.lead_coeff (sym_mpoly A i ^ h i)) = (1::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. (\<Prod>i = 1..n. Symmetric_Polynomials.lead_coeff (sym_mpoly A i ^ h i)) = (1::'a)
[PROOF STEP]
unfolding n_def
[PROOF STATE]
proof (prove)
using this:
finite A

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

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
hence "lead_monom (\<Prod>i=1..n. sym_mpoly A i ^ h i :: 'a mpoly) =
           (\<Sum>i=1..n. lead_monom (sym_mpoly A i ^ h i :: 'a mpoly))"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i = 1..n. Symmetric_Polynomials.lead_coeff (sym_mpoly A i ^ h i)) = (1::'a)

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. lead_monom (sym_mpoly A i ^ h i))
[PROOF STEP]
by (subst lead_monom_prod) auto
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. lead_monom (sym_mpoly A i ^ h i))

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. lead_monom (sym_mpoly A i ^ h i))

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
have "\<dots> = (\<Sum>i=1..n. of_nat (h i) * lead_monom (sym_mpoly A i :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 1..n. lead_monom (sym_mpoly A i ^ h i)) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
by (intro sum.cong refl, subst lead_monom_power)
       (auto simp: lead_coeff_power assms n_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 1..n. lead_monom (sym_mpoly A i ^ h i)) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly A i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_sym_mpoly_prod_notin:
  assumes "finite A" "k \<notin> A"
  shows   "lookup (lead_monom (\<Prod>i=1..n. sym_mpoly A i ^ h i :: 'a mpoly)) k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
have xs: "set xs = A" "distinct xs" "sorted xs" and [simp]: "length xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs = A &&& distinct xs &&& sorted xs) &&& length xs = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
k \<notin> A

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

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
have "lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i :: 'a mpoly) =
          (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i))
[PROOF STEP]
by (subst lead_monom_sym_mpoly_prod) (use xs assms in auto)
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i))

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i))

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
have "lookup \<dots> k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i)) k = 0
[PROOF STEP]
unfolding lookup_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 1..n. lookup (of_nat (h x) * lead_monom (sym_mpoly (set xs) x)) k) = 0
[PROOF STEP]
by (intro sum.neutral ballI, subst lead_monom_sym_mpoly)
      (insert xs assms, auto simp: xs lead_monom_sym_mpoly lookup_monom_of_set set_conv_nth)
[PROOF STATE]
proof (state)
this:
lookup (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i)) k = 0

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) k = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_sym_mpoly_prod_in:
  assumes "finite A" "k < n"
  shows   "lookup (lead_monom (\<Prod>i=1..n. sym_mpoly A i ^ h i :: 'a mpoly)) (xs ! k) =
             (\<Sum>i=k+1..n. h i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
have xs: "set xs = A" "distinct xs" "sorted xs" and [simp]: "length xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs = A &&& distinct xs &&& sorted xs) &&& length xs = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
k < n

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

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
have "lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i :: 'a mpoly) =
             (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i))
[PROOF STEP]
by (subst lead_monom_sym_mpoly_prod) (use xs assms in simp_all)
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i))

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i) = (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i))

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
have "\<dots> = (\<Sum>i=1..n. of_nat (h i) * monom_of_set (set (take i xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i)) = (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs)))
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
set xs = A
distinct xs
sorted xs

goal (1 subgoal):
 1. (\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i)) = (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs)))
[PROOF STEP]
by (intro sum.cong refl, subst lead_monom_sym_mpoly) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i)) = (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs)))

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 1..n. of_nat (h i) * lead_monom (sym_mpoly (set xs) i)) = (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs)))

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
have "lookup \<dots> (xs ! k) = (\<Sum>i | i \<in> {1..n} \<and> xs ! k \<in> set (take i xs). h i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs))) (xs ! k) = (\<Sum>i | i \<in> {1..n} \<and> xs ! k \<in> set (take i xs). h i)
[PROOF STEP]
unfolding lookup_sum lookup_monom_of_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x = 1..n. lookup (of_nat (h x) * monom_of_set (set (take x xs))) (xs ! k)) = (\<Sum>i | i \<in> {1..n} \<and> xs ! k \<in> set (take i xs). h i)
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) auto
[PROOF STATE]
proof (state)
this:
lookup (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs))) (xs ! k) = (\<Sum>i | i \<in> {1..n} \<and> xs ! k \<in> set (take i xs). h i)

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (\<Sum>i = 1..n. of_nat (h i) * monom_of_set (set (take i xs))) (xs ! k) = (\<Sum>i | i \<in> {1..n} \<and> xs ! k \<in> set (take i xs). h i)

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
have "{i. i \<in> {1..n} \<and> xs ! k \<in> set (take i xs)} = {k+1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i \<in> {1..n}. xs ! k \<in> set (take i xs)} = {k + 1..n}
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)} \<Longrightarrow> x \<in> {k + 1..n}
 2. \<And>x. x \<in> {k + 1..n} \<Longrightarrow> x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)} \<Longrightarrow> x \<in> {k + 1..n}
 2. \<And>x. x \<in> {k + 1..n} \<Longrightarrow> x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)}
[PROOF STEP]
assume i: "i \<in> {k+1..n}"
[PROOF STATE]
proof (state)
this:
i \<in> {k + 1..n}

goal (2 subgoals):
 1. \<And>x. x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)} \<Longrightarrow> x \<in> {k + 1..n}
 2. \<And>x. x \<in> {k + 1..n} \<Longrightarrow> x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)}
[PROOF STEP]
hence "take i xs ! k = xs ! k" "k < n" "k < i"
[PROOF STATE]
proof (prove)
using this:
i \<in> {k + 1..n}

goal (1 subgoal):
 1. take i xs ! k = xs ! k &&& k < n &&& k < i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> {k + 1..n}
finite A
k < n

goal (1 subgoal):
 1. take i xs ! k = xs ! k &&& k < n &&& k < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
take i xs ! k = xs ! k
k < n
k < i

goal (2 subgoals):
 1. \<And>x. x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)} \<Longrightarrow> x \<in> {k + 1..n}
 2. \<And>x. x \<in> {k + 1..n} \<Longrightarrow> x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)}
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i \<in> {k + 1..n}
take i xs ! k = xs ! k
k < n
k < i
[PROOF STEP]
show "i \<in> {i. i \<in> {1..n} \<and> xs ! k \<in> set (take i xs)}"
[PROOF STATE]
proof (prove)
using this:
i \<in> {k + 1..n}
take i xs ! k = xs ! k
k < n
k < i

goal (1 subgoal):
 1. i \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)}
[PROOF STEP]
by (force simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
i \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)}

goal (1 subgoal):
 1. \<And>x. x \<in> {i \<in> {1..n}. xs ! k \<in> set (take i xs)} \<Longrightarrow> x \<in> {k + 1..n}
[PROOF STEP]
qed (insert assms xs, auto simp: set_conv_nth Suc_le_eq nth_eq_iff_index_eq)
[PROOF STATE]
proof (state)
this:
{i \<in> {1..n}. xs ! k \<in> set (take i xs)} = {k + 1..n}

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}

goal (1 subgoal):
 1. lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ h i)) (xs ! k) = sum h {k + 1..n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_sym_poly_powerprod_inj:
  assumes "lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i :: 'a mpoly) =
             lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i :: 'a mpoly)"
  assumes "finite A" "keys m1 \<subseteq> {1..n}" "keys m2 \<subseteq> {1..n}"
  shows   "m1 = m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 = m2
[PROOF STEP]
proof (rule poly_mapping_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
fix k :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
have xs: "set xs = A" "distinct xs" "sorted xs" and [simp]: "length xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs = A &&& distinct xs &&& sorted xs) &&& length xs = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i)
finite A
keys m1 \<subseteq> {1..n}
keys m2 \<subseteq> {1..n}

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

goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
from assms(3,4)
[PROOF STATE]
proof (chain)
picking this:
keys m1 \<subseteq> {1..n}
keys m2 \<subseteq> {1..n}
[PROOF STEP]
have *: "i \<in> {1..n}" if "lookup m1 i \<noteq> 0 \<or> lookup m2 i \<noteq> 0" for i
[PROOF STATE]
proof (prove)
using this:
keys m1 \<subseteq> {1..n}
keys m2 \<subseteq> {1..n}

goal (1 subgoal):
 1. i \<in> {1..n}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
keys m1 \<subseteq> {1..n}
keys m2 \<subseteq> {1..n}
lookup m1 i \<noteq> 0 \<or> lookup m2 i \<noteq> 0

goal (1 subgoal):
 1. i \<in> {1..n}
[PROOF STEP]
by (auto simp: subset_iff in_keys_iff)
[PROOF STATE]
proof (state)
this:
lookup m1 ?i \<noteq> 0 \<or> lookup m2 ?i \<noteq> 0 \<Longrightarrow> ?i \<in> {1..n}

goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
have **: "(\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly) =
              (\<Prod>i=1..n. sym_mpoly A i ^ lookup m i :: 'a mpoly)" if "m \<in> {m1, m2}" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
using that *
[PROOF STATE]
proof (prove)
using this:
m \<in> {m1, m2}
lookup m1 ?i \<noteq> 0 \<or> lookup m2 ?i \<noteq> 0 \<Longrightarrow> ?i \<in> {1..n}

goal (1 subgoal):
 1. (\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by (intro Prod_any.expand_superset subsetI * ) (auto intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
?m \<in> {m1, m2} \<Longrightarrow> (\<Prod>i. sym_mpoly A i ^ lookup ?m i) = (\<Prod>i = 1..n. sym_mpoly A i ^ lookup ?m i)

goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
have ***: "lead_monom (\<Prod>i=1..n. sym_mpoly A i ^ lookup m1 i :: 'a mpoly) =
               lead_monom (\<Prod>i=1..n. sym_mpoly A i ^ lookup m2 i :: 'a mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m2 i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i)
finite A
keys m1 \<subseteq> {1..n}
keys m2 \<subseteq> {1..n}

goal (1 subgoal):
 1. lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m2 i)
[PROOF STEP]
by (simp add: ** )
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m2 i)

goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
have sum_eq: "sum (lookup m1) {Suc k..n} = sum (lookup m2) {Suc k..n}" if "k < n" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (lookup m1) {Suc k..n} = sum (lookup m2) {Suc k..n}
[PROOF STEP]
using arg_cong[OF ***, of "\<lambda>m. lookup m (xs ! k)"] \<open>finite A\<close> that
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m1 i)) (xs ! k) = lookup (lead_monom (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m2 i)) (xs ! k)
finite A
k < n

goal (1 subgoal):
 1. sum (lookup m1) {Suc k..n} = sum (lookup m2) {Suc k..n}
[PROOF STEP]
by (subst (asm) (1 2) lead_monom_sym_mpoly_prod_in) auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> sum (lookup m1) {Suc ?k..n} = sum (lookup m2) {Suc ?k..n}

goal (1 subgoal):
 1. \<And>k. lookup m1 k = lookup m2 k
[PROOF STEP]
show "lookup m1 k = lookup m2 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup m1 k = lookup m2 k
[PROOF STEP]
proof (cases "k \<in> {1..n}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
 2. k \<notin> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<notin> {1..n}

goal (2 subgoals):
 1. k \<in> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
 2. k \<notin> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
hence "lookup m1 k = 0" "lookup m2 k = 0"
[PROOF STATE]
proof (prove)
using this:
k \<notin> {1..n}

goal (1 subgoal):
 1. lookup m1 k = 0 &&& lookup m2 k = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<notin> {1..n}
lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i)
finite A
keys m1 \<subseteq> {1..n}
keys m2 \<subseteq> {1..n}

goal (1 subgoal):
 1. lookup m1 k = 0 &&& lookup m2 k = 0
[PROOF STEP]
by (auto simp: in_keys_iff)
[PROOF STATE]
proof (state)
this:
lookup m1 k = 0
lookup m2 k = 0

goal (2 subgoals):
 1. k \<in> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
 2. k \<notin> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup m1 k = 0
lookup m2 k = 0

goal (1 subgoal):
 1. lookup m1 k = lookup m2 k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup m1 k = lookup m2 k

goal (1 subgoal):
 1. k \<in> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<in> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k \<in> {1..n}

goal (1 subgoal):
 1. k \<in> {1..n} \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k \<in> {1..n}

goal (1 subgoal):
 1. lookup m1 k = lookup m2 k
[PROOF STEP]
proof (induction "n - k" arbitrary: k rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
case (less l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>n - ?k < n - l; ?k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ?k = lookup m2 ?k
l \<in> {1..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
have "sum (lookup m1) {Suc (l - 1)..n} = sum (lookup m2) {Suc (l - 1)..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (lookup m1) {Suc (l - 1)..n} = sum (lookup m2) {Suc (l - 1)..n}
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n - ?k < n - l; ?k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ?k = lookup m2 ?k
l \<in> {1..n}

goal (1 subgoal):
 1. sum (lookup m1) {Suc (l - 1)..n} = sum (lookup m2) {Suc (l - 1)..n}
[PROOF STEP]
by (intro sum_eq) auto
[PROOF STATE]
proof (state)
this:
sum (lookup m1) {Suc (l - 1)..n} = sum (lookup m2) {Suc (l - 1)..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (lookup m1) {Suc (l - 1)..n} = sum (lookup m2) {Suc (l - 1)..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
have "{Suc (l - 1)..n} = insert l {Suc l..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Suc (l - 1)..n} = insert l {Suc l..n}
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n - ?k < n - l; ?k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ?k = lookup m2 ?k
l \<in> {1..n}

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

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{Suc (l - 1)..n} = insert l {Suc l..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
have "sum (lookup m1) \<dots> = lookup m1 l + (\<Sum>i=Suc l..n. lookup m1 i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (lookup m1) (insert l {Suc l..n}) = lookup m1 l + sum (lookup m1) {Suc l..n}
[PROOF STEP]
by (subst sum.insert) auto
[PROOF STATE]
proof (state)
this:
sum (lookup m1) (insert l {Suc l..n}) = lookup m1 l + sum (lookup m1) {Suc l..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (lookup m1) (insert l {Suc l..n}) = lookup m1 l + sum (lookup m1) {Suc l..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
have "(\<Sum>i=Suc l..n. lookup m1 i) = (\<Sum>i=Suc l..n. lookup m2 i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (lookup m1) {Suc l..n} = sum (lookup m2) {Suc l..n}
[PROOF STEP]
by (intro sum.cong less) auto
[PROOF STATE]
proof (state)
this:
sum (lookup m1) {Suc l..n} = sum (lookup m2) {Suc l..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (lookup m1) {Suc l..n} = sum (lookup m2) {Suc l..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
have "sum (lookup m2) (insert l {Suc l..n}) = lookup m2 l + (\<Sum>i=Suc l..n. lookup m2 i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (lookup m2) (insert l {Suc l..n}) = lookup m2 l + sum (lookup m2) {Suc l..n}
[PROOF STEP]
by (subst sum.insert) auto
[PROOF STATE]
proof (state)
this:
sum (lookup m2) (insert l {Suc l..n}) = lookup m2 l + sum (lookup m2) {Suc l..n}

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<And>ka. \<lbrakk>n - ka < n - k; ka \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 ka = lookup m2 ka; k \<in> {1..n}\<rbrakk> \<Longrightarrow> lookup m1 k = lookup m2 k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup m1 l + sum (lookup m2) {Suc l..n} = lookup m2 l + sum (lookup m2) {Suc l..n}
[PROOF STEP]
show "lookup m1 l = lookup m2 l"
[PROOF STATE]
proof (prove)
using this:
lookup m1 l + sum (lookup m2) {Suc l..n} = lookup m2 l + sum (lookup m2) {Suc l..n}

goal (1 subgoal):
 1. lookup m1 l = lookup m2 l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup m1 l = lookup m2 l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lookup m1 k = lookup m2 k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lookup m1 k = lookup m2 k

goal:
No subgoals!
[PROOF STEP]
qed