mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ⋯.choose ∈ s

pp: case refine_2
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
i : ι
⊢ ↥S → M

pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, (Option.map ?refine_2 (l.idxFun i)).getD 0) = c

Tactic:
·

Goal state after:
case refine_1
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ⋯.choose ∈ s
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : m.reduce hb f = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ False

Tactic:
H',

Goal state after:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : m.reduce hb f = 0
K : m.degree 0 = m.degree f
⊢ False
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
i : ι
⊢ ↥S → M

pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
⊢ ∀ s_1 ∈ S, C (#s • s_1 + ∑ i ∈ sᶜ, (Option.map ?refine_2 (l.idxFun i)).getD 0) = c

Tactic:
·

Goal state after:
case refine_2
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
i : ι
⊢ ↥S → M
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁ ∪ ∅)

Tactic:
union_empty

Goal state after:
case inr
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B₁ B₂ : Set ((i : ι) × α i)
h₁ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₁
h₂ : (fun B ↦ ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)) B₂
i : ι
e : α i
he₁ : ⟨i, e⟩ ∈ B₁
he₂ : ⟨i, e⟩ ∉ B₂
f : α i
hfB : (M i).IsBase (insert f (Sigma.mk i ⁻¹' B₁ \ {e}))
hf₁ : f ∈ Sigma.mk i ⁻¹' B₂
hf₂ : f ∉ Sigma.mk i ⁻¹' B₁
j : ι
hne : i ≠ j
⊢ (M j).IsBase (Sigma.mk j ⁻¹' B₁)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.Indep I
hB : (M ／ I).IsBasis J X
⊢ M.IsBasis (J ∪ I) (X ∪ I)

Tactic:
simp_rw [IsBasis, hI.contract_indep_iff, contract_ground, subset_sdiff,
    maximal_subset_iff, and_imp] at hB
  refine hB.1.1.1.2.isBasis_of_maximal_subset (union_subset_union_left _ hB.1.1.2)
    fun K hK hKJ hKX ↦ ?_
  rw [union_subset_iff] at hKJ
  rw [hB.1.2 (t := K \ I) disjoint_sdiff_left (by simpa [sdiff_union_of_subset hKJ.2])
    (sdiff_subset_iff.2 (by rwa [union_comm])) (subset_sdiff.2 ⟨hKJ.1, hB.1.1.1.1⟩),
    sdiff_union_of_subset hKJ.2]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case h.refine_1
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ I ⊆ univ.sigma Js

pp: case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X

pp: case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js

Tactic:
·

Goal state after:
case h.refine_1
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ I ⊆ univ.sigma Js
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∃ i, m.degree (b i) = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∃ i, m.degree (b i) = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J \ I ⊆ Y \ X

pp: case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ Y \ X ⊆ Y \ I

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J \ I ⊆ Y \ X
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X

pp: case h.refine_3
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
S : Set ((i : ι) × α i)
hS : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' S)
hSX : S ⊆ X
hJS : univ.sigma Js ⊆ S
⊢ S ⊆ univ.sigma Js

Tactic:
·

Goal state after:
case h.refine_2
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
X : Set ((i : ι) × α i)
x✝ : X ⊆ univ.sigma fun i ↦ (M i).E
I : Set ((i : ι) × α i)
hI : (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) I
hIX : I ⊆ X
Js : (i : ι) → Set (α i)
hJs : ∀ (i : ι), (M i).IsBasis' (Js i) (Sigma.mk i ⁻¹' X) ∧ Sigma.mk i ⁻¹' I ⊆ Js i
⊢ univ.sigma Js ⊆ X
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ #s • x = ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i)

pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ∑ i ∈ sᶜ, ↑(↑l ⟨x, xs⟩ i)

Tactic:
·

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ #s • x = ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ #s • x = ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i)

Tactic:
← Finset.sum_const

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ _x ∈ s, x = ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ f = (Finsupp.linearCombination (MvPolynomial σ R) b) (Finsupp.single i (⋯.unit⁻¹ • f)) + 0

pp: case h.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)) ∧
    ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
·

Goal state after:
case h.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ f = (Finsupp.linearCombination (MvPolynomial σ R) b) (Finsupp.single i (⋯.unit⁻¹ • f)) + 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ (X ∩ M.E ∩ Iᶜ) = M ／ I ＼ ((X ∩ M.E) \ I)

Tactic:
← sdiff_eq

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ ((X ∩ M.E) \ I) = M ／ I ＼ ((X ∩ M.E) \ I)
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ∑ i ∈ sᶜ, ↑(↑l ⟨x, xs⟩ i)

Tactic:
·

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ∑ i ∈ sᶜ, ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)

pp: case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
·

Goal state after:
case h.right.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * (Finsupp.single i (⋯.unit⁻¹ • f)) i_1)) ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ J)

pp: case refine_3
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (I \ C) J

pp: case refine_4
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) J

pp: case refine_5
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ Disjoint (X \ C) (C \ J)

pp: case refine_1
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ I \ C ∪ J ⊆ X \ C ∪ J

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I J X C : Set α
h : M.IsBasis I X
hJC : M.IsBasis' J C
h_ind : M.Indep (I \ C ∪ J)
hIX : I ⊆ X
hJCss : J ⊆ C
⊢ X \ C ∪ J ⊆ M.closure (I \ C ∪ J)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
·

Goal state after:
case h.right.right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ ∀ c ∈ support 0, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : f = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : f = 0
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∃ i, m.degree (b i) ≤ m.degree f
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
hf : ∃ i, m.degree (b i) ≤ m.degree f
⊢ ∃ g r,
    f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧
      (∀ (i : ι), m.toSyn (m.degree (b i * g i)) ≤ m.toSyn (m.degree f)) ∧
        ∀ c ∈ r.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case of_equiv.Hdeg
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ ∀ (i : σ), degreeOf i ((rename ⇑e.symm) P) < #(S (e i))

pp: case of_equiv.Heval
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (e i)) → (eval x) ((rename ⇑e.symm) P) = 0

Tactic:
·

Goal state after:
case of_equiv.Hdeg
R : Type u_1
inst✝² : CommRing R
σ✝ : Type u_2
inst✝¹ : Finite σ✝
inst✝ : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval : ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → (eval x) P = 0
⊢ ∀ (i : σ), degreeOf i ((rename ⇑e.symm) P) < #(S (e i))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∈ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

pp: case neg
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∉ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
heI : e ∈ I
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C