[GOAL]
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
⊢ natDegree (cancelLeads p q) < natDegree q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : p = 0
⊢ natDegree (cancelLeads p q) < natDegree q
[PROOFSTEP]
convert hq
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : p = 0
⊢ natDegree (cancelLeads p q) = 0
[PROOFSTEP]
simp [hp, cancelLeads]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
⊢ natDegree (cancelLeads p q) < natDegree q
[PROOFSTEP]
rw [cancelLeads, sub_eq_add_neg, tsub_eq_zero_iff_le.mpr h, pow_zero, mul_one]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) < natDegree q
[PROOFSTEP]
by_cases h0 : C p.leadingCoeff * q + -(C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p) = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) < natDegree q
[PROOFSTEP]
exact (le_of_eq (by simp only [h0, natDegree_zero])).trans_lt hq
[GOAL]
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = 0
[PROOFSTEP]
simp only [h0, natDegree_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) < natDegree q
[PROOFSTEP]
apply lt_of_le_of_ne
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) ≤ natDegree q
[PROOFSTEP]
rw [natDegree_add_le_iff_left]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q) ≤ natDegree q
[PROOFSTEP]
apply natDegree_C_mul_le
[GOAL]
case neg.a.qn
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (-(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) ≤ natDegree q
[PROOFSTEP]
refine (natDegree_neg (C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p)).le.trans ?_
[GOAL]
case neg.a.qn
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) ≤ natDegree q
[PROOFSTEP]
exact natDegree_mul_le.trans <| Nat.add_le_of_le_sub h <| natDegree_C_mul_X_pow_le _ _
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : ¬↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
⊢ natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) ≠ natDegree q
[PROOFSTEP]
contrapose! h0
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = natDegree q
⊢ ↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p) = 0
[PROOFSTEP]
rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h, add_comm _ p.natDegree]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = natDegree q
⊢ coeff
      (↑C (leadingCoeff p) * q +
        -(↑C (leadingCoeff q) * (p * X ^ (natDegree p + (natDegree q - natDegree p) - natDegree p))))
      (natDegree p + (natDegree q - natDegree p)) =
    0
[PROOFSTEP]
simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : leadingCoeff p * leadingCoeff q = leadingCoeff q * leadingCoeff p
h : natDegree p ≤ natDegree q
hq : 0 < natDegree q
hp : ¬p = 0
h0 : natDegree (↑C (leadingCoeff p) * q + -(↑C (leadingCoeff q) * X ^ (natDegree q - natDegree p) * p)) = natDegree q
⊢ leadingCoeff p * coeff q (natDegree p + (natDegree q - natDegree p)) + -(leadingCoeff q * coeff p (natDegree p)) = 0
[PROOFSTEP]
rw [add_comm p.natDegree, tsub_add_cancel_of_le h, ← leadingCoeff, ← leadingCoeff, comm, add_right_neg]


[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ mirror 0 = 0
[PROOFSTEP]
simp [mirror]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
classical
by_cases ha : a = 0
· rw [ha, monomial_zero_right, mirror_zero]
·
  rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ← C_mul_X_pow_eq_monomial,
    reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
rw [ha, monomial_zero_right, mirror_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : ¬a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
[PROOFSTEP]
rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ← C_mul_X_pow_eq_monomial,
  reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
rw [hp, mirror_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ natDegree (mirror p) = natDegree p
[PROOFSTEP]
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow, tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ leadingCoeff (reverse p) * leadingCoeff (X ^ natTrailingDegree p) ≠ 0
[PROOFSTEP]
rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
[PROOFSTEP]
rw [hp, mirror_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
[PROOFSTEP]
rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp), reverse_natTrailingDegree, zero_add]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
by_cases h2 : p.natDegree < n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ natDegree (mirror p) < n
[PROOFSTEP]
rwa [mirror_natDegree]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
⊢ 0 = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
h1 : n ≤ natDegree p + natTrailingDegree p
⊢ 0 = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
h1 : n ≤ natDegree p + natTrailingDegree p
⊢ natDegree p + natTrailingDegree p - n < natTrailingDegree p
[PROOFSTEP]
exact (tsub_lt_iff_left h1).mpr (Nat.add_lt_add_right h2 _)
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : natDegree p < n
h1 : ¬n ≤ natDegree p + natTrailingDegree p
⊢ 0 = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : ¬natDegree p < n
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [not_lt] at h2
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
⊢ coeff (mirror p) n = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
rw [revAt_le (h2.trans (Nat.le_add_right _ _))]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
by_cases h3 : p.natTrailingDegree ≤ n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : natTrailingDegree p ≤ n
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
rw [← tsub_add_eq_add_tsub h2, ← tsub_tsub_assoc h2 h3, mirror, coeff_mul_X_pow', if_pos h3, coeff_reverse,
  revAt_le (tsub_le_self.trans h2)]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : ¬natTrailingDegree p ≤ n
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
rw [not_le] at h3
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ coeff (mirror p) n = coeff p (natDegree p + natTrailingDegree p - n)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt (lt_tsub_iff_right.mpr (Nat.add_lt_add_left h3 _))]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ coeff (mirror p) n = 0
[PROOFSTEP]
exact coeff_eq_zero_of_lt_natTrailingDegree (by rwa [mirror_natTrailingDegree])
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
h2 : n ≤ natDegree p
h3 : n < natTrailingDegree p
⊢ n < natTrailingDegree (mirror p)
[PROOFSTEP]
rwa [mirror_natTrailingDegree]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ eval 1 (mirror p) = eval 1 p
[PROOFSTEP]
simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (Finset.sum (Finset.range (natDegree p + 1)) fun x => coeff (mirror p) x) =
    Finset.sum (Finset.range (natDegree p + 1)) fun x => coeff p x
[PROOFSTEP]
refine' Finset.sum_bij_ne_zero _ _ _ _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (natDegree p + 1) → coeff (mirror p) a ≠ 0 → ℕ
[PROOFSTEP]
exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ),
    a ∈ Finset.range (natDegree p + 1) →
      coeff (mirror p) a ≠ 0 → ↑(revAt (natDegree p + natTrailingDegree p)) a ∈ Finset.range (natDegree p + 1)
[PROOFSTEP]
intro n hn hp
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff (mirror p) n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ∈ Finset.range (natDegree p + 1)
[PROOFSTEP]
rw [Finset.mem_range_succ_iff] at *
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff (mirror p) n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ≤ natDegree p
[PROOFSTEP]
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff (mirror p) n ≠ 0
⊢ natDegree p + natTrailingDegree p - n ≤ natDegree p
[PROOFSTEP]
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff (mirror p) n ≠ 0
⊢ natTrailingDegree (mirror p) ≤ n
[PROOFSTEP]
exact natTrailingDegree_le_of_ne_zero hp
[GOAL]
case refine'_3
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a₁ a₂ : ℕ),
    a₁ ∈ Finset.range (natDegree p + 1) →
      coeff (mirror p) a₁ ≠ 0 →
        a₂ ∈ Finset.range (natDegree p + 1) →
          coeff (mirror p) a₂ ≠ 0 →
            ↑(revAt (natDegree p + natTrailingDegree p)) a₁ = ↑(revAt (natDegree p + natTrailingDegree p)) a₂ → a₁ = a₂
[PROOFSTEP]
exact fun n₁ n₂ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n₁ n₂ : ℕ
x✝³ : n₁ ∈ Finset.range (natDegree p + 1)
x✝² : coeff (mirror p) n₁ ≠ 0
x✝¹ : n₂ ∈ Finset.range (natDegree p + 1)
x✝ : coeff (mirror p) n₂ ≠ 0
h : ↑(revAt (natDegree p + natTrailingDegree p)) n₁ = ↑(revAt (natDegree p + natTrailingDegree p)) n₂
⊢ n₁ = n₂
[PROOFSTEP]
rw [← @revAt_invol _ n₁, h, revAt_invol]
[GOAL]
case refine'_4
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (b : ℕ),
    b ∈ Finset.range (natDegree p + 1) → coeff p b ≠ 0 → ∃ a h₁ h₂, b = ↑(revAt (natDegree p + natTrailingDegree p)) a
[PROOFSTEP]
intro n hn hp
[GOAL]
case refine'_4
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ ∃ a h₁ h₂, n = ↑(revAt (natDegree p + natTrailingDegree p)) a
[PROOFSTEP]
use revAt (p.natDegree + p.natTrailingDegree) n
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ ∃ h₁ h₂, n = ↑(revAt (natDegree p + natTrailingDegree p)) (↑(revAt (natDegree p + natTrailingDegree p)) n)
[PROOFSTEP]
refine' ⟨_, _, revAt_invol.symm⟩
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ∈ Finset.range (natDegree p + 1)
[PROOFSTEP]
rw [Finset.mem_range_succ_iff] at *
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff p n ≠ 0
⊢ ↑(revAt (natDegree p + natTrailingDegree p)) n ≤ natDegree p
[PROOFSTEP]
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff p n ≠ 0
⊢ natDegree p + natTrailingDegree p - n ≤ natDegree p
[PROOFSTEP]
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]
[GOAL]
case h.refine'_1
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≤ natDegree p
hp : coeff p n ≠ 0
⊢ natTrailingDegree p ≤ n
[PROOFSTEP]
exact natTrailingDegree_le_of_ne_zero hp
[GOAL]
case h.refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ coeff (mirror p) (↑(revAt (natDegree p + natTrailingDegree p)) n) ≠ 0
[PROOFSTEP]
change p.mirror.coeff _ ≠ 0
[GOAL]
case h.refine'_2
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (natDegree p + 1)
hp : coeff p n ≠ 0
⊢ coeff (mirror p) (↑(revAt (natDegree p + natTrailingDegree p)) n) ≠ 0
[PROOFSTEP]
rwa [coeff_mirror, revAt_invol]
[GOAL]
case refine'_5
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ),
    a ∈ Finset.range (natDegree p + 1) →
      coeff (mirror p) a ≠ 0 → coeff (mirror p) a = coeff p (↑(revAt (natDegree p + natTrailingDegree p)) a)
