awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
⊢ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).degree

Tactic:
exact (degree_sum_le s _).trans <| Finset.sup_le fun i hi ↦ (degree_smul_le _ _).trans <|
      degree_map_le.trans <| Finset.le_sup (f := fun i ↦ (f i).degree) hi

Premises used: Polynomial.degree_map_le, Polynomial.degree_sum_le, Finset.sup_le, Polynomial.degree_smul_le, Polynomial.map, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
a : ∀ b ∈ s, (f b).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (s.sup fun (i : ι) ↦ (f i).degree) ≤
    degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
pos :
  ∀ (hf : f i = 0),
    (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
neg :
  ∀ (hf : ¬f i = 0),
    (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
by_cases hf : f i = 0
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : f i = 0
⊢ (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
neg :
  (↑(f i).natDegree : WithBot ℕ) ≤
    degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (f i).degree ≤ degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
rw [degree_eq_natDegree hf]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
neg :
  Ne.{u_1 + 1} (α := A) (coeff (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) (f i).natDegree) 0
⊢ (↑(f i).natDegree : WithBot ℕ) ≤
    degree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
apply le_degree_of_ne_zero

Premises used: Polynomial.le_degree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
neg :
  Ne.{u_1 + 1} (α := A) (∑ b ∈ s, (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree) 0
⊢ Ne.{u_1 + 1} (α := A) (coeff (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) (f i).natDegree) 0

Tactic:
rw [finsetSum_coeff]

Premises used: Polynomial.finsetSum_coeff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
h₁ : ∀ (x : ι), (HSMul.hSMul (β := A[X]) (v x) (map (algebraMap R A) (f x))).coeff (f i).natDegree
| fun (b : ι) ↦ (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
x : ι
h₁ : (f x).coeff (f i).natDegree • v x
| (HSMul.hSMul (β := A[X]) (v x) (map (algebraMap R A) (f x))).coeff (f i).natDegree

Tactic:
rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]

Premises used: Polynomial.coeff_map, Polynomial.coeff_smul, mul_comm, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
h₁ : ∀ (x : ι), (f x).coeff (f i).natDegree • v x
| fun (b : ι) ↦ (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree

Tactic:
ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]

Premises used: Polynomial.coeff_map, Polynomial.coeff_smul, mul_comm, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
neg : Ne.{u_1 + 1} (α := A) (∑ x ∈ s, (f x).coeff (f i).natDegree • v x) 0
⊢ Ne.{u_1 + 1} (α := A) (∑ b ∈ s, (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree) 0

Tactic:
conv in (fun _ ↦ _) =>
      ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]

Premises used: Polynomial.coeff_map, Polynomial.coeff_smul, mul_comm, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
H : Eq.{u_1 + 1} (α := A) (∑ x ∈ s, (f x).coeff (f i).natDegree • v x) 0
⊢ False

Tactic:
hf (leadingCoeff_eq_zero.mp (linearIndepOn_finset_iff.mp h _ H i hi))

Premises used: linearIndepOn_finset_iff, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
H : Eq.{u_1 + 1} (α := A) (∑ x ∈ s, (f x).coeff (f i).natDegree • v x) 0
⊢ False

Tactic:
exact hf (leadingCoeff_eq_zero.mp (linearIndepOn_finset_iff.mp h _ H i hi))

Premises used: linearIndepOn_finset_iff, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
a :
  natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).natDegree
a₁ :
  (s.sup fun (i : ι) ↦ (f i).natDegree) ≤
    natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) =
    s.sup fun (i : ι) ↦ (f i).natDegree

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
⊢ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).natDegree

Tactic:
natDegree_sum_le_of_forall_le _ _ fun i hi ↦ (natDegree_smul_le _ _).trans <|
      natDegree_map_le.trans <| Finset.le_sup (f := fun i ↦ (f i).natDegree) hi

Premises used: Algebra.algebraMap, Polynomial.natDegree_sum_le_of_forall_le, Polynomial.natDegree_smul_le, Polynomial.natDegree_map_le, Polynomial.map, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
⊢ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).natDegree

Tactic:
exact natDegree_sum_le_of_forall_le _ _ fun i hi ↦ (natDegree_smul_le _ _).trans <|
      natDegree_map_le.trans <| Finset.le_sup (f := fun i ↦ (f i).natDegree) hi

Premises used: Polynomial.natDegree_sum_le_of_forall_le, Polynomial.natDegree_smul_le, Polynomial.natDegree_map_le, Polynomial.map, LE.le.trans, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
a :
  ∀ b ∈ s,
    (f b).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (s.sup fun (i : ι) ↦ (f i).natDegree) ≤
    natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
