/-
Copyright (c) 2025 Junyu Guo and Hao Shen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyu Guo, Hao Shen
-/
module

public import Mathlib
public import Groebner.Remainder
public import Groebner.ToMathlib.Finsupp

/-! # Gröbner Basis

Definition:

* `MonomialOrder.IsGroebnerBasis m G I`: Given a monomial order `m`, a subset `G` of an ideal `I`
  is said to be a Gröbner basis if:
  (1) `G` is contained in `I` (i.e., all polynomials in `G` belong to the ideal `I`).
  (2) The ideal generated by the leading terms of all polynomials in `I` is equal to
    the ideal generated by the leading terms of the polynomials in `G`.

Buchberger criterion is proved with the following sequence of theorems, where each one is proved
(directly or indirectly) with some of theorems before it:

* `MonomialOrder.IsGroebnerBasis.remainder_eq_zero_iff_mem_ideal`: Given a remainder of a
  polynomial on division by a Gröbner basis of an ideal, the remainder is 0 if and only if the
  polynomial is in the ideal.

* `MonomialOrder.IsGroebnerBasis.isRemainder_zero_iff_mem_ideal`: Given a Gröbner basis of an
  ideal, 0 is a remainder of a polynomial on division by the Gröbner basis if and only if the
  polynomial is in the ideal `I`.

* `MonomialOrder.IsGroebnerBasis.ideal_eq_span`: Gröbner basis of any ideal spans the ideal.

* `MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero`: A set of
  polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal and 0 is a
  remainder of each member of this ideal on division by this set.

* `MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero`
  (Buchberger Criterion): a basis of an ideal is a Gröbner basis of it if and only if 0 is a
  remainder of echo sPolynomial between two polynomials on the basis.

Other main theroems:

* `MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder`: Remainder of any polynomial on
  division by a Gröbner basis exists and is unique.

* `MonomialOrder.IsGroebnerBasis.exists_isGroebnerBasis_finite`: Finite Gröbner basis exists for any
  ideal of a noetherian multivariate polynomial ring.

## Naming convention

Some theorems with an argument in type `Set (MvPolynomial σ R)` and a hypothesis that leading
coefficients of all polynomials in the set are invertible have 2 variants, named as following
respectively:

* without suffix `'` or `₀`: any polynomial `b` in the set has an invertible leading coefficient
  (`IsUnit (m.leadingCoeff p)`);
* with suffix `₀`: any polynomial `b` in the set either has an invertible leading coefficient or is
  equal to 0 (`IsUnit (m.leadingCoeff p) ∨ b = 0`);
* with suffix `'`: no hypotheses on leading coefficients, while requiring `R` to be a field
  (`Field k`, where the ring is denoted as `k` instead).

## Reference : [Cox2015]

-/

@[expose] public section

namespace MonomialOrder

open MvPolynomial IsRemainder

/-- A subset `G` of an ideal `I` is said to be a Gröbner basis if:

1. `G` is contained in `I` (i.e., all polynomials in `G` belong to the ideal `I`).
2. The ideal generated by the leading terms of all polynomials in `I` is equal to
   the ideal generated by the leading terms of the polynomials in `G`.
-/
def IsGroebnerBasis {σ : Type*} {m : MonomialOrder σ} {R : Type*}
    [CommSemiring R] (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) :=
  G ⊆ I ∧ Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G)
namespace IsGroebnerBasis

open scoped MonomialOrder
section CommSemiring
variable {σ : Type*} {m : MonomialOrder σ} {R : Type*} [CommSemiring R]
variable (f p : MvPolynomial σ R) (r : MvPolynomial σ R)

lemma subset {G : Set (MvPolynomial σ R)} {I} (h : m.IsGroebnerBasis G I) : G ⊆ I := h.1

lemma span_leadingTerm_image {G : Set (MvPolynomial σ R)} {I} (h : m.IsGroebnerBasis G I) :
    Ideal.span (m.leadingTerm '' ↑I) = Ideal.span (m.leadingTerm '' G) := h.2

lemma isGroebnerBasis_iff (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) :
    m.IsGroebnerBasis G I ↔
      G ⊆ I ∧ m.leadingTerm '' ↑I ⊆ (Ideal.span (m.leadingTerm '' G) : Set (MvPolynomial σ R)) := by
  constructor
  · intro h
    rw [← h.span_leadingTerm_image]
    exact ⟨h.subset, Ideal.subset_span⟩
  intro ⟨h₁, h₂⟩
  refine ⟨h₁, ?_⟩
  apply le_antisymm
  · rwa [Ideal.span_le]
  apply Ideal.span_mono
  exact Set.image_mono h₁

lemma of_subset {G G' : Set (MvPolynomial σ R)} {I} (h : m.IsGroebnerBasis G I)
    (hG : G ⊆ G') (hI : G' ⊆ I) : m.IsGroebnerBasis G' I := by
  rw [isGroebnerBasis_iff] at *
  exact ⟨hI, subset_trans h.2 (Ideal.span_mono <| Set.image_mono hG)⟩

@[simp]
lemma isGroebnerBasis_self (I : Ideal (MvPolynomial σ R)) :
    m.IsGroebnerBasis I I := by
  simp [IsGroebnerBasis]

@[simp]
lemma isGroebnerBasis_sdiff_singleton_zero (G : Set (MvPolynomial σ R))
    (I : Ideal (MvPolynomial σ R)) :
    m.IsGroebnerBasis (G \ {0}) I ↔ m.IsGroebnerBasis G I := by
  simp [IsGroebnerBasis, m.span_leadingTerm_sdiff_singleton_zero]

@[simp]
lemma isGroebnerBasis_insert_zero (G : Set (MvPolynomial σ R))
    (I : Ideal (MvPolynomial σ R)) :
    m.IsGroebnerBasis (insert 0 G) I ↔ m.IsGroebnerBasis G I := by
  unfold IsGroebnerBasis
  congr! 1
  · constructor
    · intro h x hx
      apply h
      simp [hx]
    · simp [Set.insert_subset_iff]
  · simp [m.span_leadingTerm_insert_zero]

/-- Finite Gröbner basis exists for any ideal of a noetherian multivariate polynomial ring. -/
theorem exists_isGroebnerBasis_finite [inst : IsNoetherianRing (MvPolynomial σ R)]
    (I : Ideal (MvPolynomial σ R)) :
    ∃ G : Set (MvPolynomial σ R), m.IsGroebnerBasis G I ∧ G.Finite := by
  -- todo: Ideal.fg_span_iff_fg_span_finset_subset
  have key := (Submodule.fg_span_iff_fg_span_finset_subset _).mp <|
    inst.noetherian <| Ideal.span <| m.leadingTerm '' ↑I
  simp only [Set.subset_image_iff] at key
  rcases key with ⟨s, ⟨G', hG'I, hG's⟩, hIs⟩
  have ⟨G, hG, hG₁⟩ := hG's ▸ Set.exists_subset_bijOn G' m.leadingTerm
  use G
  split_ands
  · exact subset_trans hG hG'I
  · rwa [hG₁.image_eq]
  · simp [Set.BijOn.finite_iff_finite hG₁]

lemma singleton_zero_bot :
    m.IsGroebnerBasis {(0 : MvPolynomial σ R)} ⊥ := by
  simp [IsGroebnerBasis]

lemma empty_bot :
    m.IsGroebnerBasis (∅ : Set <| MvPolynomial σ R) ⊥ := by
  simp [IsGroebnerBasis]

@[simp]
lemma singleton_zero_iff (I : Ideal (MvPolynomial σ R)) :
    m.IsGroebnerBasis {(0 : MvPolynomial σ R)} I ↔ I = ⊥ := by
  constructor
  · simp [IsGroebnerBasis, Ideal.span_eq_bot]
    aesop
  · simp_intro .. [singleton_zero_bot]

@[simp]
lemma empty_iff (I : Ideal (MvPolynomial σ R)) :
    m.IsGroebnerBasis (∅ : Set <| MvPolynomial σ R) I ↔ I = ⊥ := by
  constructor
  · simp [IsGroebnerBasis, Ideal.span_eq_bot]
    aesop
  · simp_intro .. [empty_bot]

@[simp, nontriviality]
lemma of_subsingleton [Subsingleton (MvPolynomial σ R)]
    {s : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} :
    m.IsGroebnerBasis s I := by
  classical
  simp [IsGroebnerBasis, Subsingleton.eq_zero (α := MvPolynomial σ R),
    Subsingleton.eq_zero (α := Ideal <| MvPolynomial σ R) I,
    Subsingleton.eq_zero (α := Ideal <| MvPolynomial σ R) (Ideal.span _)]

theorem isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le
    {G : Set (MvPolynomial σ R)} (I : Ideal (MvPolynomial σ R))
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :
    m.IsGroebnerBasis G I ↔
      G ⊆ I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, m.degree g ≤ m.degree p := by
  classical
  constructor
  · intro h
    exists h.subset
    intro p hp hp0
    apply Set.mem_image_of_mem m.leadingTerm at hp
    apply Ideal.subset_span at hp
    rw [h.span_leadingTerm_image, SetLike.mem_coe,
      m.span_leadingTerm_eq_span_monomial (by simp_intro .. [hG]),
      ← Set.image_image (monomial · 1) _ _, mem_ideal_span_monomial_image,
      m.support_leadingTerm' hp0] at hp
    simpa using hp
  rintro ⟨hG', h_degree⟩
  rw [isGroebnerBasis_iff]
  constructor
  · exact hG'
  intro p' hp
  rcases hp with ⟨p, hp', hp'₁⟩
  rw [←hp'₁, leadingTerm, SetLike.mem_coe,
    m.span_leadingTerm_eq_span_monomial (by simp_intro .. [hG]),
    ← Set.image_image (monomial · 1) _ _, mem_ideal_span_monomial_image]
  intro j hj
  specialize h_degree p
  simp_all [MonomialOrder.leadingCoeff_eq_zero_iff]

lemma isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le₀
    {G : Set (MvPolynomial σ R)} (I : Ideal (MvPolynomial σ R))
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) :
    m.IsGroebnerBasis G I ↔
      G ⊆ I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ m.degree p := by
  rw [← isGroebnerBasis_sdiff_singleton_zero,
    isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le]
  · simp [and_assoc]
  simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]

lemma span_leadingTerm_eq_span_monomial {G : Set (MvPolynomial σ R)}
    {I : Ideal (MvPolynomial σ R)}
    (h : m.IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :
    Ideal.span (m.leadingTerm '' ↑G) =
    Ideal.span ((fun p ↦ monomial (m.degree p) (1 : R)) '' (I \ {(0 : MvPolynomial σ R)})) := by
  classical
  wlog hR : Nontrivial R
  · rw [not_nontrivial_iff_subsingleton] at hR
    exact ((Submodule.subsingleton_iff _).mpr inferInstance).elim _ _
  rw [m.span_leadingTerm_eq_span_monomial (B := (↑G : Set (MvPolynomial σ R))) hG]
  apply le_antisymm
  · rw [Ideal.span_le]
    refine subset_trans ?_ Submodule.subset_span
    apply Set.image_mono
    apply Set.subset_diff_singleton h.subset
    contrapose! hG
    use 0
    simpa
  · rw [Ideal.span_le]
    intro x
    simp? says
      simp only [Set.mem_image, Set.mem_diff, SetLike.mem_coe, Set.mem_singleton_iff, ne_eq,
        forall_exists_index, and_imp]
    intro y hy hy0 hxy
    rw [← hxy, ← Set.image_image (monomial · 1) _ _, mem_ideal_span_monomial_image]
    simpa using ((isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le _ hG).mp h).2 y hy hy0

theorem span_leadingTerm_eq_span_monomial₀ {G : Set (MvPolynomial σ R)}
    {I : Ideal (MvPolynomial σ R)}
    (h : m.IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) :
    Ideal.span (m.leadingTerm '' ↑G) =
    Ideal.span ((fun p ↦ monomial (m.degree p) (1 : R)) '' (I \ {(0 : MvPolynomial σ R)})) := by
  rw [← isGroebnerBasis_sdiff_singleton_zero] at h
  convert span_leadingTerm_eq_span_monomial h _ using 1
  · simp [m.image_leadingTerm_sdiff_singleton_zero]
  · simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]