[PROOFSTEP]
exact fun n _ _ => p.coeff_mirror n
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ coeff (mirror (mirror p)) n = coeff p n
[PROOFSTEP]
rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
h : mirror p = 0
⊢ p = 0
[PROOFSTEP]
rw [← p.mirror_mirror, h, mirror_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
h : p = 0
⊢ mirror p = 0
[PROOFSTEP]
rw [h, mirror_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ trailingCoeff (mirror p) = leadingCoeff p
[PROOFSTEP]
rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror, revAt_le (Nat.le_add_left _ _),
  add_tsub_cancel_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ leadingCoeff (mirror p) = trailingCoeff p
[PROOFSTEP]
rw [← p.mirror_mirror, mirror_trailingCoeff, p.mirror_mirror]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ coeff (p * mirror p) (natDegree p + natTrailingDegree p) = sum p fun n x => x ^ 2
[PROOFSTEP]
rw [coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk]
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ (Finset.sum (Finset.range (Nat.succ (natDegree p + natTrailingDegree p))) fun k =>
      coeff p (k, natDegree p + natTrailingDegree p - k).fst *
        coeff (mirror p) (k, natDegree p + natTrailingDegree p - k).snd) =
    sum p fun n x => x ^ 2
[PROOFSTEP]
refine'
  (Finset.sum_congr rfl fun n hn => _).trans
    (p.sum_eq_of_subset (fun _ => (· ^ 2)) (fun _ => zero_pow zero_lt_two) fun n hn =>
        Finset.mem_range_succ_iff.mpr ((le_natDegree_of_mem_supp n hn).trans (Nat.le_add_right _ _))).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ Finset.range (Nat.succ (natDegree p + natTrailingDegree p))
⊢ coeff p (n, natDegree p + natTrailingDegree p - n).fst *
      coeff (mirror p) (n, natDegree p + natTrailingDegree p - n).snd =
    coeff p n ^ 2
[PROOFSTEP]
rw [coeff_mirror, ← revAt_le (Finset.mem_range_succ_iff.mp hn), revAt_invol, ← sq]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ natDegree (p * mirror p) = 2 * natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natDegree (p * mirror p) = 2 * natDegree p
[PROOFSTEP]
rw [hp, zero_mul, natDegree_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natDegree (p * mirror p) = 2 * natDegree p
[PROOFSTEP]
rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
[PROOFSTEP]
rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
[PROOFSTEP]
rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
[GOAL]
R : Type u_1
inst✝ : Ring R
p q : R[X]
⊢ mirror (-p) = -mirror p
[PROOFSTEP]
rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
rw [hp, zero_mul, mirror_zero, zero_mul]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
rw [hq, mul_zero, mirror_zero, mul_zero]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ mirror (p * q) = mirror p * mirror q
[PROOFSTEP]
rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * reverse q * (X ^ natTrailingDegree p * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * reverse q * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
repeat' rw [mul_assoc]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * reverse q * X ^ natTrailingDegree q) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ reverse p * (X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)) =
    reverse p * X ^ natTrailingDegree p * (reverse q * X ^ natTrailingDegree q)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ mirror (a • p) = a • mirror p
[PROOFSTEP]
rw [← C_mul', ← C_mul', mirror_mul_of_domain, mirror_C]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ Irreducible f
[PROOFSTEP]
constructor
[GOAL]
case not_unit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ¬IsUnit f
[PROOFSTEP]
exact h1
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
⊢ ∀ (a b : R[X]), f = a * b → IsUnit a ∨ IsUnit b
[PROOFSTEP]
intro g h fgh
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
let k := g * h.mirror
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have key : f * f.mirror = k * k.mirror := by
  rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h, mul_comm g.mirror,
    mul_assoc, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
⊢ f * mirror f = k * mirror k
[PROOFSTEP]
rw [fgh, mirror_mul_of_domain, mirror_mul_of_domain, mirror_mirror, mul_assoc, mul_comm h, mul_comm g.mirror, mul_assoc,
  ← mul_assoc]
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have g_dvd_f : g ∣ f := by
  rw [fgh]
  exact dvd_mul_right g h
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ f
[PROOFSTEP]
rw [fgh]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
⊢ g ∣ g * h
[PROOFSTEP]
exact dvd_mul_right g h
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have h_dvd_f : h ∣ f := by
  rw [fgh]
  exact dvd_mul_left h g
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ f
[PROOFSTEP]
rw [fgh]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
⊢ h ∣ g * h
[PROOFSTEP]
exact dvd_mul_left h g
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have h_dvd_k_rev : h ∣ k.mirror := by
  rw [mirror_mul_of_domain, mirror_mirror]
  exact dvd_mul_left h g.mirror
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror k
[PROOFSTEP]
rw [mirror_mul_of_domain, mirror_mirror]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ mirror g * h
[PROOFSTEP]
exact dvd_mul_left h g.mirror
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
have hk := h2 k key
[GOAL]
case isUnit_or_isUnit'
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
rcases hk with (hk | hk | hk | hk)
[GOAL]
case isUnit_or_isUnit'.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inr (h3 h h_dvd_f (by rwa [← hk]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = f
⊢ h ∣ mirror f
[PROOFSTEP]
rwa [← hk]
[GOAL]
case isUnit_or_isUnit'.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inr (h3 h h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -f
⊢ h ∣ mirror f
[PROOFSTEP]
rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]
[GOAL]
case isUnit_or_isUnit'.inr.inr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inl (h3 g g_dvd_f (by rwa [← hk]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = mirror f
⊢ g ∣ mirror f
[PROOFSTEP]
rwa [← hk]
[GOAL]
case isUnit_or_isUnit'.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ IsUnit g ∨ IsUnit h
[PROOFSTEP]
exact Or.inl (h3 g g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * mirror f = k * mirror k → k = f ∨ k = -f ∨ k = mirror f ∨ k = -mirror f
h3 : ∀ (g : R[X]), g ∣ f → g ∣ mirror f → IsUnit g
g h : R[X]
fgh : f = g * h
k : R[X] := g * mirror h
key : f * mirror f = k * mirror k
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ mirror k
hk : k = -mirror f
⊢ g ∣ mirror f
[PROOFSTEP]
rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]


[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ LeftInverse (Polynomial.eval₂ C (X PUnit.unit)) (eval₂ Polynomial.C fun x => Polynomial.X)
[PROOFSTEP]
let f : R[X] →+* MvPolynomial PUnit R := Polynomial.eval₂RingHom MvPolynomial.C (X PUnit.unit)
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
⊢ LeftInverse (Polynomial.eval₂ C (X PUnit.unit)) (eval₂ Polynomial.C fun x => Polynomial.X)
[PROOFSTEP]
let g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ LeftInverse (Polynomial.eval₂ C (X PUnit.unit)) (eval₂ Polynomial.C fun x => Polynomial.X)
[PROOFSTEP]
show ∀ p, f.comp g p = p
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ ∀ (p : MvPolynomial PUnit R), ↑(RingHom.comp f g) p = p
[PROOFSTEP]
apply is_id
[GOAL]
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ RingHom.comp (RingHom.comp f g) C = C
[PROOFSTEP]
ext a
[GOAL]
case hC.a.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
a : R
m✝ : PUnit →₀ ℕ
⊢ coeff m✝ (↑(RingHom.comp (RingHom.comp f g) C) a) = coeff m✝ (↑C a)
[PROOFSTEP]
dsimp
[GOAL]
case hC.a.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
a : R
m✝ : PUnit →₀ ℕ
⊢ coeff m✝ (Polynomial.eval₂ C (X PUnit.unit) (eval₂ Polynomial.C (fun x => Polynomial.X) (↑C a))) = coeff m✝ (↑C a)
[PROOFSTEP]
rw [eval₂_C, Polynomial.eval₂_C]
[GOAL]
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ ∀ (n : PUnit), ↑(RingHom.comp f g) (X n) = X n
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case hX.unit
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ ↑(RingHom.comp f g) (X PUnit.unit) = X PUnit.unit
[PROOFSTEP]
dsimp
[GOAL]
case hX.unit
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
f : R[X] →+* MvPolynomial PUnit R := eval₂RingHom C (X PUnit.unit)
g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun x => Polynomial.X
⊢ Polynomial.eval₂ C (X PUnit.unit) (eval₂ Polynomial.C (fun x => Polynomial.X) (X PUnit.unit)) = X PUnit.unit
[PROOFSTEP]
rw [eval₂_X, Polynomial.eval₂_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (↑Polynomial.C a)) = ↑Polynomial.C a
[PROOFSTEP]
rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) p) = p
hq : eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) q) = q
⊢ eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (p + q)) = p + q
[PROOFSTEP]
rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x => Polynomial.X) (Polynomial.eval₂ C (X PUnit.unit) (↑Polynomial.C n * Polynomial.X ^ p)) =
    ↑Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x => Polynomial.X)
      (Polynomial.eval₂ C (X PUnit.unit) (↑Polynomial.C n * Polynomial.X ^ (p + 1))) =
    ↑Polynomial.C n * Polynomial.X ^ (p + 1)
[PROOFSTEP]
rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C, eval₂_mul, eval₂_C, eval₂_pow,
  eval₂_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : CommSemiring S₂
inst✝ : CommSemiring S₃
e : S₁ ≃+* S₂
f : S₂ ≃+* S₃
p : MvPolynomial σ S₁
⊢ ↑(RingEquiv.trans (mapEquiv σ e) (mapEquiv σ f)) p = ↑(mapEquiv σ (RingEquiv.trans e f)) p
[PROOFSTEP]
simp only [RingEquiv.coe_trans, comp_apply, mapEquiv_apply, RingEquiv.coe_ringHom_trans, map_map]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
⊢ AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f) = mapAlgEquiv σ (AlgEquiv.trans e f)
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(AlgEquiv.trans (mapAlgEquiv σ e) (mapAlgEquiv σ f)) a✝) =
    coeff m✝ (↑(mapAlgEquiv σ (AlgEquiv.trans e f)) a✝)
[PROOFSTEP]
simp only [AlgEquiv.trans_apply, mapAlgEquiv_apply, map_map]
[GOAL]
case h.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e✝ : ℕ
s : σ →₀ ℕ
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (↑(map (RingHom.comp ↑f ↑e)) a✝) = coeff m✝ (↑(map ↑(AlgEquiv.trans e f)) a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
⊢ AlgHom.comp (aeval fun a => IsEmpty.elim he a) (Algebra.ofId R (MvPolynomial σ R)) = AlgHom.id R R
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
x✝ : R
⊢ ↑(AlgHom.comp (aeval fun a => IsEmpty.elim he a) (Algebra.ofId R (MvPolynomial σ R))) x✝ = ↑(AlgHom.id R R) x✝
[PROOFSTEP]
simp [Algebra.ofId_apply, algebraMap_eq]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
⊢ AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun a => IsEmpty.elim he a) = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext i m
[GOAL]
case hf.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
he : IsEmpty σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (↑(AlgHom.comp (Algebra.ofId R (MvPolynomial σ R)) (aeval fun a => IsEmpty.elim he a)) (X i)) =
    coeff m (↑(AlgHom.id R (MvPolynomial σ R)) (X i))