pos :
  ∀ (hf : f i = 0),
    (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
neg :
  ∀ (hf : ¬f i = 0),
    (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
by_cases hf : f i = 0
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : f i = 0
⊢ (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
simp [hf]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
neg :
  Ne.{u_1 + 1} (α := A) (coeff (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) (f i).natDegree) 0
⊢ (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))

Tactic:
apply le_natDegree_of_ne_zero

Premises used: Polynomial.le_natDegree_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
rw :
  (Multiset.map
        (Function.comp (β := R[X]) natDegree fun (x : R) ↦
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        s).sum =
    s.card
h :
  ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s) f →
      f.Monic
⊢ natDegree (R := R)
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s)) =
    s.card

Tactic:
rw [natDegree_multiset_prod_of_monic, Multiset.map_map]

Premises used: Multiset.map_map, Polynomial.natDegree_multiset_prod_of_monic
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
⊢ (Multiset.map
        (Function.comp (β := R[X]) natDegree fun (x : R) ↦
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        s).sum =
    s.card

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
⊢ ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s) f →
      f.Monic

Tactic:
Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a

Premises used: Iff.mpr, Polynomial.monic_X_sub_C, Multiset.forall_mem_map_iff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
⊢ ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s) f →
      f.Monic

Tactic:
exact Multiset.forall_mem_map_iff.2 fun a _ => monic_X_sub_C a

Premises used: Iff.mpr, Polynomial.monic_X_sub_C, Multiset.forall_mem_map_iff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
rw :
  natDegree.{u} (R := R)
      (prod
        (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
    #s
rw₁ :
  natDegree (R := R)
      (prod
        (Multiset.map ((fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∘ f)
          s.val)) =
    #s
rw₂ :
  natDegree (R := R)
      (prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          (Multiset.map f s.val))) =
    #s
rw₃ : (Multiset.map f s.val).card = #s
rw₄ : s.val.card = #s
rw₅ rw₆ : s.val.card = s.val.card
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s

Tactic:
rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]

Premises used: Polynomial.C, HSub.hSub, Finset.prod, Polynomial.natDegree_multiset_prod_X_sub_C_eq_card, Function.comp_def, Finset.card, Multiset.map_map, Polynomial.X, DFunLike.coe, Multiset.card_map
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
l : List R[X]
⊢ l.prod.degree = (List.map degree l).sum

Tactic:
map_list_prod (@degreeMonoidHom R _ _ _) l

Premises used: Multiset.foldr, WithBot.some, Finset.fold, List.sum, map_list_prod, Polynomial.degree, Multiplicative, Finset.max, Finset.sup, Polynomial.degreeMonoidHom, WithBot.map₂, Multiset.fold, Option.map₂
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
h_1 : Nontrivial R
h₁ : Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
⊢ natDegree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).natDegree

Tactic:
apply natDegree_prod'

Premises used: Polynomial.natDegree_prod'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
h_1 : Nontrivial R
h₁ : ∀ a ∈ s, (f a).leadingCoeff ≠ 0
⊢ Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0

Tactic:
rw [prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
h_1 : Nontrivial R
x : ι
hx : x ∈ s
⊢ (f x).leadingCoeff ≠ 0

Tactic:
simp [h x hx]
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
h_1 : Nontrivial R
h₁ : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
rw [natDegree_multiset_prod']

Premises used: Polynomial.natDegree_multiset_prod'
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
h_1 : Nontrivial R
h₁ : ¬∃ a ∈ t, a = 0
⊢ Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0

Tactic:
simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]

Premises used: Multiset.mem_map, Multiset.prod_eq_zero_iff, Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h_1 : 0 ∉ t
h_2 : Nontrivial R
h : 0 ∈ t
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
inst_2 : Nontrivial R
⊢ t.prod.degree = Multiset.sum (Multiset.map (fun (f : R[X]) ↦ f.degree) t)

Tactic:
map_multiset_prod (@degreeMonoidHom R _ _ _) _

Premises used: Multiset.sum, Multiset.foldr, WithBot.some, Finset.fold, Polynomial.degree, map_multiset_prod, Multiplicative, Finset.max, Finset.sup, Polynomial.degreeMonoidHom, WithBot.map₂, Multiset.fold, Option.map₂
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
inst_2 : Nontrivial R
⊢ degree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).degree

Tactic:
map_prod (@degreeMonoidHom R _ _ _) _ _

Premises used: Multiset.sum, Multiset.foldr, WithBot.some, Finset.fold, Polynomial.degree, map_prod, Multiplicative, Finset.max, Finset.sup, Polynomial.degreeMonoidHom, Finset.sum, WithBot.map₂, Multiset.fold, Option.map₂
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
rw :
  Eq (α := R) (prod (Multiset.map (⇑leadingCoeffHom : (a : R[X]) → R) t))
    (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t))
⊢ t.prod.leadingCoeff = prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)

Tactic:
rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]