lemma isGroebnerBasis_of_forall_finite_isGroebnerBasis₀ {G : Set (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0)
    {I : Ideal (MvPolynomial σ R)}
    (h : ∀ s : Finset σ,
      ∃ (σ' : Type*), ∃ m' : MonomialOrder σ', ∃ e : m'.Embedding m,
        ↑s ⊆ Set.range e ∧ m'.IsGroebnerBasis (rename e ⁻¹' G) (I.comap (rename e))) :
    m.IsGroebnerBasis G I := by
  rw [isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le₀ (hG := hG)]
  constructor
  · intro p hp
    obtain ⟨σ', m', e, h, h', -⟩ := h p.vars
    -- todo: `Injective` is not necessary for `MvPolynomial.exists_rename_eq_of_vars_subset_range`
    obtain ⟨p', rfl⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range _ _ e.coe_injective h
    -- why are they defeq?
    apply Set.mem_of_mem_of_subset (Set.mem_preimage.mpr <| hp) h'
  rintro p hp hp0
  obtain ⟨σ', m', e, h, h'⟩ := h p.vars
  obtain ⟨p', rfl⟩ := MvPolynomial.exists_rename_eq_of_vars_subset_range _ _ e.coe_injective h
  rw [isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le₀] at h'
  case hG =>
    intro g
    simpa using hG (g.rename e)
  simp? at hp0 says
    simp only [ne_eq, Embedding.coe_injective, rename_eq_zero_iff_of_injective] at hp0
  -- again: why is `hp` defeq with the hypothesis
  replace ⟨g', h⟩ := h'.2 p' hp hp0
  -- todo: why is here a extra space?
  simp? at h says simp only [Set.mem_preimage, ne_eq] at h
  refine ⟨g'.rename e, h.1, by simpa using h.2⟩

theorem isGroebnerBasis_union_of_forall_finite_isGroebnerBasis₀
    {I : Ideal (MvPolynomial σ R)} {σ' : Finset σ → Type*}
    {m' : (s : Finset σ) → MonomialOrder (σ' s)}
    {e : (s : Finset σ) → (m' s).Embedding m}
    {G' : (s : Finset σ) → Set (MvPolynomial (σ' s) R)}
    (hG' : ∀ s, ∀ g ∈ G' s, IsUnit ((m' s).leadingCoeff g) ∨ g = 0)
    (h : ∀ s, ↑s ⊆ Set.range (e s))
    (h' : ∀ s, (m' s).IsGroebnerBasis (G' s) (I.comap <| rename (e s))) :
    m.IsGroebnerBasis (⋃ s : Finset σ, rename (e s) '' G' s) I := by
  apply isGroebnerBasis_of_forall_finite_isGroebnerBasis₀
  · simp
    intro g s g' hg' rfl
    simpa using hG' s g' hg'
  intro s
  use σ' s, m' s, e s
  exists h s
  simp only [Set.preimage_iUnion]
  apply of_subset (h' s)
  · apply Set.subset_iUnion_of_subset s
    simp [Set.preimage_image_eq _ (rename_injective _ (e s).coe_injective)]
  simp
  intro s'
  apply Set.preimage_mono
  simpa using (h' s').subset

lemma isGroebnerBasis_of_forall_finite_isGroebnerBasis {G : Set (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
    {I : Ideal (MvPolynomial σ R)}
    (h : ∀ s : Finset σ,
      ∃ (σ' : Type*), ∃ m' : MonomialOrder σ', ∃ e : m'.Embedding m,
        ↑s ⊆ Set.range e ∧ m'.IsGroebnerBasis (rename e ⁻¹' G) (I.comap (rename e))) :
    m.IsGroebnerBasis G I :=
  isGroebnerBasis_of_forall_finite_isGroebnerBasis₀ (fun g hg ↦ Or.inl (hG g hg)) h

theorem isGroebnerBasis_union_of_forall_finite_isGroebnerBasis
    {I : Ideal (MvPolynomial σ R)} {σ' : Finset σ → Type*}
    {m' : (s : Finset σ) → MonomialOrder (σ' s)}
    {e : (s : Finset σ) → (m' s).Embedding m}
    {G' : (s : Finset σ) → Set (MvPolynomial (σ' s) R)}
    (hG' : ∀ s, ∀ g ∈ G' s, IsUnit ((m' s).leadingCoeff g))
    (h : ∀ s, ↑s ⊆ Set.range (e s))
    (h' : ∀ s, (m' s).IsGroebnerBasis (G' s) (I.comap <| rename (e s))) :
    m.IsGroebnerBasis (⋃ s : Finset σ, rename (e s) '' G' s) I :=
  isGroebnerBasis_union_of_forall_finite_isGroebnerBasis₀ (fun s g hg ↦ Or.inl (hG' s g hg)) h h'

end CommSemiring

section CommRing

variable {σ : Type*} {m : MonomialOrder σ} {R : Type*} [CommRing R]

/-- Given a remainder `r` of a polynomial `p` on division by a Gröbner basis `G` of an ideal `I`,
the remainder `r` is 0 if and only if `p` is in the ideal `I`.

Any leading coefficient of polynomial in the Gröbner basis `G` is required to be a unit. -/
theorem remainder_eq_zero_iff_mem_ideal
    {p : MvPolynomial σ R} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)}
    {r : MvPolynomial σ R} (h : m.IsGroebnerBasis G I)
    (hr : m.IsRemainder p G r) :
    r = 0 ↔ p ∈ I := by
  constructor
  · rw [← mem_ideal_iff h.subset hr]
    simp_intro ..
  intro h_p_mem
  rcases h with ⟨h_G', h_span⟩
  have ⟨⟨q, h_p_eq_sum_r, h_r_reduced⟩, h_degree⟩ := hr
  rw [h_p_eq_sum_r, Ideal.add_mem_iff_right] at h_p_mem
  on_goal 2 =>
    exact Ideal.span_le.mpr h_G' <| (Finsupp.mem_span_iff_linearCombination ..).mpr ⟨_, rfl⟩
  apply Set.mem_image_of_mem m.leadingTerm at h_p_mem
  -- todo: Ideal.mem_span_of_mem
  apply Submodule.mem_span_of_mem (R := MvPolynomial σ R) at h_p_mem
  contrapose! h_p_mem with h_r_ne_zero
  simpa [← h_span] using term_notMem_span_leadingTerm hr (m.degree r) (by simp [h_r_ne_zero])

/-- Given a Gröbner basis `G` of an ideal `I`, 0 is a remainder on division by `G` if and
only if `p` is in the ideal `I`.
-/
theorem isRemainder_zero_iff_mem_ideal {p : MvPolynomial σ R}
    {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g))
    (h : m.IsGroebnerBasis G I) :
    m.IsRemainder p G 0 ↔ p ∈ I := by
  constructor
  · intro hr
    apply (remainder_eq_zero_iff_mem_ideal h hr).mp rfl
  · intro hp
    obtain ⟨r, hr⟩ := exists_isRemainder₀ (fun g a ↦ Or.symm (Or.inr (hG g a))) p
    rwa [(remainder_eq_zero_iff_mem_ideal h hr).mpr hp] at hr

lemma isRemainder_zero_iff_mem_ideal₀ {p : MvPolynomial σ R}
    {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0)
    (h : m.IsGroebnerBasis G I) :
    m.IsRemainder p G 0 ↔ p ∈ I := by
  rw [← isGroebnerBasis_sdiff_singleton_zero] at h
  rw [← isRemainder_sdiff_singleton_zero_iff_isRemainder]
  refine isRemainder_zero_iff_mem_ideal ?_ h
  simp_intro a b [or_iff_not_imp_right.mp (hG _ _)]

/-- Gröbner basis of any ideal spans the ideal. -/
theorem ideal_eq_span {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) (h : m.IsGroebnerBasis G I) :
    I = Ideal.span G := by
  apply le_antisymm
  · intro p hp
    rw [← isRemainder_zero_iff_mem_ideal hG h] at hp
    obtain ⟨⟨f, h_eq, h_deg⟩, h_remain⟩ := hp
    rw [h_eq, Finsupp.linearCombination_apply, add_zero]
    apply Ideal.sum_mem
    intro g hg
    rcases g with ⟨g, gG'⟩
    exact Ideal.mul_mem_left _ _ (Ideal.subset_span gG')
  · intro p hp
    suffices Ideal.span ↑G ≤ I from this hp
    apply Ideal.span_le.mpr
    intro p hp'
    exact h.subset hp'

theorem ideal_eq_span₀ {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) (h : m.IsGroebnerBasis G I) :
    I = Ideal.span G := by
  rw [← isGroebnerBasis_sdiff_singleton_zero] at h
  rw [h.ideal_eq_span, Ideal.span_sdiff_singleton_zero]
  simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]

theorem isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span (G : Set (MvPolynomial σ R))
    (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :
    m.IsGroebnerBasis G I ↔ (I = Ideal.span G ∧ m.IsGroebnerBasis G (Ideal.span G)) := by
  constructor
  · intro this
    simpa [ideal_eq_span hG this]
  · simp_intro ..

theorem isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span₀ (G : Set (MvPolynomial σ R))
    (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) :
    m.IsGroebnerBasis G I ↔ (I = Ideal.span G ∧ m.IsGroebnerBasis G (Ideal.span G)) := by
  simp_rw [← isGroebnerBasis_sdiff_singleton_zero (G := G),
    ← Ideal.span_sdiff_singleton_zero (s := G)]
  apply isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span
  simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]

/-- A set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal
and 0 is a remainder of each member of this ideal on division by this set.

Any leading coefficient of polynomial in the set is required to be a unit. -/
theorem isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero
    (G : Set (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R))
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :
    m.IsGroebnerBasis G I ↔ G ⊆ I ∧ ∀ p ∈ I, m.IsRemainder p G 0 := by
  constructor
  · intro h
    exists h.subset
    intro p h_p_in_I
    rwa [isRemainder_zero_iff_mem_ideal hG h]
  · intro h
    rcases h with ⟨h_G, h_remainder⟩
    rw [isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le I hG]
    constructor
    · apply h_G
    · intro p hp hp0
      exact exists_degree_le_degree_of_zero hp0 (h_remainder p hp)

/-- A set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal
and 0 is a remainder of each member of this ideal on division by this set.

It is a variant of
`MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero`, allowing
the set to contain also 0, besides polynomials with invertible leading coefficients. -/
theorem isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero₀ (G : Set (MvPolynomial σ R))
    (I : Ideal (MvPolynomial σ R)) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) :
    m.IsGroebnerBasis G I ↔ G ⊆ I ∧ ∀ p ∈ I, m.IsRemainder p G 0 := by
  rw [← isGroebnerBasis_sdiff_singleton_zero]
  convert isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero (G \ {0}) I _ using 2
  · simp
  · simp [isRemainder_sdiff_singleton_zero_iff_isRemainder]
  · simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]

/-- Remainder of any polynomial on division by a Gröbner basis exists and is unique.

Any leading coefficient of polynomial in the Gröbner basis is required to be a unit. -/
theorem existsUnique_isRemainder {G : Set (MvPolynomial σ R)}
    {I : Ideal (MvPolynomial σ R)}
    (h : m.IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) (p : MvPolynomial σ R) :
    ∃! (r : MvPolynomial σ R), m.IsRemainder p G r := by
  apply existsUnique_of_exists_of_unique (exists_isRemainder hG p)
  intro r₁ r₂ hr₁ hr₂
  rw [← sub_eq_zero]
  by_contra! hrne0
  have hr := (m.degree_mem_support_iff _).mpr hrne0
  apply sub_monomial_notMem_span_leadingTerm (B := ↑G) hr₁ hr₂ at hr
  rw [span_leadingTerm_eq_span_monomial h hG] at hr
  apply hr
  apply Submodule.mem_span_of_mem
  apply Set.mem_image_of_mem
  simpa [hrne0] using sub_mem_ideal_of_isRemainder_of_subset_ideal h.subset hr₁ hr₂

/-- Remainder of any polynomial on division by a Gröbner basis exists and is unique.

It is a variant of `MonomialOrder.IsGroebnerBasis.existsUnique_isRemainder`, allowing the
Gröbner basis to contain also 0, besides polynomials with invertible leading coefficients. -/
theorem existsUnique_isRemainder₀ {G : Set (MvPolynomial σ R)}
    {I : Ideal (MvPolynomial σ R)}
    (h : m.IsGroebnerBasis G I) (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0)
    (p : MvPolynomial σ R) :
    ∃! (r : MvPolynomial σ R), m.IsRemainder p G r := by
  rw [← isGroebnerBasis_sdiff_singleton_zero] at h
  simp_rw [← isRemainder_sdiff_singleton_zero_iff_isRemainder p G]
  convert existsUnique_isRemainder h _ p
  simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]

private lemma degree_lt_of_left_ne_zero_of_degree_mul_lt_of_mem_nonZeroDivisors {R} [CommSemiring R]
    {p p' q : MvPolynomial σ R}
    (hp : p ≠ 0) (hq : m.leadingCoeff q ∈ nonZeroDivisors _)
    (h : m.degree (p * q) ≺[m] m.degree (p' * q)) :
    m.degree p ≺[m] m.degree p' := by
  apply lt_of_le_of_lt' m.degree_mul_le at h
  simpa [m.degree_mul_of_right_mem_nonZeroDivisors hp hq] using h

private lemma degree_mul_lt_iff_left_lt_of_ne_zero_of_mem_nonZeroDivisors {R}
    [CommSemiring R] {p p' q : MvPolynomial σ R}
    (hp : p ≠ 0) (hq : m.leadingCoeff q ∈ nonZeroDivisors _) :
    m.degree (p * q) ≺[m] m.degree (p' * q) ↔ m.degree p ≺[m] m.degree p' := by
  refine ⟨degree_lt_of_left_ne_zero_of_degree_mul_lt_of_mem_nonZeroDivisors hp hq, ?_⟩
  intro h
  simpa [m.degree_mul_of_right_mem_nonZeroDivisors hp hq,
    m.degree_mul_of_right_mem_nonZeroDivisors (show p' ≠ 0 by contrapose! h; simp [h]) hq] using h

set_option maxHeartbeats 400000 in
-- It reaches the default max heart beats with option `says.verify` set to `true`, without which the
-- proof can pass with default max heart beats.
/-- Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if 0 is a
remainder of echo sPolynomial between two polynomials on the basis. -/
theorem isGroebnerBasis_iff_isRemainder_sPolynomial_zero
    {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :
    m.IsGroebnerBasis G (Ideal.span G) ↔
      ∀ (g₁ g₂ : G), m.IsRemainder (m.sPolynomial g₁ g₂ : MvPolynomial σ R) G 0 := by
  /- The informal proof is attached in comment blocks (`/- -/`), where math expressions are written
  in `$ $` or `$$ $$` like in LaTeX or Markdown, while we tend to use unicode symbols like Lean code
  instead of LaTeX commands are used for readability. And every block roughly corresponds with a
  block of code below it and above the next comment block (if it exists). And inline comments (`--`)
  are about technical details in formalization. -/
  -- TODO: (maybe) simplify this proof with `withBotDegree`? (The current proof was made before
  -- `withBotDegree` was defined and used to refactore `IsRemainder`, so it deals with some edge
  -- cases about degree of zero polynomial.)
  classical
  constructor
  · /- (→) Easy to prove. -/
    intro h _ _
    rw [isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero (hG := hG)] at h
    apply h.2
    apply m.sPolynomial_mem_ideal <;> exact Set.mem_of_mem_of_subset (by simp) h.1
  /- (←)
  We only need to prove for all $p ∈ ⟨G⟩$ (`p ∈ Ideal.span G`),
  (with loss of generality, assuming $p ≠ 0$)
  $0$ is a remainder of $p$ on division by $G$ (`m.IsRemainder p G 0`), i.e.
  to prove that these exists finite subset $G'$ of $G$ and $f$
  s.t. $p = ∑_{g ∈ G'} f(g) * g$ and $∀ g ∈ G', degree(f(g) * g) ≤ degree(p)$. -/
  wlog! _ : Nontrivial R
  · simp
  have hG₁ {g : G} := hG g g.prop
  have hG₀ {g} := (@hG₁ g).mem_nonZeroDivisors
  -- `rfl` doens't rewrite the goal?
  intro hsPoly
  rw [isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero (hG := hG)]
  exists Ideal.subset_span
  intro p hp
  wlog! hpne0 : p ≠ 0
  · simp [hpne0]
  simp_rw [isRemainder_def, add_zero, ← map_add,
    ← m.withBotDegree_mul_of_left_mem_nonZeroDivisors hG₀,
    m.withBotDegree_le_withBotDegree_iff_of_ne_zero _ hpne0]
  refine ⟨?_, by simp⟩
  /- From $p ∈ ⟨G⟩$, we get immediately that all condition we needed above except for
  $∀ g ∈ G', degree(f(g) * g) ≤ degree(p)$.
  We assume it doesn't hold, i.e. $max_{g ∈ G'} degree(f(g) * g) > degree(p)$. -/
    -- todo: `Ideal.mem_span_iff_exists_finset_subset`?
  obtain ⟨f₀_, G'₀_, hG'_, ⟨-, hsumf⟩⟩ := Submodule.mem_span_iff_exists_finset_subset.mp hp
  -- we need variants of `f₀` abd `G'₀` that use coercion `↥G` instead of `MvPolynomial σ R`, to
  -- pass the information of set membership and make use of `hG` and S-polynomial decomposition.
  let G'₀ := G'₀_.attach.image (β := G) (fun p ↦ ⟨p.val, hG'_ p.prop⟩)
  let f₀ (p : G) := f₀_ p
  convert_to ∑ a ∈ G'₀, f₀ a * a = p at hsumf
  · unfold G'₀
    rw [Finset.sum_image (by simp [Function.Injective])]
    exact Finset.sum_attach .. |>.symm
  clear_value G'₀ f₀
  clear hG'_ G'₀_ f₀_
  by_cases! h : G'₀.sup (fun g ↦ (m.toSyn <| m.degree <| g.val * (f₀ g))) ≤ m.toSyn (m.degree p)
  · exact ⟨f₀, G'₀, hsumf.symm, by simpa using h⟩
  /- We have now $P(max_{g ∈ G'} degree(f(g) * g))$ where
  $P(a) : ∃ finite G' ⊆ G and f, p = ∑ g ∈ G', f(g) * g ∧ ∀ g ∈ G', degree(f(g) * g) ≤ a$,
  and we will prove an assertion that, for each $a > degree(p)$, if $P(a)$, then there exists
  $degree(g) ≤ a' < a$ s.t. $P(a')$ also holds. With this assertion, we can get $P(degree(p))$ by
  well-founded induction on $a$.
  (Formalization note: here we don't directly prove $degree(p)$ satisfies predicate $P$ by
   induction. We prove with predicate $a ↦ degree(p) ≤ a ∧ P(a)$ instead.) -/
  -- todo: lemmas for induction in this form.
  refine WellFounded.induction_bot WellFoundedLT.toWellFoundedRelation.wf
    (a := G'₀.sup fun g ↦ (m.toSyn <| m.degree <| g.val * (f₀ g))) (bot := m.toSyn (m.degree p))
    (C := fun a ↦ m.toSyn (m.degree p) ≤ a ∧
      ∃ (f : G → MvPolynomial σ R) (G' : Finset G),
        p = ∑ g ∈ G', (f g) * g ∧
        ∀ g ∈ G', (m.toSyn <| m.degree <| g.val * f g) ≤ a)
    (fun a ha ⟨ha', ⟨f, G', hsumf, h_deg_le⟩⟩ ↦ ?_)
    ⟨le_of_lt h, ⟨f₀, G'₀, hsumf.symm, by apply Finset.le_sup⟩⟩ |>.2
  /- We start to prove the assertion. Assume $a > degree(p)$ (`ha`), $G' ⊆ G$ (`hG'subsetG`),
  $f$ (`f`) s.t. $p = ∑ g ∈ G', f(g) * g$ (`hsumf`), and
  $∀ g ∈ G', degree(f(g) * g) ≤ a$ (`h_deg_le`).
  Without loss of generality, we can assume $f(g)$ vanishes when $g ∉ G'$.  -/
  clear! f₀ G'₀
  wlog hf₀support : ∀ g, g ∉ G' → f g = 0 generalizing f
  · specialize this (fun g ↦ if g ∈ G' then f g else 0); simp_all
  apply lt_of_le_of_ne' ha' at ha
  /- Let $lt'(g) := leadingTerm(g) if degree(f(g) * g) = a, or else 0$ (`lt'`).
  $$ p = ∑ g ∈ G', f(g) * g
       = ∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g +
        ∑ g ∈ G', (f(g) - lt'(g)) * g.$$ (`hp`) -/
  let degFgEqA g := (m.toSyn <| m.degree <| f g * g.val) = a
  let lt' g := if degFgEqA g then m.leadingTerm (f g) else 0
  have hp := calc
    p = ∑ g ∈ G', f g * g := hsumf
    _ = ∑ g ∈ G' with degFgEqA g, m.leadingTerm (f g) * g +
        ∑ g ∈ G', (f g - lt' g) * g := by
      simp [← Finset.sum_add_distrib, ← add_mul, ← ite_zero_mul, Finset.sum_filter, -ite_mul, lt']
  /- For any $g ∈ G'$, it can be easily seen that $degree (f(g) - lt'(g)) g$ is either less than $a$
  or equal to $0$, so $degree( (f(g) - lt'(g)) * g ) < a$, and $∑ g ∈ G', (f(g) - lt'(g)) * g < a$.
  Since $$degree( ∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g +
      ∑ g ∈ G', (f(g) - lt'(g)) * g )
    = degree(p) < a,$$
  we can obtain $degree( ∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g ) < a$.
  Obviously, $degree(leadingTerm(f(g)) g)) = a$, for all $g ∈ G'$ s.t. $degree(f(g) g) = a$.
  So this sum can be decomposed into a sum of S-polynomials: there exists $c(g₁, g₂) ∈ R$ (`c`)
  for each $g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\}$, s.t.
  $$∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g
    = ∑ g ∈ G' with (degree(f(g) * g) = a), leadingCoeff(f(g)) • lm(f(g)) * g
    = ∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
          c(g₁, g₂) * sPoly(lm(f(g₁)) * g₁, lm(f(g₂)) * g₂)
    = ∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
          c(g₁, g₂) * (lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * sPoly(g₁, g₂),$$
    (`h_sum_sPoly`)
  where $lm(p)$ is leading monomial of $p$ ($x^degree(p)$ if we ignore edge case that $p = 0$),
  and $lcm(lm(g₁), lm(g₂))$ is least common multiple of $lm(g₁)$ and $lm(g₂)$.
  (Formalization note: formalization of $lcm$ is based on operations on `Finsupp` instead of
  `MvPolynomial`. For more formalization details, see the doc of `MonomialOrder.sPolynomial`.) -/
  have h_a_gt_zero : 0 < a := bot_lt_of_lt ha
  let leadingTerm_mul_eq (p q : MvPolynomial σ R) :
      m.leadingTerm p * q = m.leadingCoeff p • (monomial (m.degree p) 1 * q) := by
    rw [smul_eq_C_mul, ← mul_assoc, C_mul_monomial, mul_one, leadingTerm]
    -- simp [← mul_assoc]
  obtain ⟨c, h_sum_sPoly⟩ := m.sPolynomial_decomposition_of_degree_sum_smul_le
    (d := a) (B := G'.filter degFgEqA) (g := fun g ↦ monomial (m.degree (f g)) 1 * g.val)
    (c := fun g ↦ m.leadingCoeff (f g))
    (hB := by simp [hG, m.leadingCoeff_mul_of_right_mem_nonZeroDivisors' hG₀])
    (by
      simp only [Finset.mem_filter, and_imp, degFgEqA]
      intro b hb h
      rw [m.degree_mul_of_right_mem_nonZeroDivisors ?_ hG₀]
        at h ⊢
      · simpa [m.degree_monomial] using h
      · simp
      contrapose! h_a_gt_zero with hfb
      simp [← h, hfb])
    (by
      simp only [leadingTerm_mul_eq] at hp
      simp only [← sub_eq_iff_eq_add.mpr hp]
      apply lt_of_le_of_lt m.degree_sub_le
      simp? [ha] says simp only [sup_lt_iff, ha, true_and]
      apply lt_of_le_of_lt m.degree_sum_le
      simp only [Finset.sup_lt_iff h_a_gt_zero, lt']
      intro g hg
      wlog h : degFgEqA g
      · simpa [h] using lt_of_le_of_ne (mul_comm g.val _ ▸ h_deg_le g hg) h
      simp? [h] says simp only [h, ↓reduceIte]
      wlog! +distrib h' : f g - m.leadingTerm (f g) ≠ 0
      · simp [h_a_gt_zero, h']
      apply lt_of_le_of_lt' (h_deg_le g hg)
      -- case edge about `degree 0`
      rw [mul_comm g.val, degree_mul_lt_iff_left_lt_of_ne_zero_of_mem_nonZeroDivisors h' hG₀]
      exact m.degree_sub_leadingTerm_lt_degree (m.degree_ne_zero_of_sub_leadingTerm_ne_zero h'))
  conv at h_sum_sPoly =>
    simp only [← leadingTerm_mul_eq]
    rhs
    simp only [m.sPolynomial_monomial_mul_of_mem_nonZeroDivisors hG₀ hG₀,
      ← G'.filter degFgEqA |>.sum_coe_sort]
  /- For echo $g₁, g₂ ∈ G$, $0$ is a remainder of $sPoly(g₁, g₂)$ on division
  by G, and thus we obtain its "quotients" in form of a finitely supported function $q_{g₁, g₂}$
  s.t. it satisfies the following conditions (`hq`):
    - $supp(q_{g₁, g₂}) ⊆ G$,
    - $sPoly(g₁, g₂) = ∑ g ∈ G, q_{g₁, g₂}(g) * g$,
    - $∀ g ∈ G, degree(q_{g₁, g₂}(g) * g) ≤ degree(sPoly(g₁, g₂))$, and
    - if $sPoly(g₁, g₂) = 0$ then $q_{g₁, g₂} = 0$. -/
  simp [IsRemainder, -Subtype.forall, ← map_add,
    ← m.withBotDegree_mul_of_left_mem_nonZeroDivisors hG₀,
    m.withBotDegree_le_withBotDegree_iff] at hsPoly
  replace hsPoly (g₁ g₂ : G'.filter degFgEqA) := hsPoly g₁ g₂
  let q (g₁ g₂ : G'.filter degFgEqA) := (hsPoly g₁ g₂).choose
  have hq (g₁ g₂ : G'.filter degFgEqA) := (hsPoly g₁ g₂).choose_spec
  -- I'd like to get rid of `.choose` in following formalization.
  simp_rw [show _ = q _ _ by unfold q; rfl] at hq
  -- TODO: a variant of `generalize` tactic that can replace with arguments
  clear_value q -- clear its value to ensure we will not use it (optional)
  /- Let $G''$ be $G' ∪ (∪ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\}, supp(q_{g₁, g₂})).$
  Obviously, $G''$ is a finite subset of $G$, and
  $support(q_{g₁, g₂}) ⊆ G''$ for all $g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\}$.
  Then for all $g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\}$,
  $sPoly(g₁, g₂) = ∑ g ∈ G'', q_{g₁, g₂}(g) * g$. -/
  let G'' : Finset G := G' ∪
    (G'.filter degFgEqA).attach.biUnion fun b₁ ↦
      (G'.filter degFgEqA).attach.biUnion fun b₂ ↦ (q b₁ b₂).support
  conv at hq =>
    ext g₁ g₂
    simp only [Finsupp.linearCombination_apply_of_mem_supported
        (l := (q g₁ g₂)) (s := G'')
        (hs := by
          simp? [Finsupp.mem_supported, G''] says
            simp only [Finset.coe_union, Finset.coe_biUnion, Finset.coe_attach, Set.mem_univ,
              Set.iUnion_true, Finsupp.mem_supported, G'']
          apply Set.subset_union_of_subset_right
          exact Set.subset_iUnion₂_of_subset g₁ g₂ subset_rfl), smul_eq_mul]
  /- Substituting them into our decomposition by S-polynomials, we have:
  $$∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g
    = ∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
        c(g₁, g₂) * (lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * sPoly(g₁, g₂)
    = ∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
        c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) *
        ∑ g ∈ G'', q_{g₁, g₂}(g) * g
    = ∑ g ∈ G'',
        (∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
          c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * q_{g₁, g₂}(g)) *
        g. $$ (`h_sum_sPoly`)
  Note: degrees of $(f(g) - lt'(g)) * g$ and
    $c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * q_{g₁, g₂} * g$ are
    both less than $a$. It is a key to complete the proof. We will proof it at the end. -/
  simp_rw [(hq _ _).1] at h_sum_sPoly
  replace hq (g₁ g₂ : G'.filter degFgEqA) := (hq g₁ g₂).2
  clear hsPoly -- clear the infoview (optional)
  set_option backward.isDefEq.respectTransparency false in
  simp_rw [mul_one, G''.mul_sum, ← mul_assoc, Finset.smul_sum,
    ← smul_mul_assoc, smul_monomial, Finset.sum_comm (t:=G''), ← Finset.sum_mul,
    smul_eq_mul (α := R)] at h_sum_sPoly
  /- With the assumption that $f(g)$ vanishes when $g ∉ G'$ and $G'' ⊆ G'$, we have
  $$p = ∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g + ∑ g ∈ G', (f(g) - lt'(g)) * g
    = ∑ g ∈ G' with (degree(f(g) * g) = a), leadingTerm(f(g)) * g + ∑ g ∈ G'', (f(g) - lt'(g)) * g
    = ∑ g ∈ G'',
        (∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
           c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * q_{g₁, g₂}(g)) *
        g +
      ∑ g ∈ G'', (f(g) - lt'(g)) * g
    = ∑ g ∈ G'',
        (∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
           c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * q_{g₁, g₂}(g) +
         (f(g) - lt'(g))) *
        g.$$ -/
  convert_to p = _ + ∑ g ∈ G'', (f g - lt' g) * g using 2 at hp
  · exact Finset.sum_subset (by simp [G'']) (by simp_intro .. [hf₀support, lt'])
  simp_rw [h_sum_sPoly, ← Finset.sum_add_distrib, ← add_mul] at hp
  /- Let $f'(g)$ be
  $$∑ g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\},
      c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * q_{g₁, g₂}(g)
    + (f(g) - lt'(g)),$$
  and $a'$ be $max(degree(p), max_{g ∈ G''} f'(g) * g)$. Then we have $p = ∑ g ∈ G'', f'(g) * g$,
  and apparently $degree(p) ≤ a'$ and $∀ g ∈ G'', degree(f'(g) * g) ≤ a'$. Now both
  $degree(p) ≤ a'$ and $P(a')$ are got.
  To prove the theorem, it remains to prove that $a' < a$. -/
  -- use `by exact hp` to assign a long expression (which we don't want to write) to `?f'`
  refine ⟨m.toSyn (m.degree p) ⊔ G''.sup fun g ↦ m.toSyn <| m.degree <| ?f' g * g.val,
    (?_ : _ < _), by simp, ?f', G'', by exact hp, ?le_max⟩
  case le_max =>
    intro h g
    rw [mul_comm]
    exact le_trans (Finset.le_sup (f := fun g ↦ m.toSyn <| m.degree (?f' g * g.val)) g) le_sup_right
  /- It suffices that $degree(f'(g) * g) < a$ for all $g ∈ G''$. Then it suffices that, degrees of
  the left side (too long...) and the right side $f(g) - lt'(g)$ of the outermost $+$ in $f'$
  multiplied by $g$ respectively are both less than $a$ for all $g ∈ G''$.
  -/
  clear hp h_sum_sPoly -- remove them since they're long and will not be used anymore
  simp? [ha, Finset.sup_lt_iff h_a_gt_zero, add_mul, -Subtype.forall] says
    simp only [Finset.univ_eq_attach, mul_one, add_mul, sup_lt_iff, ha,
      Finset.sup_lt_iff h_a_gt_zero, true_and]
  intro g hg'
  apply lt_of_le_of_lt degree_add_le
  apply max_lt
  · /- To prove the left side, it suffices to show
    $degree(c(g₁, g₂)•(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) *
      q_{g₁, g₂}(g) * g) < a$
    for all $g₁, g₂ ∈ \{g ∈ G' | degree(f(g) * g) = a\}$ (`g₁`, `g₂`). -/
    simp_rw [Finset.sum_mul]
    refine lt_of_le_of_lt m.degree_sum_le <| (Finset.sup_lt_iff h_a_gt_zero).mpr ?_
    simp? [-Finset.mem_filter, -Subtype.forall] says simp only [Finset.mem_attach, forall_const]
    intro g₁
    refine lt_of_le_of_lt m.degree_sum_le <| (Finset.sup_lt_iff h_a_gt_zero).mpr ?_
    simp? [-Finset.mem_filter, -Subtype.forall] says simp only [Finset.mem_attach, forall_const]
    intro g₂
    /- Without loss of generality, we assume $sPoly(g₁, g₂) ≠ 0$.
    (If it is $0$, then $q_{g₁, g₂} = 0$).
    $$degree(
      c(g₁, g₂) • (lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)) / lcm(lm(g₁), lm(g₂))) * q_{g₁, g₂}(g) * g)
    ≤ degree(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂))) - degree(lcm(lm(g₁), lm(g₂))) +
        degree(q_{g₁, g₂}(g) * g)$$ -/
    obtain ⟨h_deg_gq_le_sPoly, h_q_eq_0_of_sPoly_eq_0⟩ := hq g₁ g₂ g
    wlog! hsPoly_ne_0 : m.sPolynomial g₁.val.val g₂.val.val ≠ 0 generalizing
    · suffices (q g₁ g₂) g = 0 by simp [this, h_a_gt_zero]
      rw [← mul_left_mem_nonZeroDivisors_eq_zero_iff <|
          m.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors hG₀,
        h_q_eq_0_of_sPoly_eq_0 hsPoly_ne_0]
    rw [mul_assoc]
    apply lt_of_le_of_lt degree_mul_le
    rw [AddEquiv.map_add]
    refine add_lt_of_add_lt_right ?_ (degree_monomial_le _)
    /- $$... ≤ degree(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂))) - degree(lcm(lm(g₁), lm(g₂))) +
                degree(sPoly(g₁, g₂))$$ -/
    apply lt_of_le_of_lt (add_le_add_right (mul_comm g.val (q _ _ g) ▸ h_deg_gq_le_sPoly) _)
    /- $$... < degree(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂))) - degree(lcm(lm(g₁), lm(g₂))) +
                degree(lcm(lm(g₁), lm(g₂)))$$ -/
    apply lt_of_lt_of_le (add_lt_add_right (m.degree_sPolynomial_lt_sup_degree hsPoly_ne_0) _)
    /- $$... = degree(lcm(lm(f(g₁) * g₁), lm(f(g₂) * g₂)))$$ -/
    rw [← AddEquiv.map_add, tsub_add_cancel_of_le <| sup_le_sup (by simp) (by simp)]
    /- $$... ≤ a.$$ -/
    have hfgg₁ := (G'.mem_filter.mp g₁.2).2
    have hfgg₂ := (G'.mem_filter.mp g₂.2).2
    unfold degFgEqA at hfgg₁ hfgg₂
    rw [degree_mul_of_right_mem_nonZeroDivisors _ hG₀, ← m.toSyn.eq_symm_apply] at hfgg₁ hfgg₂
    · simp [hfgg₁, hfgg₂]
    all_goals
      by_contra! hfg0
      simp [hfg0, h_a_gt_zero.ne] at hfgg₁ hfgg₂
  · /- It is easy to prove $degree(f(g) - lt'(g)) < a$. -/
    wlog h : degFgEqA g
    · by_cases hg'G' : g ∈ G'
      · simp [h, lt', lt_of_le_of_ne (mul_comm (f g) g ▸ h_deg_le g hg'G') h]
      · simp [hg'G', h_a_gt_zero, lt', hf₀support]
    simp? [h, lt'] says simp only [h, ↓reduceIte, lt']
    wlog! +distrib hLTgg' : f g - m.leadingTerm (f g) ≠ 0
    · simp [hLTgg', h_a_gt_zero]
    rw [← h] at ⊢ h_a_gt_zero
    apply ne_of_lt at h_a_gt_zero
    rw [ne_eq, eq_comm, toSyn_eq_zero_iff] at h_a_gt_zero
    have : f g ≠ 0 := by
      have := m.ne_zero_of_degree_ne_zero h_a_gt_zero
      contrapose! this
      simp [this]
    simp [degree_mul_of_right_mem_nonZeroDivisors hLTgg' hG₀,
      degree_mul_of_right_mem_nonZeroDivisors this hG₀,
      m.degree_sub_leadingTerm_lt_degree (m.degree_ne_zero_of_sub_leadingTerm_ne_zero hLTgg')]

theorem isGroebnerBasis_iff_isRemainder_sPolynomial_zero₀
    {G : Set (MvPolynomial σ R)} (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g) ∨ g = 0) :
    m.IsGroebnerBasis G (Ideal.span G) ↔
      ∀ (g₁ g₂ : G), m.IsRemainder (m.sPolynomial g₁ g₂ : MvPolynomial σ R) G 0 := by
  rw [← isGroebnerBasis_sdiff_singleton_zero, ← Ideal.span_sdiff_singleton_zero,
    isGroebnerBasis_iff_isRemainder_sPolynomial_zero (G := G \ {0})
      (by simp_intro _ _ [or_iff_not_imp_right.mp (hG _ _)])]
  simp? [imp_forall_iff, imp.swap (a := ¬(_ : MvPolynomial σ R) = 0) (b := _ ∈ G)] says
    simp only [isRemainder_sdiff_singleton_zero_iff_isRemainder, Subtype.forall, Set.mem_diff,
      Set.mem_singleton_iff, ne_eq, and_imp, imp_forall_iff,
      imp.swap (a := ¬(_ : MvPolynomial σ R) = 0) (b := _ ∈ G)]
  congr! with p q - -
  by_cases! h : p = 0 ∨ q = 0
  · rcases h with h | h <;> simp [h]
  simp [h]

/-- Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if any
remainder of echo sPolynomial between two polynomials on the basis is 0.

It is a variant of
`MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero`. -/
theorem isGroebnerBasis_iff_forall_isRemainder_sPolynomial_zero {G : Set (MvPolynomial σ R)}
    (hG : ∀ g ∈ G, IsUnit (m.leadingCoeff g)) :
    m.IsGroebnerBasis G (Ideal.span G) ↔
    ∀ (g₁ g₂ : G) (r : MvPolynomial σ R),
      m.IsRemainder (m.sPolynomial g₁ g₂ : MvPolynomial σ R) G r → r = 0 := by
  constructor
  · intro h g₁ g₂ r hr
    apply (remainder_eq_zero_iff_mem_ideal h hr).mpr
    rw [isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero (hG := hG)] at h
    apply m.sPolynomial_mem_ideal
    <;> exact Set.mem_of_subset_of_mem h.1 (by simp)
  · rw [isGroebnerBasis_iff_isRemainder_sPolynomial_zero (hG := hG)]
    intro h g₁ g₂
    obtain ⟨r, hr⟩ := exists_isRemainder hG (m.sPolynomial (R := R) ↑g₁ ↑g₂)
    rwa [h g₁ g₂ r hr] at hr

-- todo: avoid requiring `hG`
lemma _root_.MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename {σ'}
    {m' : MonomialOrder σ'} {m : MonomialOrder σ}
    (e : Embedding m' m) (G : Set (MvPolynomial σ' R))
    (hG : ∀ g ∈ G, IsUnit (m'.leadingCoeff g))
    (I : Ideal (MvPolynomial σ' R)) :
    m'.IsGroebnerBasis G I ↔
      m.IsGroebnerBasis (MvPolynomial.rename e '' G) (I.map (MvPolynomial.rename e)) := by
  classical
  rw [isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span (hG := hG),
    isGroebnerBasis_iff_isRemainder_sPolynomial_zero (hG := hG),
    isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span (hG := by simpa using hG),
    isGroebnerBasis_iff_isRemainder_sPolynomial_zero (hG := by simpa using hG),
    and_congr]
  · constructor
    · intro rfl
      rw [Ideal.map_span]
    · intro h
      apply congrArg (Ideal.map (killCompl e.coe_injective)) at h
      simpa [Ideal.map_mapₐ, killCompl_comp_rename, Ideal.map_span, ← Set.image_comp] using h
  · simp [e.sPolynomial_rename, e.isRemainder_iff_isRemainder_rename]

-- todo: avoid requiring `hG`
lemma _root_.MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename₀ {σ'}
    {m' : MonomialOrder σ'} {m : MonomialOrder σ}
    (e : Embedding m' m) (G : Set (MvPolynomial σ' R))
    (hG : ∀ g ∈ G, IsUnit (m'.leadingCoeff g) ∨ g = 0)
    (I : Ideal (MvPolynomial σ' R)) :
    m'.IsGroebnerBasis G I ↔
      m.IsGroebnerBasis (MvPolynomial.rename e '' G) (I.map (MvPolynomial.rename e)) := by
  rw [← isGroebnerBasis_sdiff_singleton_zero,
    e.isGroebnerBasis_iff_isGroebnerBasis_rename
      (hG := by simp_intro .. [or_iff_not_imp_right.mp (hG _ _)]),
    Set.image_diff (rename_injective _ e.coe_injective)]
  simp

-- lemma _root_.MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename'' {σ'}
--     {m' : MonomialOrder σ'} {m : MonomialOrder σ}
--     (e : Embedding m' m) (G : Set (MvPolynomial σ' R))
--     (I : Ideal (MvPolynomial σ' R)) :
--     m'.IsGroebnerBasis G I ↔
--       m.IsGroebnerBasis (MvPolynomial.rename e '' G) (I.map (MvPolynomial.rename e)) := by
--   classical
--   apply and_congr
--   · refine ⟨fun h ↦ subset_trans (Set.image_mono h) Ideal.subset_span, ?_⟩
--     intro h
--     apply Set.image_mono (f := killCompl e.coe_injective) at h
--     apply (subset_trans · Ideal.subset_span) at h
--     rw [← Ideal.map, Ideal.map_mapₐ, Set.image_image] at h
--     simpa [killCompl_comp_rename] using h
--   · simp_rw [Set.image_image, e.leadingTerm_rename, ← Set.image_image]
--     #check Submodule.exists_finset_of_mem_iSup
--     sorry

end CommRing

section Field

variable {k : Type*} [Field k] {σ : Type*} {m : MonomialOrder σ}

/-- A set of polynomials is a Gröbner basis of an ideal if and only if it is a subset of this ideal
and 0 is a remainder of each member of this ideal on division by this set.

It is a variant of
`MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero`,
over a field and without hypothesis on leading coefficients in the set. -/
theorem isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero'
    (G : Set (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) :
    m.IsGroebnerBasis G I ↔ G ⊆ I ∧ ∀ p ∈ I, m.IsRemainder p G 0 :=
  isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero₀ G I (by simp [em'])

lemma isRemainder_zero_iff_mem_ideal' {p : MvPolynomial σ k}
    {G : Set (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)} (h : m.IsGroebnerBasis G I) :
    m.IsRemainder p G 0 ↔ p ∈ I := by
  refine isRemainder_zero_iff_mem_ideal₀ ?_ h
  simp [em']

/-- Buchberger Criterion: a basis of an ideal is a Gröbner basis of it if and only if any
remainder of echo sPolynomial between two polynomials on the basis is 0.

It is a variant of
`MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero`. -/
theorem isGroebnerBasis_iff_isRemainder_sPolynomial_zero' (G : Set (MvPolynomial σ k)) :
    m.IsGroebnerBasis G (Ideal.span G) ↔
    ∀ (g₁ g₂ : G) (r : MvPolynomial σ k),
      m.IsRemainder (m.sPolynomial g₁ g₂ : MvPolynomial σ k) G r → r = 0 := by
  constructor
  · intro h g₁ g₂ r hr
    apply (remainder_eq_zero_iff_mem_ideal h hr).mpr
    rw [isGroebnerBasis_iff_subset_ideal_and_isRemainder_zero'] at h
    apply m.sPolynomial_mem_ideal
    <;> exact Set.mem_of_subset_of_mem h.1 (by simp)
  · rw [isGroebnerBasis_iff_isRemainder_sPolynomial_zero₀ (hG := by simp [em'])]
    intro h g₁ g₂
    obtain ⟨r, hr⟩ := exists_isRemainder' G (m.sPolynomial (R := k) ↑g₁ ↑g₂)
    rwa [h g₁ g₂ r hr] at hr

theorem isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span' (G : Set (MvPolynomial σ k))
    (I : Ideal (MvPolynomial σ k)) :
    m.IsGroebnerBasis G I ↔ (I = Ideal.span G ∧ m.IsGroebnerBasis G (Ideal.span G)) :=
  isGroebnerBasis_iff_ideal_eq_span_and_isGroebnerBasis_span₀ G I (by simp [em'])

theorem isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le'
    (G : Set (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k)) :
    m.IsGroebnerBasis G I ↔
      G ⊆ I ∧ ∀ p ∈ I, p ≠ 0 → ∃ g ∈ G, g ≠ 0 ∧ m.degree g ≤ m.degree p :=
  isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le₀ I (by simp [em'])

--- lemma _root_.MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename {σ'}
---     {m' : MonomialOrder σ'} {m : MonomialOrder σ}
---     (e : Embedding m' m) (G : Set (MvPolynomial σ' R))
---     (I : Ideal (MvPolynomial σ' R)) :
---     m'.IsGroebnerBasis G I ↔
---       m.IsGroebnerBasis (MvPolynomial.rename e '' G) (I.map (MvPolynomial.rename e)) := by
---   classical
---   apply and_congr
---   · refine ⟨fun h ↦ subset_trans (Set.image_mono h) Ideal.subset_span, ?_⟩
---     intro h
---     apply Set.image_mono (f := killCompl e.coe_injective) at h
---     apply (subset_trans · Ideal.subset_span) at h
---     rw [← Ideal.map, Ideal.map_mapₐ, Set.image_image] at h
---     simpa [killCompl_comp_rename] using h
---   · simp_rw [Set.image_image, e.leadingTerm_rename, ← Set.image_image]
---     sorry

lemma _root_.MonomialOrder.Embedding.isGroebnerBasis_iff_isGroebnerBasis_rename' {σ'}
    {m' : MonomialOrder σ'} {m : MonomialOrder σ}
    (e : Embedding m' m) (G : Set (MvPolynomial σ' k))
    (I : Ideal (MvPolynomial σ' k)) :
    m'.IsGroebnerBasis G I ↔
      m.IsGroebnerBasis (MvPolynomial.rename e '' G) (I.map (MvPolynomial.rename e)) :=
  e.isGroebnerBasis_iff_isGroebnerBasis_rename₀ (hG := by simp [em']) ..

-- todo: generalize to ring.
lemma exists_isGroebnerBasis_finite_of_exists_span_finite
    {B : Set (MvPolynomial σ k)} (hB : B.Finite) :
    ∃ G : Set (MvPolynomial σ k), m.IsGroebnerBasis G (Ideal.span B) ∧ G.Finite := by
  classical
  let σ' := hB.toFinset.biUnion MvPolynomial.vars
  let m' := m.ofInjective (σ' := σ') (Subtype.val_injective)
  let emb : m'.Embedding m := MonomialOrder.Embedding.ofInjective m Subtype.val_injective
  have ⟨G', hG', hG'finite⟩ :=
    exists_isGroebnerBasis_finite (m := m') ((Ideal.span B).map (killCompl emb.coe_injective))
  use rename emb '' G'
  refine ⟨?_, hG'finite.image ..⟩
  rwa [emb.isGroebnerBasis_iff_isGroebnerBasis_rename', Ideal.map_mapₐ, Ideal.map_span,
    AlgHom.coe_comp, Function.comp_def, Set.image_congr (g := id), Set.image_id] at hG'
  intro p hpB
  apply p.rename_killCompl_app
  rw [Embedding.coe_ofInjective, Subtype.range_coe, SetLike.coe_subset_coe]
  apply Finset.subset_biUnion_of_mem vars (hB.mem_toFinset.mpr hpB)

lemma isGroebnerBasis_of_forall_finite_isGroebnerBasis' {G : Set (MvPolynomial σ k)}
    {I : Ideal (MvPolynomial σ k)}
    (h : ∀ s : Finset σ,
      ∃ (σ' : Type*), ∃ m' : MonomialOrder σ', ∃ e : m'.Embedding m,
        ↑s ⊆ Set.range e ∧ m'.IsGroebnerBasis (rename e ⁻¹' G) (I.comap (rename e))) :
    m.IsGroebnerBasis G I :=
  isGroebnerBasis_of_forall_finite_isGroebnerBasis₀ (hG := by simp_intro .. [em']) h

theorem isGroebnerBasis_union_of_forall_finite_isGroebnerBasis'
    {I : Ideal (MvPolynomial σ k)} {σ' : Finset σ → Type*}
    {m' : (s : Finset σ) → MonomialOrder (σ' s)}
    {e : (s : Finset σ) → (m' s).Embedding m}
    {G' : (s : Finset σ) → Set (MvPolynomial (σ' s) k)}
    (h : ∀ s, ↑s ⊆ Set.range (e s))
    (h' : ∀ s, (m' s).IsGroebnerBasis (G' s) (I.comap <| rename (e s))) :
    m.IsGroebnerBasis (⋃ s : Finset σ, rename (e s) '' G' s) I :=
  isGroebnerBasis_union_of_forall_finite_isGroebnerBasis₀ (by simp_intro .. [em']) h h'

-- todo: generalize to ring?
lemma isGroebnerBasis_iff_minimal (I : Ideal (MvPolynomial σ k))
    {G : Set (MvPolynomial σ k)} :
    m.IsGroebnerBasis G I ↔ G ⊆ I ∧
      {a | Minimal (· ∈ m.degree '' ((I : Set (MvPolynomial σ k)) \ {0})) a} ⊆
        m.degree '' (G \ {0}) := by
  classical
  constructor
  · intro h
    rw [IsGroebnerBasis.isGroebnerBasis_iff_subset_and_degree_le_eq_and_degree_le'] at h
    exists h.1
    intro a ha
    -- by_contra! h'
    simp at ha ⊢
    obtain ⟨p, hp, rfl⟩ := ha.prop
    obtain ⟨g, hg⟩ := h.2 p hp.1 hp.2
    refine ⟨g, ⟨hg.1, hg.2.1⟩, ?_⟩
    exact ha.eq_of_le ⟨g, ⟨h.1 hg.1, hg.2.1⟩, rfl⟩ hg.2.2
  · intro h
    rw [isGroebnerBasis_iff]
    exists h.1
    rw [--← span_leadingTerm_sdiff_singleton_zero, ← span_leadingTerm_sdiff_singleton_zero (B := G),
      ← Ideal.span_le,
      span_leadingTerm_eq_span_monomial', span_leadingTerm_eq_span_monomial',
      -- span_leadingTerm_eq_span_monomial (G := G \ {0}),
      ← Set.image_image (g := (monomial · (1 : k))) (f := m.degree),
      ← Set.image_image (g := (monomial · (1 : k))) (f := m.degree),
      ideal_span_monomial_image_eq_ideal_span_monomial_image_minimal,
      --ideal_span_monomial_image_eq_ideal_span_monomial_image_minimal (s := m.degree '' (G \ {0})),
      Ideal.span_le]
    intro p
    rw [SetLike.mem_coe, mem_ideal_span_monomial_image, Set.mem_image]
    rintro ⟨a, ⟨ha, rfl⟩⟩
    obtain ⟨p, ⟨hp, rfl⟩⟩ := h.2 ha
    simp [support_monomial]
    exact ⟨p, And.intro hp (le_refl (m.degree p))⟩

end Field

end IsGroebnerBasis

end MonomialOrder