[PROOFSTEP]
exact IsEmpty.elim' he i
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)
[PROOFSTEP]
apply mvPolynomialEquivMvPolynomial R (Sum S₁ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
[GOAL]
case hfgC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C = C
[PROOFSTEP]
refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)
[GOAL]
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C = RingHom.comp C C
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C = RingHom.comp C C
[PROOFSTEP]
case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C = RingHom.comp C C
[PROOFSTEP]
ext1
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) C) x✝ = ↑(RingHom.comp C C) x✝
[PROOFSTEP]
simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
[GOAL]
case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₂), ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n) = ↑C (X n)
[PROOFSTEP]
intro
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : S₂
⊢ ↑(RingHom.comp (RingHom.comp (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)) C) (X n✝) = ↑C (X n✝)
[PROOFSTEP]
simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
[GOAL]
case hfgX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₁), ↑(sumToIter R S₁ S₂) (↑(iterToSum R S₁ S₂) (X n)) = X n
[PROOFSTEP]
simp [iterToSum_X, sumToIter_Xl]
[GOAL]
case hgfC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C = C
[PROOFSTEP]
ext1
[GOAL]
case hgfC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (iterToSum R S₁ S₂) (sumToIter R S₁ S₂)) C) x✝ = ↑C x✝
[PROOFSTEP]
simp only [RingHom.comp_apply, sumToIter_C, iterToSum_C_C]
[GOAL]
case hgfX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∀ (n : S₁ ⊕ S₂), ↑(iterToSum R S₁ S₂) (↑(sumToIter R S₁ S₂) (X n)) = X n
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case hgfX.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₁
⊢ ↑(iterToSum R S₁ S₂) (↑(sumToIter R S₁ S₂) (X (Sum.inl val✝))) = X (Sum.inl val✝)
[PROOFSTEP]
simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]
[GOAL]
case hgfX.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₂
⊢ ↑(iterToSum R S₁ S₂) (↑(sumToIter R S₁ S₂) (X (Sum.inr val✝))) = X (Sum.inr val✝)
[PROOFSTEP]
simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
⊢ ∀ (r : R),
    Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
      ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
intro r
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
    ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) : _) := by rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
⊢ ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
A : ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
    ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
have B : algebraMap R (MvPolynomial (Sum S₁ S₂) R) r = C r := by rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
A : ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
⊢ ↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r = ↑C r
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
src✝ : MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := sumRingEquiv R S₁ S₂
r : R
A : ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r = ↑C (↑C r)
B : ↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r = ↑C r
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (MvPolynomial (S₁ ⊕ S₂) R)) r) =
    ↑(algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R))) r
[PROOFSTEP]
simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe_apply, Equiv.coe_fn_mk, B, sumToIter_C, A]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s))
      (Polynomial.aevalTower (rename Option.some) (X none)) =
    AlgHom.id R (MvPolynomial S₁ R)[X]
[PROOFSTEP]
ext : 2
[GOAL]
case h₁.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
⊢ ↑(AlgHom.comp
          (AlgHom.comp (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s))
            (Polynomial.aevalTower (rename Option.some) (X none)))
          (IsScalarTower.toAlgHom R (MvPolynomial S₁ R) (MvPolynomial S₁ R)[X]))
      (X i✝) =
    ↑(AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R)[X])
          (IsScalarTower.toAlgHom R (MvPolynomial S₁ R) (MvPolynomial S₁ R)[X]))
      (X i✝)
[PROOFSTEP]
simp [← Polynomial.C_eq_algebraMap]
[GOAL]
case h₂.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n✝ : ℕ
⊢ Polynomial.coeff
      (↑(AlgHom.comp (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s))
            (Polynomial.aevalTower (rename Option.some) (X none)))
        Polynomial.X)
      n✝ =
    Polynomial.coeff (↑(AlgHom.id R (MvPolynomial S₁ R)[X]) Polynomial.X) n✝
[PROOFSTEP]
simp [← Polynomial.C_eq_algebraMap]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
      (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)) =
    AlgHom.id R (MvPolynomial (Option S₁) R)
[PROOFSTEP]
ext i : 2
[GOAL]
case hf.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)))
        (X i)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))
[PROOFSTEP]
cases i
[GOAL]
case hf.a.none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)))
        (X none)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))
[PROOFSTEP]
simp
[GOAL]
case hf.a.some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
val✝ : S₁
⊢ coeff m✝
      (↑(AlgHom.comp (Polynomial.aevalTower (rename Option.some) (X none))
            (aeval fun o => Option.elim o Polynomial.X fun s => ↑Polynomial.C (X s)))
        (X (Option.some val✝))) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (aeval fun o => Option.elim o (↑C Polynomial.X) X)
      (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)) =
    AlgHom.id R (MvPolynomial S₁ R[X])
[PROOFSTEP]
ext : 2
[GOAL]
case h₁.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ↑(AlgHom.comp
          (AlgHom.comp (aeval fun o => Option.elim o (↑C Polynomial.X) X)
            (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)))
          (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X =
    ↑(AlgHom.comp (AlgHom.id R (MvPolynomial S₁ R[X])) (IsScalarTower.toAlgHom R R[X] (MvPolynomial S₁ R[X])))
      Polynomial.X
[PROOFSTEP]
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp, IsScalarTower.coe_toAlgHom',
  comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X, Option.elim', aevalTower_X, AlgHom.coe_id, id.def,
  eq_self_iff_true, imp_true_iff]
[GOAL]
case h₂.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i✝ : S₁
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (aeval fun o => Option.elim o (↑C Polynomial.X) X)
            (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i)))
        (X i✝)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial S₁ R[X])) (X i✝))
[PROOFSTEP]
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp, IsScalarTower.coe_toAlgHom',
  comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X, Option.elim', aevalTower_X, AlgHom.coe_id, id.def,
  eq_self_iff_true, imp_true_iff]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ AlgHom.comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
      (aeval fun o => Option.elim o (↑C Polynomial.X) X) =
    AlgHom.id R (MvPolynomial (Option S₁) R)
[PROOFSTEP]
ext ⟨i⟩ : 2
[GOAL]
case hf.none.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
            (aeval fun o => Option.elim o (↑C Polynomial.X) X))
        (X none)) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))
[PROOFSTEP]
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C, Polynomial.aeval_X, AlgHom.coe_id, id.def,
  aevalTower_X]
[GOAL]
case hf.some.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
val✝ : S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (↑(AlgHom.comp (aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
            (aeval fun o => Option.elim o (↑C Polynomial.X) X))
        (X (Option.some val✝))) =
    coeff m✝ (↑(AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))
[PROOFSTEP]
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C, Polynomial.aeval_X, AlgHom.coe_id, id.def,
  aevalTower_X]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) =
    eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i
[PROOFSTEP]
ext i : 2
[GOAL]
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ↑(RingHom.comp (↑(finSuccEquiv R n)) C) i =
    ↑(RingHom.comp
          (eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) C)
      i
[PROOFSTEP]
simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe, coe_eval₂Hom, comp_apply,
  renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]
[GOAL]
case hC.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ↑(algebraMap R (MvPolynomial (Fin n) R)[X]) i = ↑Polynomial.C (↑C i)
[PROOFSTEP]
rfl
[GOAL]
case hX.a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ Polynomial.coeff (↑↑(finSuccEquiv R n) (X i)) n✝ =
    Polynomial.coeff
      (↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) (X i))
      n✝
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case hX.a.refine'_1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ Polynomial.coeff (↑↑(finSuccEquiv R n) (X 0)) n✝ =
    Polynomial.coeff
      (↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) (X 0))
      n✝
[PROOFSTEP]
simp [finSuccEquiv]
[GOAL]
case hX.a.refine'_2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ ∀ (i : Fin n),
    Polynomial.coeff (↑↑(finSuccEquiv R n) (X (Fin.succ i))) n✝ =
      Polynomial.coeff
        (↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i)
          (X (Fin.succ i)))
        n✝
[PROOFSTEP]
simp [finSuccEquiv]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
⊢ ↑(finSuccEquiv R n) p =
    ↑(eval₂Hom (RingHom.comp Polynomial.C C) fun i => Fin.cases Polynomial.X (fun k => ↑Polynomial.C (X k)) i) p
[PROOFSTEP]
rw [← finSuccEquiv_eq, RingHom.coe_coe]
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C) = C
[PROOFSTEP]
refine' RingHom.ext fun x => _
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C)) x = ↑C x
[PROOFSTEP]
rw [RingHom.comp_apply]
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑↑(AlgEquiv.symm (finSuccEquiv R n)) (↑(RingHom.comp Polynomial.C C) x) = ↑C x
[PROOFSTEP]
refine' (MvPolynomial.finSuccEquiv R n).injective (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) _)
[GOAL]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp Polynomial.C C) x = ↑(finSuccEquiv R n) (↑C x)
[PROOFSTEP]
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) (X 0) = Polynomial.X
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ ↑(finSuccEquiv R n) (X (Fin.succ j)) = ↑Polynomial.C (X j)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) f) i) = coeff (cons i m) f
[PROOFSTEP]
induction' f using MvPolynomial.induction_on' with j r p q hp hq generalizing i m
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
[PROOFSTEP]
swap
[GOAL]
case h2
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
p q : MvPolynomial (Fin (n + 1)) R
hp : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) p) i) = coeff (cons i m) p
hq : ∀ (m : Fin n →₀ ℕ) (i : ℕ), coeff m (Polynomial.coeff (↑(finSuccEquiv R n) q) i) = coeff (cons i m) q
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (p + q)) i) = coeff (cons i m) (p + q)
[PROOFSTEP]
simp only [(finSuccEquiv R n).map_add, Polynomial.coeff_add, coeff_add, hp, hq]
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (Polynomial.coeff (↑(finSuccEquiv R n) (↑(monomial j) r)) i) = coeff (cons i m) (↑(monomial j) r)
[PROOFSTEP]
simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, prod_pow, Polynomial.coeff_C_mul,
  coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero, Fin.cases_succ, ← map_prod, ← RingHom.map_pow,
  Function.comp_apply]
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (Polynomial.coeff (Polynomial.X ^ ↑j 0 * ↑Polynomial.C (∏ x : Fin n, X x ^ ↑j (Fin.succ x))) i) =
    if j = cons i m then r else 0
[PROOFSTEP]
rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]
[GOAL]
case h1
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = r * if j = cons i m then 1 else 0
[PROOFSTEP]
congr 1
[GOAL]
case h1.e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = if j = cons i m then 1 else 0
[PROOFSTEP]
obtain rfl | hjmi := eq_or_ne j (m.cons i)
[GOAL]
case h1.e_a.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (if i = ↑(cons i m) 0 then ∏ x : Fin n, X x ^ ↑(cons i m) (Fin.succ x) else 0) =
    if cons i m = cons i m then 1 else 0
[PROOFSTEP]
simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul, prod_pow] using coeff_monomial m m (1 : R)
[GOAL]
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = if j = cons i m then 1 else 0
[PROOFSTEP]
simp only [hjmi, if_false]
[GOAL]
case h1.e_a.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = 0
[PROOFSTEP]
obtain hij | rfl := ne_or_eq i (j 0)
[GOAL]
case h1.e_a.inr.inl
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i✝ : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
hij : i ≠ ↑j 0
⊢ coeff m (if i = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = 0
[PROOFSTEP]
simp only [hij, if_false, coeff_zero]
[GOAL]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ coeff m (if ↑j 0 = ↑j 0 then ∏ x : Fin n, X x ^ ↑j (Fin.succ x) else 0) = 0
[PROOFSTEP]
simp only [eq_self_iff_true, if_true]
[GOAL]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
[PROOFSTEP]
have hmj : m ≠ j.tail := by
  rintro rfl
  rw [cons_tail] at hjmi
  contradiction
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
⊢ m ≠ tail j
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (↑j 0) (tail j)
⊢ False
[PROOFSTEP]
rw [cons_tail] at hjmi
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case h1.e_a.inr.inr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
m✝ : Fin n →₀ ℕ
i : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (↑j 0) m
hmj : m ≠ tail j
⊢ coeff m (∏ x : Fin n, X x ^ ↑j (Fin.succ x)) = 0
[PROOFSTEP]
simpa only [monomial_eq, C_1, one_mul, prod_pow, Finsupp.tail_apply, if_neg hmj.symm] using
  coeff_monomial m j.tail (1 : R)
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
⊢ ↑(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) (↑(finSuccEquiv R n) f))
[PROOFSTEP]
let φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  { Polynomial.mapRingHom (eval s) with
    commutes' := fun r => by
      convert Polynomial.map_C (eval s)
      exact (eval_C _).symm }
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                  OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
    ↑(algebraMap R R[X]) r
[PROOFSTEP]
convert Polynomial.map_C (eval s)
[GOAL]
case h.e'_3.h.e'_6
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
src✝ : (MvPolynomial (Fin n) R)[X] →+* R[X] := mapRingHom (eval s)
r : R
⊢ r = ↑(eval s) (↑(algebraMap R (MvPolynomial (Fin n) R)) r)
[PROOFSTEP]
exact (eval_C _).symm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) (↑(finSuccEquiv R n) f))
[PROOFSTEP]
show aeval (Fin.cons y s : Fin (n + 1) → R) f = (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) f = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) f
[PROOFSTEP]
congr 2
[GOAL]
case e_a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ aeval (Fin.cons y s) = AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))
[PROOFSTEP]
apply MvPolynomial.algHom_ext
[GOAL]
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ∀ (i : Fin (n + 1)),
    ↑(aeval (Fin.cons y s)) (X i) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X i)
[PROOFSTEP]
rw [Fin.forall_fin_succ]
[GOAL]
case e_a.hf
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let src := mapRingHom (eval s);
  {
    toRingHom :=
      { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
        map_add' :=
          (_ :
            ∀ (x y : (MvPolynomial (Fin n) R)[X]),
              OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) },
    commutes' :=
      (_ :
        ∀ (r : R),
          OneHom.toFun
              (↑↑{ toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑src) 0 = 0),
                    map_add' :=
                      (_ :
                        ∀ (x y : (MvPolynomial (Fin n) R)[X]),
                          OneHom.toFun (↑↑src) (x + y) = OneHom.toFun (↑↑src) x + OneHom.toFun (↑↑src) y) })
              (↑(algebraMap R (MvPolynomial (Fin n) R)[X]) r) =
            ↑(algebraMap R R[X]) r) }
⊢ ↑(aeval (Fin.cons y s)) (X 0) = ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      ↑(aeval (Fin.cons y s)) (X (Fin.succ i)) =
        ↑(AlgHom.comp (Polynomial.aeval y) (AlgHom.comp φ ↑(finSuccEquiv R n))) (X (Fin.succ i))
[PROOFSTEP]
simp only [aeval_X, Fin.cons_zero, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
  Polynomial.map_C, AlgHom.coe_mk, RingHom.toFun_eq_coe, Polynomial.coe_mapRingHom, comp_apply, finSuccEquiv_apply,
  eval₂Hom_X', Fin.cases_zero, Polynomial.map_X, Polynomial.eval_X, Fin.cons_succ, Fin.cases_succ, eval_X,
  Polynomial.eval_C, RingHom.coe_mk, MonoidHom.coe_coe, AlgHom.coe_coe, implies_true, and_self,
  RingHom.toMonoidHom_eq_coe]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
s' : Fin n → R
f : (MvPolynomial (Fin n) R)[X]
i : ℕ
⊢ Polynomial.coeff (Polynomial.map (eval s') f) i = ↑(eval s') (Polynomial.coeff f i)
[PROOFSTEP]
simp only [Polynomial.coeff_map]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ↔ cons i m ∈ support f
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) → cons i m ∈ support f
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
⊢ cons i m ∈ support f
[PROOFSTEP]
simpa [← finSuccEquiv_coeff_coeff] using h
[GOAL]
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ support f → m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ support f
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
[PROOFSTEP]
simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ Polynomial.support (↑(finSuccEquiv R n) f) = Finset.image (fun m => ↑m 0) (support f)
[PROOFSTEP]
ext i
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ Polynomial.support (↑(finSuccEquiv R n) f) ↔ i ∈ Finset.image (fun m => ↑m 0) (support f)
[PROOFSTEP]
rw [Polynomial.mem_support_iff, Finset.mem_image, nonzero_iff_exists]
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) ↔ ∃ a, a ∈ support f ∧ ↑a 0 = i
[PROOFSTEP]
constructor
[GOAL]
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) → ∃ a, a ∈ support f ∧ ↑a 0 = i
[PROOFSTEP]
rintro ⟨m, hm⟩
[GOAL]
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ ∃ a, a ∈ support f ∧ ↑a 0 = i
[PROOFSTEP]
refine' ⟨cons i m, _, cons_zero _ _⟩
[GOAL]
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ cons i m ∈ support f
[PROOFSTEP]
rw [← support_coeff_finSuccEquiv]
[GOAL]
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
[PROOFSTEP]
simpa using hm
[GOAL]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, a ∈ support f ∧ ↑a 0 = i) → ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0
[PROOFSTEP]
rintro ⟨m, h, rfl⟩
[GOAL]
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) a ≠ 0
[PROOFSTEP]
refine' ⟨tail m, _⟩
[GOAL]
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) (tail m) ≠ 0
[PROOFSTEP]
rwa [← coeff, ← mem_support_iff, support_coeff_finSuccEquiv, cons_tail]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ Finset.image (cons i) (support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)) =
    Finset.filter (fun m => ↑m 0 = i) (support f)
[PROOFSTEP]
ext m
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ m ∈ Finset.image (cons i) (support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)) ↔
    m ∈ Finset.filter (fun m => ↑m 0 = i) (support f)
[PROOFSTEP]
rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m) ↔ coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
conv_lhs =>
  congr
  ext
  rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
  congr
  ext
  rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
  congr
  ext
  rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| ∃ a, a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
congr
[GOAL]
case p
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| fun a => a ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i a = m
[PROOFSTEP]
ext
[GOAL]
case p.h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| x✝ ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ∧ cons i x✝ = m
[PROOFSTEP]
rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne.def]
[GOAL]
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
constructor
[GOAL]
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
rintro ⟨m', ⟨h, hm'⟩⟩
[GOAL]
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i
[PROOFSTEP]
simp only [← hm']
[GOAL]
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff (cons i m') f ≠ 0 ∧ ↑(cons i m') 0 = i
[PROOFSTEP]
exact ⟨h, by rw [cons_zero]⟩
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ ↑(cons i m') 0 = i
[PROOFSTEP]
rw [cons_zero]
[GOAL]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
[PROOFSTEP]
intro h
[GOAL]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
[PROOFSTEP]
use tail m
[GOAL]
case h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff (cons i (tail m)) f = 0 ∧ cons i (tail m) = m
[PROOFSTEP]
rw [← h.2, cons_tail]
[GOAL]
case h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff m f = 0 ∧ m = m
[PROOFSTEP]
simp [h.1]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ Finset.Nonempty (Polynomial.support (↑(finSuccEquiv R n) f))
[PROOFSTEP]
simp only [Finset.nonempty_iff_ne_empty, Ne, Polynomial.support_eq_empty]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ¬↑(finSuccEquiv R n) f = 0
[PROOFSTEP]
refine fun c => h ?_
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
⊢ f = 0
[PROOFSTEP]
let ii := (finSuccEquiv R n).symm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = 0
[PROOFSTEP]
calc
  f = ii (finSuccEquiv R n f) := by simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
  _ = ii 0 := by rw [c]
  _ = 0 := by simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = ↑ii (↑(finSuccEquiv R n) f)
[PROOFSTEP]
simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ ↑ii (↑(finSuccEquiv R n) f) = ↑ii 0
[PROOFSTEP]
rw [c]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ ↑ii 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h₂ : WithBot.some = Nat.cast := rfl
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
h₂ : WithBot.some = Nat.cast
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
  rw [degreeOf_eq_sup, finSuccEquiv_support f, Finset.sup_image, h₀]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.1446258} {β : Type ?u.1446261} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
h₂ : WithBot.some = Nat.cast
⊢ (Finset.sup (Polynomial.support (↑(finSuccEquiv R n) f)) fun x => x) = degreeOf 0 f
[PROOFSTEP]
rw [degreeOf_eq_sup, finSuccEquiv_support f, Finset.sup_image, h₀]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α β : Type} (f : α → β), (fun x => x) ∘ f = f
h₁ : ∀ {α : Type ?u.1446323} {β : Type ?u.1446326} (f : α → β), (f ∘ fun x => x) = f
h₂ : WithBot.some = Nat.cast
h' : (Finset.sup (Polynomial.support (↑(finSuccEquiv R n) f)) fun x => x) = degreeOf 0 f
⊢ degree (↑(finSuccEquiv R n) f) = ↑(degreeOf 0 f)
[PROOFSTEP]
rw [Polynomial.degree, ← h', ← h₂, Finset.coe_sup_of_nonempty (support_finSuccEquiv_nonempty h), Finset.max_eq_sup_coe,
  h₁]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
[PROOFSTEP]
by_cases c : f = 0
[GOAL]
case pos
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
[PROOFSTEP]
rw [c, (finSuccEquiv R n).map_zero, Polynomial.natDegree_zero, degreeOf_zero]
[GOAL]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ natDegree (↑(finSuccEquiv R n) f) = degreeOf 0 f
[PROOFSTEP]
rw [Polynomial.natDegree, degree_finSuccEquiv (by simpa only [Ne.def])]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ f ≠ 0
[PROOFSTEP]
simpa only [Ne.def]
[GOAL]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ WithBot.unbot' 0 ↑(degreeOf 0 f) = degreeOf 0 f
[PROOFSTEP]
erw [WithBot.unbot'_coe]
[GOAL]
case neg
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ ↑(degreeOf 0 f) = degreeOf 0 f
[PROOFSTEP]
simp
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf j (Polynomial.coeff (↑(finSuccEquiv R n) p) i) ≤ degreeOf (Fin.succ j) p
[PROOFSTEP]
rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ (b : Fin n →₀ ℕ),
    b ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i) → ↑b j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑m j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
[PROOFSTEP]
rw [← Finsupp.cons_succ j i m]
[GOAL]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑(cons i m) (Fin.succ j) ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
[PROOFSTEP]
exact Finset.le_sup (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j)) (support_coeff_finSuccEquiv.1 hm)