mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! ≤
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (multinomial s fun i ↦ 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
⊢ p = q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
⊢ p = q → ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
σ : Type u_2
p q : MvPolynomial σ R
⊢ p = q → ∀ (x : σ → R), (eval x) p = (eval x) q

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ Multiset.replicate (↑m) x
⊢ ¬x ≠ j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ ↑s
h : x = j
⊢ x ∈ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ (↑(fill x m s)).countPerms = n.choose ↑m * (↑s).countPerms

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ ∀ i ∈ s, id 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ ∀ i ∈ s, 0! = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ Nat.multinomial s ⇑d = d.multinomial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ∀ a ∈ (Finsupp.single 0 x).support ∪ (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).support, 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ∀ a ∈ (Finsupp.single 0 x).support ∪ (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).support,
    ∀ (b₁ b₂ : α), b₁ + b₂ = b₁ + b₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l : List α
⊢ (l.toFinsupp.sum fun x a ↦ a) = l.sum

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
⊢ (Finsupp.single 0 x + Finsupp.embDomain succEmb l.toFinsupp).update 0 0 =
    (Finsupp.embDomain succEmb l.toFinsupp).update 0 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x✝ : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (Finsupp.single 0 x✝ + Finsupp.embDomain succEmb l.toFinsupp).update 0 0 =
    (Finsupp.embDomain succEmb l.toFinsupp).update 0 0
x : ℕ
⊢ succEmb x = x + 1

Tactic:
by

Goal state after:
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 : 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
hsne : s.Nonempty
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J ∈ s}
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ εs (π.tag J)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x✝ : ℕ
l : List ℕ
succEmb : ℕ ↪ ℕ := addRightEmbedding 1
this :
  (Finsupp.single 0 x✝ + Finsupp.embDomain succEmb l.toFinsupp).update 0 0 =
    (Finsupp.embDomain succEmb l.toFinsupp).update 0 0
