theorem Minimal.minimal_iff_minimal_exists_minimal_and_le {α : Type u_1} [Preorder α] [WellFoundedLT α] {P : α → Prop} {x : α} : Minimal P x ↔ Minimal (fun (x : α) => ∃ (m' : α), Minimal P m' ∧ m' ≤ x) x ∧ P x

theorem Minimal.prop_of_minimal_exists_minimal_and_le {α : Type u_1} [PartialOrder α] [WellFoundedLT α] {P : α → Prop} {x : α} (h : Minimal (fun (x : α) => ∃ (m' : α), Minimal P m' ∧ m' ≤ x) x) : P x

theorem Minimal.minimal_iff_minimal_exists_minimal_and_le' {α : Type u_1} [PartialOrder α] [WellFoundedLT α] {P : α → Prop} {x : α} : Minimal P x ↔ Minimal (fun (x : α) => ∃ (m' : α), Minimal P m' ∧ m' ≤ x) x

theorem AddMonoidAlgebra.ideal_span_of'_image_eq_ideal_span_of'_image_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} : Ideal.span (of' k A '' s) = Ideal.span (of' k A '' {x : A | Minimal (fun (x : A) => x ∈ s) x})

theorem AddMonoidAlgebra.ideal_span_single_image_eq_ideal_span_single_image_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} : Ideal.span ((fun (x : A) => single x 1) '' s) = Ideal.span ((fun (x : A) => single x 1) '' {x : A | Minimal (fun (x : A) => x ∈ s) x})

theorem AddMonoidAlgebra.minimal_span_of'_image_iff_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} [Nontrivial k] {x : A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span (of' k A '' s), x ∈ p.coeff.support) x ∧ x ∈ s ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.minimal_ideal_span_single_image_iff_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} [Nontrivial k] {x : A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span ((fun (x : A) => single x 1) '' s), x ∈ p.coeff.support) x ∧ x ∈ s ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.minimal_ideal_span_of'_image_iff_minimal' {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {x : A} {s : Set A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span (of' k A '' s), x ∈ p.coeff.support) x ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.minimal_ideal_span_single_image_iff_minimal' {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {x : A} {s : Set A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span ((fun (x : A) => single x 1) '' s), x ∈ p.coeff.support) x ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.ideal_span_of'_image_eq_ideal_span_of'_image_iff {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s t : Set A} : Ideal.span (of' k A '' s) = Ideal.span (of' k A '' t) ↔ ∀ (x : A), Minimal (fun (x : A) => x ∈ s) x ↔ Minimal (fun (x : A) => x ∈ t) x

theorem AddMonoidAlgebra.ideal_span_single_image_eq_ideal_span_single_image_iff {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s t : Set A} : Ideal.span ((fun (x : A) => single x 1) '' s) = Ideal.span ((fun (x : A) => single x 1) '' t) ↔ ∀ (x : A), Minimal (fun (x : A) => x ∈ s) x ↔ Minimal (fun (x : A) => x ∈ t) x

theorem MvPolynomial.ideal_span_monomial_image_eq_ideal_span_monomial_image_minimal {σ : Type u_2} {R : Type u_1} [CommSemiring R] {s : Set (σ →₀ ℕ)} : Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s) = Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' {x : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x})

theorem MvPolynomial.minimal_ideal_span_monomial_image_iff_minimal {σ : Type u_2} {R : Type u_1} [CommSemiring R] {x : σ →₀ ℕ} {s : Set (σ →₀ ℕ)} [Nontrivial R] : Minimal (fun (x : σ →₀ ℕ) => ∃ p ∈ Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s), x ∈ p.support) x ↔ Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x

theorem MvPolynomial.ideal_span_monomial_image_eq_ideal_span_monomial_image_iff {σ : Type u_2} {R : Type u_1} [CommSemiring R] {s t : Set (σ →₀ ℕ)} [Nontrivial R] : Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s) = Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' t) ↔ ∀ (x : σ →₀ ℕ), Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x ↔ Minimal (fun (x : σ →₀ ℕ) => x ∈ t) x

theorem MonomialOrder.span_leadingTerm_le_span_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {B : Set (MvPolynomial σ R)} : Ideal.span (m.leadingTerm '' B) ≤ Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

theorem MonoidAlgebra.mem_ideal_span_single_image_ {k : Type u_1} {G : Type u_3} [Monoid G] [Semiring k] {s : Set (k × G)} {x : MonoidAlgebra k G} : x ∈ Ideal.span ((fun (cm : k × G) => single cm.2 cm.1) '' s) ↔ ∀ (m : G), x.coeff m ∈ Ideal.span (Prod.fst '' {cm : k × G | cm ∈ s ∧ ∃ (d : G), m = d * cm.2})

theorem coeff_toMultiplicative_apply_ofAdd {R : Type u_4} {M : Type u_5} [Semiring R] [Add M] (x : AddMonoidAlgebra R M) (m : M) : ((AddMonoidAlgebra.toMultiplicative R M) x).coeff (Multiplicative.ofAdd m) = x.coeff m

theorem Set.image_ofPred {α : Type u_4} {β : Type u_5} {p : α → Prop} {f : β → α} (hf : Function.Surjective f) : f '' {b : β | p (f b)} = {a : α | p a}

theorem Set.image_ofPred_comp {α : Type u_4} {β : Type u_5} {p : α → Prop} {f : β → α} (hf : Function.Surjective f) : f '' ofPred (p ∘ f) = {a : α | p a}

theorem MonoidAlgebra.mem_ideal_span_single_image' {k : Type u_1} {G : Type u_3} {ι : Type u_4} [Monoid G] [Semiring k] {s : Set ι} {fm : ι → G} {fc : ι → k} {x : MonoidAlgebra k G} : x ∈ Ideal.span ((fun (i : ι) => single (fm i) (fc i)) '' s) ↔ ∀ (m : G), x.coeff m ∈ Ideal.span (fc '' {i : ι | i ∈ s ∧ ∃ (d : G), m = d * fm i})

theorem MonoidAlgebra.mem_ideal_span_single_image {k : Type u_1} {G : Type u_3} {ι : Type u_4} [Monoid G] [Semiring k] {s : Set ι} {fm : ι → G} {fc : ι → k} {x : MonoidAlgebra k G} : x ∈ Ideal.span ((fun (i : ι) => single (fm i) (fc i)) '' s) ↔ ∀ m ∈ x.coeff.support, x.coeff m ∈ Ideal.span (fc '' {i : ι | i ∈ s ∧ ∃ (d : G), m = d * fm i})

theorem AddMonoidAlgebra.mem_ideal_span_single_image' {k : Type u_1} {G : Type u_3} {ι : Type u_4} [AddMonoid G] [Semiring k] {s : Set ι} {fm : ι → G} {fc : ι → k} {x : AddMonoidAlgebra k G} : x ∈ Ideal.span ((fun (i : ι) => single (fm i) (fc i)) '' s) ↔ ∀ (m : G), x.coeff m ∈ Ideal.span (fc '' {i : ι | i ∈ s ∧ ∃ (d : G), m = d + fm i})

theorem AddMonoidAlgebra.mem_ideal_span_single_image {k : Type u_1} {G : Type u_3} {ι : Type u_4} [AddMonoid G] [Semiring k] {s : Set ι} {fm : ι → G} {fc : ι → k} {x : AddMonoidAlgebra k G} : x ∈ Ideal.span ((fun (i : ι) => single (fm i) (fc i)) '' s) ↔ ∀ m ∈ x.coeff.support, x.coeff m ∈ Ideal.span (fc '' {i : ι | i ∈ s ∧ ∃ (d : G), m = d + fm i})

theorem MvPolynomial.mem_ideal_span_monomial_image' {σ : Type u_4} {R : Type u_5} {ι : Type u_6} [CommSemiring R] {x : MvPolynomial σ R} {s : Set ι} {fm : ι → σ →₀ ℕ} {fc : ι → R} : x ∈ Ideal.span ((fun (i : ι) => (monomial (fm i)) (fc i)) '' s) ↔ ∀ xi ∈ x.support, x.coeff xi ∈ Ideal.span (fc '' {i : ι | i ∈ s ∧ fm i ≤ xi})