Premises used: Polynomial.leadingCoeffHom_apply, MonoidHom.map_multiset_prod
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
⊢ Eq (α := R) (prod (Multiset.map (⇑leadingCoeffHom : (a : R[X]) → R) t))
    (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t))

Tactic:
simp only [leadingCoeffHom_apply]

Premises used: Polynomial.leadingCoeffHom_apply
-- Module: Mathlib.Algebra.Polynomial.BigOperators
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
⊢ Eq.{u + 1} (α := R) (leadingCoeff (∏ i ∈ s, f i)) (∏ i ∈ s, (f i).leadingCoeff)

Tactic:
simpa using leadingCoeff_multiset_prod (s.1.map f)

Premises used: Multiset.map, Finset.val, Polynomial.leadingCoeff_multiset_prod
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
rw : eval x (eval ((C : (a : R) → R[X]) y) ((C : (a : R[X]) → R[X][Y]) p)) = eval x p
rw₁ rw₂ : eval x p = eval x p
⊢ evalEval x y ((C : (a : R[X]) → R[X][Y]) p) = eval x p

Tactic:
rw [evalEval, eval_C]

Premises used: Polynomial.eval_C, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
rw : eval x (eval ((C : (a : R) → R[X]) y) (map C p)) = eval y p
rw₁ : eval x ((C : (a : R) → R[X]) (eval y p)) = eval y p
rw₂ rw₃ : eval y p = eval y p
⊢ evalEval x y (map C p) = eval y p

Tactic:
rw [evalEval, eval_map_apply, eval_C]

Premises used: Polynomial.eval_C, Polynomial.evalEval, Polynomial.eval_map_apply
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y p : R
rw : eval x ((C : (a : R) → R[X]) p) = p
rw₁ rw₂ : p = p
⊢ evalEval x y (CC p) = p

Tactic:
rw [evalEval_C, eval_C]

Premises used: Polynomial.eval_C, Polynomial.evalEval_C
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
⊢ evalEval x y 0 = 0

Tactic:
simp only [evalEval, eval_zero]

Premises used: Polynomial.eval_zero, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
⊢ evalEval x y 1 = 1

Tactic:
simp only [evalEval, eval_one]

Premises used: Polynomial.evalEval, Polynomial.eval_one
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
⊢ evalEval x y (↑n : R[X][Y]) = (↑n : R)

Tactic:
simp only [evalEval, eval_natCast]

Premises used: Polynomial.eval_natCast, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
rw : eval x (eval ((C : (a : R) → R[X]) y) Y) = y
rw₁ : eval x ((C : (a : R) → R[X]) y) = y
rw₂ rw₃ : y = y
⊢ evalEval x y Y = y

Tactic:
rw [evalEval, eval_X, eval_C]

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p + q) = evalEval x y p + evalEval x y q

Tactic:
simp only [evalEval, eval_add]

Premises used: Polynomial.evalEval, Polynomial.eval_add
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
f : ℕ → R → R[X][Y]
⊢ evalEval x y (p.sum f) = p.sum fun (n : ℕ) (a : R) ↦ evalEval x y (f n a)

Tactic:
simp only [evalEval, eval, eval₂_sum]

Premises used: Polynomial.eval, Polynomial.eval₂_sum, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_3
s : Finset ι
x y : R
f : ι → R[X][Y]
⊢ evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, evalEval x y (f i)

Tactic:
simp only [evalEval, eval_finsetSum]

Premises used: Polynomial.eval_finsetSum, Polynomial.evalEval
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : DistribSMul S R
inst_2 : IsScalarTower S R R
x y : R
s : S
p : R[X][Y]
⊢ evalEval x y (s • p) = s • evalEval x y p

Tactic:
simp only [evalEval, eval_smul]

Premises used: Polynomial.evalEval, Polynomial.eval_smul
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Semiring R
x y : R
⊢ Function.Surjective (α := R[X][Y]) (evalEval x y)

Tactic:
fun y => ⟨CC y, evalEval_CC ..⟩

Premises used: Polynomial.CC, Polynomial.evalEval_CC, Exists.intro, Function.Surjective
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Ring R
x y : R
p : R[X][Y]
⊢ evalEval x y (-p) = -evalEval x y p

Tactic:
simp only [evalEval, eval_neg]

Premises used: Polynomial.evalEval, Polynomial.eval_neg
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Ring R
x y : R
p q : R[X][Y]
⊢ evalEval x y (p - q) = evalEval x y p - evalEval x y q

Tactic:
simp only [evalEval, eval_sub]

Premises used: Polynomial.evalEval, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.Bivariate
Goal:
R : Type u_1
inst : Ring R
x y : R
n : ℤ
⊢ evalEval x y (↑n : R[X][Y]) = (↑n : R)

Tactic:
simp only [evalEval, eval_intCast]

Premises used: Polynomial.evalEval, Polynomial.eval_intCast