x : ℕ
⊢ (Finsupp.embDomain succEmb l.toFinsupp) (x + 1) = l[x]?.getD 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x : ℕ
l : List ℕ
⊢ (x :: l).multinomial = (x + l.sum).choose x * l.multinomial

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ GameAdd rβ rα (a₁, b₁).swap (a₂, b₂).swap ↔ GameAdd rα rβ (a₁, b₁) (a₂, b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
h : RProd rα rβ x✝¹ x✝
⊢ ∀ {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, rα a₁ a₂ → rβ b₁ b₂ → Relation.TransGen (GameAdd rα rβ) (a₁, b₁) (a₂, b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a : α
b : β
ha : Acc rα a
hb : Acc rβ b
⊢ Acc (Prod.GameAdd rα rβ) (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m : Multiset ℕ
l l' : List ℕ
h : (List.isSetoid ℕ) l l'
⊢ l.multinomial = l'.multinomial

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂ b₂ =
      (fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) b₁ a₁ a₂ b₂ ∧
    (fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ a₂ b₂ =
      (fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) a₁ b₁ b₂ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: x : ℕ
m : Multiset ℕ
⊢ (x ::ₘ m).multinomial = (x + m.sum).choose x * m.multinomial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: n : ℕ
⊢ {n}.multinomial = 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
⊢ ∀ {x y : α × α}, GameAdd rα s(x.1, x.2) s(y.1, y.2) ↔ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(b, a₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(a₂, b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m m' : Multiset ℕ
⊢ (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
rα : α → α → Prop
a b : α
ha : Acc rα a
hb : Acc rα b
⊢ Acc (Sym2.GameAdd rα) s(a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a✝ : α
b✝ : β
C : α → α → Sort u_3
hr : WellFounded rα
IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁
a b : α
⊢ WellFounded fun x y ↦ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ k ∉ Finset.range k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: k : ℕ
m : Multiset ℕ
⊢ (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: k n : ℕ
⊢ (k • {n}).multinomial = Nat.multinomial (Finset.range k) fun x ↦ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m : Multiset ℕ
⊢ 0 < m.multinomial

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finsupp.WellFounded

Goal state before:
pp: α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) a
⊢ Acc (Finsupp.Lex r s) x

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn a + m.toSyn b

Tactic:
rw [← map_add]
  exact m.toSyn_monotone le_self_add

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn a + m.toSyn b

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : m.syn
⊢ 0 ≤ a

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
⊢ StrictMono ⇑m.toSyn

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot (σ →₀ ℕ)
⊢ m.toWithBotSyn a = ⊥ ↔ a = ⊥

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot (σ →₀ ℕ)
⊢ m.toWithBotSyn a ≤ ⊥ ↔ a = ⊥

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot (σ →₀ ℕ)
⊢ ⊥ < m.toWithBotSyn a ↔ ⊥ < a

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot m.syn
⊢ m.toWithBotSyn.symm a = ⊥ ↔ a = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_1
N : Type u_2
inst✝³ : LinearOrder α
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedCancelAddMonoid N
a b : Lex (α →₀ N)
h : a ≤ b
c : Lex (α →₀ N)
⊢ a + c ≤ b + c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
N : Type u_2
inst✝³ : LinearOrder α
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedCancelAddMonoid N
a b c : Lex (α →₀ N)
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
by

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

Goal state before:
pp: ⊢ toLex (single 0 2) > toLex (single 0 1 + single 1 1)

Tactic:
by

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

Goal state before:
pp: ⊢ toLex (single 1 1) < toLex (single 0 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
⊢ Fibration (InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd) (DFinsupp.Lex r s) fun x ↦
    x.2.1.piecewise x.2.2 x.1

Tactic:
by

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

Goal state before:
pp: ⊢ toLex (single 1 1) < toLex (single 0 2)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : LinearOrder σ
inst✝ : Unique σ
c d : σ →₀ ℕ
⊢ lex.toSyn c < lex.toSyn d ↔ c default < d default

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
inst✝¹ : LinearOrder σ
inst✝ : Unique σ
c d : σ →₀ ℕ
⊢ lex.toSyn c ≤ lex.toSyn d ↔ c default ≤ d default

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : x.support = insert b t
h : ∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))
⊢ (erase b x).support = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ (∀ i ∈ x.support, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i : ι
hi : Acc (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) i
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
hr : WellFounded (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
⊢ WellFounded (Pi.Lex r fun {i} ↦ s i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
⊢ WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 ↦ x1 < x2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
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
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J ∉ s}
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ ε' * B J

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Trichotomous r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
⊢ WellFounded (Finsupp.DegLex r s)

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
⊢ Finsupp.degree (degLex.degree f) = f.totalDegree

Tactic:
by

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f g : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
h : degLex.toSyn (degLex.degree f) ≤ degLex.toSyn (degLex.degree g)
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : DegLex (α →₀ ℕ)
⊢ a < b ↔
    degree (ofDegLex a) < degree (ofDegLex b) ∨
      degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : DegLex (α →₀ ℕ)
⊢ ¬a < a

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
a : ι
s : Finset ι
a_not_mem : a ∉ s
ih : (∀ i ∈ s, f i ≠ 0) → degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)
ha : ¬f a = 0
hs : ∀ a ∈ s, ¬f a = 0
⊢ ?m.84 ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
h : ∀ i ∈ s, f i ≠ 0
⊢ degreeOf n (∏ i ∈ s, f i) = ∑ i ∈ s, degreeOf n (f i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ degreeOf i (p ^ n) = n * degreeOf i p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degrees = p.degrees + q.degrees

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f * g).totalDegree = f.totalDegree + g.totalDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ r ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a b c : DegLex (α →₀ ℕ)), a < b → b < c → a < c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ∣ g
hg : g ≠ 0
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f g : DegLex (α →₀ ℕ)
⊢ (fun f ↦ toLex (degree (ofDegLex f), toLex (ofDegLex f))) f =
      (fun f ↦ toLex (degree (ofDegLex f), toLex (ofDegLex f))) g →
    f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
this : f.totalDegree = 0
⊢ coeff 0 f ∣ a ∧ f = C (coeff 0 f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
⊢ C a ≠ 0

Tactic:
by

Goal state after: