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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
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 (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
Heval' : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S (Option.some i)) → Polynomial.map (eval x) Q = 0
m : ℕ
d : σ →₀ ℕ
i : σ
e : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some e).update none m
he : n ∈ P.support
hn : n none = m ∧ n.some = e
⊢ n (Option.some i) = n (Option.some i)

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
half_sharp :
  (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum +
      (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum + (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum

Tactic:
]

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
half_sharp :
  (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
⊢ (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum +
      (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum + (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h_option.Heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
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 (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
m : ℕ
d : σ →₀ ℕ
x : σ → R
Heval' : ∀ (n : ℕ), (Polynomial.map (eval x) Q).coeff n = Polynomial.coeff 0 n
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (eval x) (Q.coeff m) = 0

Tactic:
]

Goal state after:
case h_option.Heval
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
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 (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
m : ℕ
d : σ →₀ ℕ
x : σ → R
Heval' : ∀ (n : ℕ), (Polynomial.map (eval x) Q).coeff n = Polynomial.coeff 0 n
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (eval x) (Q.coeff m) = 0
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r = q * b + r

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r = q * b + r
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∑ i_1 ∈ S, m.degree (X i - C i_1) = single i #S

pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∑ i_1 ∈ S, m.degree (X i - C i_1) = single i #S

R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
r : R
a✝ : r ∈ S
⊢ IsRegular 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
r : R
a✝ : r ∈ S
⊢ IsRegular 1
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False

Tactic:
]

Goal state after:
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
sharp :
  2 • (Multiset.map (fun x ↦ f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum <
    2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum
impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]
rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]
distrib : (Multiset.map (fun x ↦ f ![a, b]) ω).sum = ω.size • f ![a, b]
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ g ⟨b, ⋯⟩ * ↑⟨b, ⋯⟩ = q * b

pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∀ (b_1 : ↑{b}), g b_1 ≠ 0 → b_1 ≠ ⟨b, ⋯⟩ → g b_1 * ↑b_1 = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : ↑{b} →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr : f = (Finsupp.linearCombination (MvPolynomial σ R) fun b_1 ↦ ↑b_1) g + r
q : MvPolynomial σ R := g ⟨b, ⋯⟩
h1 : m.toSyn (m.degree (b * q)) ≤ m.toSyn (m.degree f)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∀ (b_1 : ↑{b}), g b_1 ≠ 0 → b_1 ≠ ⟨b, ⋯⟩ → g b_1 * ↑b_1 = 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ Finset.image (mapDomain fun x ↦ i) (P S ()).support
hP : P S i = (rename fun x ↦ i) (P S ())
⊢ ∃ e ≤ #S, m = single i e

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hm : m ∈ Finset.image (mapDomain fun x ↦ i) (P S ()).support
hP : P S i = (rename fun x ↦ i) (P S ())
⊢ ∃ e ≤ #S, m = single i e
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ lex.toSyn e ≤ lex.toSyn (MonomialOrder.degree ?refine_1.m (P S ()))

pp: case refine_1.m
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ MonomialOrder Unit

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ lex.toSyn e ≤ lex.toSyn (MonomialOrder.degree ?refine_1.m (P S ()))

case refine_1.m
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ MonomialOrder Unit
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ coeff e (P S ()) ≠ 0

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ coeff e (P S ()) ≠ 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ mapDomain (fun x ↦ i) e = single i (e ())

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ mapDomain (fun x ↦ i) e = single i (e ())
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : j = i
⊢ e ?pos.a✝ = e ()

pp: case pos.a
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : j = i
⊢ Unit

Tactic:
]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ 0 = 0

pp: case neg.h
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ j ∉ Set.range fun x ↦ i

Tactic:
]

Goal state after:
case neg.h
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
j : ι
hj : ¬j = i
⊢ j ∉ Set.range fun x ↦ i
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
this : r = 0
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
this : r = 0
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Hdeg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
i : σ
⊢ ∀ b ∈ r.support, b i < #(S i)

Tactic:
]

Goal state after:
case h.Hdeg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
i : σ
⊢ ∀ b ∈ r.support, b i < #(S i)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ (eval x) r = 0

Tactic:
]

Goal state after:
case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ (eval x) r = 0
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : p'.vertices.length = p'.length + 1
⊢ (p'.cons e).vertices.length = (p'.cons e).length + 1

Tactic:
| cons p' e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : a ∈ p'.vertices
⊢ a ∈ (p'.cons e).vertices

Tactic:
| cons p' e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : p'.vertices.head? = some a
⊢ (p'.cons e).vertices.head? = some a

Tactic:
| cons p' e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
]

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : p'.vertices[0] = a
⊢ (p'.cons e).vertices[0] = a

Tactic:
| cons p' e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b b✝ c✝ : V
p' : Path a b✝
e : b✝ ⟶ c✝
ih : ∀ (h : p'.vertices ≠ []), p'.vertices.getLast h = b✝
h : (p'.cons e).vertices ≠ []
⊢ (p'.cons e).vertices.getLast h = c✝

Tactic:
| cons p' e ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

Tactic:
]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)

Tactic:
]

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ 0 = 0

pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ ∀ x_1 ∈ h.support, (eval x) (h x_1 • Alon.P (S x_1) x_1) = 0

Tactic:
]

Goal state after:
case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ ∀ x_1 ∈ h.support, (eval x) (h x_1 • Alon.P (S x_1) x_1) = 0
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n

Tactic:
]

Goal state after:
case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
⊢ ∃ v p₁ p₂, p'.cons e = p₁.comp p₂ ∧ p₁.length = n