mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
ε : ℝ
ε0 : 0 < ε
δ₁ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₁ c x ε) →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
δ₂ : ℝ≥0 → (ι → ℝ) → ℝ → { a // 0 < a }
Hδ₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ (ε : ℝ),
        0 < ε →
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x ↑(δ₂ c x ε) →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε0' : 0 < ε / 2
H0 : 0 < 2 ^ Fintype.card ι
εs : (ι → ℝ) → ℝ
hεs0 : ∀ (i : ι → ℝ), 0 < εs i
hεs : ∀ (t : Finset (ι → ℝ)), ↑t ⊆ s → ∑ i ∈ t, 2 ^ Fintype.card ι * εs i ≤ ε / 2
ε' : ℝ
ε'0 : 0 < ε'
hεI : B I * ε' < ε / 2
δ : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ if x ∈ s then δ₁ c x (εs x) else δ₂ c x ε'
π : TaggedPrepartition I
c : ℝ≥0
hπδ : l.MemBaseSet I c (δ c) π
hπp : π.IsPartition
⊢ B I * ε' = B I * ε'

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) →
    (fun x ↦ degree (ofDegLex x)) x ≤ (fun x ↦ degree (ofDegLex x)) y

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) →
    (fun x ↦ degree (ofDegLex x)) x ≤ (fun x ↦ degree (ofDegLex x)) y
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (monomial n) a = (monomial n) a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (∃ m r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r) ↔ ∃ m b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

Tactic:
]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ (∃ m r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r) ↔ ∃ m b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : ∃ b, b ∣ a ∧ r = C b
h : p = (monomial m) 1 * r
⊢ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

Tactic:
]

Goal state after:
case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : ∃ b, b ∣ a ∧ r = C b
h : p = (monomial m) 1 * r
⊢ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree a + degree (b - a)

Tactic:
]

Goal state after:
case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree a + degree (b - a)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ b ≤ a ↔ b ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m) 1 * r
b : R
hb : b ∣ a
hr : r = C b
⊢ (monomial m) b = (monomial m) b

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ b < a ↔ b < a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ 0 < 1

Tactic:
]

Goal state after:
α : Type u_1
⊢ 0 < 1
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ degree (single 0 1 + single 1 1) < degree (ofDegLex (toDegLex (single 0 2))) ∨
    degree (single 0 1 + single 1 1) = degree (ofDegLex (toDegLex (single 0 2))) ∧
      toLex (single 0 1 + single 1 1) < toLex (ofDegLex (toDegLex (single 0 2)))

Tactic:
]

Goal state after:
α : Type u_1
⊢ degree (single 0 1 + single 1 1) < degree (ofDegLex (toDegLex (single 0 2))) ∨
    degree (single 0 1 + single 1 1) = degree (ofDegLex (toDegLex (single 0 2))) ∧
      toLex (single 0 1 + single 1 1) < toLex (ofDegLex (toDegLex (single 0 2)))
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m) b
⊢ p = (monomial m) b

Tactic:
]

Goal state after:
case right
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m) b
⊢ p = (monomial m) b
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ (∃ m b, m ≤ n ∧ b ∣ 1 ∧ p = (monomial m) b) ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u

Tactic:
]

Goal state after:
case inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ (∃ m b, m ≤ n ∧ b ∣ 1 ∧ p = (monomial m) b) ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ (∃ b, ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b) ↔
    ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)

Tactic:
]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ (∃ b, ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b) ↔
    ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ {r ∈ piFinset S | P (init r)} = map (snocEquiv α).toEmbedding (S (last n) ×ˢ {r ∈ piFinset (init S) | P r})

Tactic:
simp [← map_snocEquiv_filter_piFinset, map_map]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (tail r)}) = #({r ∈ piFinset S | P (tail r)})

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (init r)}) = #({r ∈ piFinset S | P (init r)})

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ #({r ∈ piFinset S | P (p.removeNth r)}) = #({r ∈ piFinset S | P (p.removeNth r)})

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case pos
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : m i = 0
j : σ
hj : j = i
⊢ m i ≤ m i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
a✝ : Nontrivial R
⊢ (∃ s, s ∣ 1 ∧ (p = C s ∨ p = s • X i)) ↔ ∃ r, IsUnit r ∧ (p = C r ∨ p = r • 1 • X i)

Tactic:
]

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
a✝ : Nontrivial R
⊢ (∃ s, s ∣ 1 ∧ (p = C s ∨ p = s • X i)) ↔ ∃ r, IsUnit r ∧ (p = C r ∨ p = r • 1 • X i)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
a✝ : Nontrivial R
r : R
⊢ r ∣ 1 ∧ (p = C r ∨ p = r • X i) ↔ r ∣ 1 ∧ (p = C r ∨ p = r • X i)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (monomial (m.degree p)) (m.leadingCoeff p) = (monomial (m.degree p)) (m.leadingCoeff p)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : MvPolynomial σ R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ Finsupp.single s 1 = Finsupp.single s 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ c = 1 ↔ c = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
⊢ coeff d f = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬m.toSyn d ≤ m.toSyn (m.degree f)
⊢ coeff d f = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f = 0 → m.leadingCoeff f = 0

Tactic:
]

Goal state after:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f = 0 → m.leadingCoeff f = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0

Tactic:
]

Goal state after:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support

Tactic:
]

Goal state after:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ ↑f.support
hd' : m.toSyn d = f.support.sup ⇑m.toSyn
⊢ d ∈ f.support

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ ↑f.support
hd' : m.toSyn d = f.support.sup ⇑m.toSyn
⊢ d ∈ f.support
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
⊢ p ≠ 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
⊢ p ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = m.toSyn 0 ↔ f.totalDegree = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = m.toSyn 0 ↔ f.totalDegree = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ≤ m.toSyn 0 ↔ f.totalDegree = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ≤ m.toSyn 0 ↔ f.totalDegree = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ f.totalDegree = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ f.totalDegree = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ ∀ m ∈ f.support, ∀ (x : σ), m x = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ ∀ m ∈ f.support, ∀ (x : σ), m x = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d = 0 ↔ ∀ (x : σ), d x = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d = 0 ↔ ∀ (x : σ), d x = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = 0

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ 0 ≤ m.toSyn d ∧ ¬d = 0

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ 0 ≤ m.toSyn d ∧ ¬d = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : f = C (m.leadingCoeff f)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.toSyn.symm (max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))))

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.toSyn.symm (max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))
⊢ m.toSyn (m.degree (f a + ∑ x ∈ s, f x)) ≤ max (m.toSyn (m.degree (f a))) (s.sup fun x ↦ m.toSyn (m.degree (f x)))

Tactic:
]

Goal state after:
case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))
⊢ m.toSyn (m.degree (f a + ∑ x ∈ s, f x)) ≤ max (m.toSyn (m.degree (f a))) (s.sup fun x ↦ m.toSyn (m.degree (f x)))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ f ≠ 0

Tactic:
]

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ f ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ False

Tactic:
]

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.degree (g + f) = m.degree g

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.degree (g + f) = m.degree g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.degree f = m.degree g → m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f * g).support, m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f * g).support, m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ m.toSyn (m.degree f + m.degree g) < m.toSyn c → coeff c (f * g) = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ m.toSyn (m.degree f + m.degree g) < m.toSyn c → coeff c (f * g) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ ∑ x ∈ Finset.antidiagonal c, coeff x.1 f * coeff x.2 g = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ ∑ x ∈ Finset.antidiagonal c, coeff x.1 f * coeff x.2 g = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Euclidean

Goal state before:
pp: x y : ℤ
⊢ x.natAbs < y.natAbs ↔ x.natAbs < y.natAbs

Tactic:
]

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0

Tactic:
]

Goal state after:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
this : m.toSyn (m.degree g) < m.toSyn e
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))

Tactic:
]

Goal state after:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)

Tactic:
]

Goal state after:
α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ (Fintype.card α + k - 1).choose k = (Fintype.card α + k - 1).choose k

Tactic:
]

Goal state after: