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

Goal state before:
pp: case a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
x : α → R
n : ℕ
x✝ : ↥(s.sym n)
a✝ : x✝ ∈ univ
⊢ (Multiset.map x ↑↑x✝).prod = (Multiset.map x ↑↑x✝).prod

Tactic:
]

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

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

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!
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
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
this : p = 0
⊢ 0 = 0

Tactic:
]

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 ∈ π.boxes ∧ π.tag J ∈ s
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ εs (π.tag J)

Tactic:
]

Goal state after:
ι : 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 ∈ π.boxes ∧ π.tag J ∈ s
⊢ dist ((vol J) (f (π.tag J))) (g J) ≤ εs (π.tag J)
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∏ i ∈ s, 2 ^ f i) * (∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! =
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ((∏ x ∈ s, 2 ^ f x) * ∏ x ∈ s, (f x)!)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case h1
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
a✝ : i ∈ s
⊢ (2 * f i)‼ ≤ (2 * f i)!

Tactic:
]

Goal state after:
case h1
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
a✝ : i ∈ s
⊢ (2 * f i)‼ ≤ (2 * f i)!
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case inl
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
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
x✝ : f i ∈ Set.univ
⊢ x i ∈ s (f i)

Tactic:
]

Goal state after:
case inl
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
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
x✝ : f i ∈ Set.univ
⊢ x i ∈ s (f i)
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)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s)).countPerms =
    n.choose ↑m * (↑s).countPerms

Tactic:
]

Goal state after:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s)).countPerms =
    n.choose ↑m * (↑s).countPerms
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)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s)).countPerms =
    n.choose ↑m * (↑s).countPerms

Tactic:
]

Goal state after:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑(fill x m s)).countPerms =
    n.choose ↑m * (↑s).countPerms
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
]

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

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

Tactic:
]

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a

Tactic:
]

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = 0

Tactic:
]

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 ↦ x ≠ x_1) (Multiset.replicate (↑m) x) = 0
Module: Mathlib.Data.Nat.Choose.Multinomial

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

Tactic:
]

Goal state after:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ Multiset.replicate (↑m) x, ¬x ≠ a
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ (∑ i ∈ s, d i)! / ∏ i ∈ s, (d i)! = (∑ x ∈ s, id (d x))! / ∏ x ∈ s, (d x)!

Tactic:
]

Goal state after:
σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ (∑ i ∈ s, d i)! / ∏ i ∈ s, (d i)! = (∑ x ∈ s, id (d x))! / ∏ x ∈ s, (d x)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ (((Finsupp.single 0 x).sum fun x a ↦ a) + (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).sum fun x a ↦ a) =
    x + l.sum

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ (((Finsupp.single 0 x).sum fun x a ↦ a) + (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).sum fun x a ↦ a) =
    x + l.sum
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
  match l with
  | nil => simp
  | x :: l =>
    simp only [toFinsupp_cons_eq_single_add_embDomain, sum_cons]
    rw [Finsupp.sum_add_index (by simp) (by simp)]
    simp [Finsupp.sum_embDomain, l.toFinsupp_sum]

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

Goal state before:
pp: x : ℕ
l : List ℕ
⊢ ((x :: l).toFinsupp.sum fun x ↦ id).choose ((x :: l).toFinsupp 0) * ((x :: l).toFinsupp.update 0 0).multinomial =
    (x + l.sum).choose x * l.toFinsupp.multinomial

Tactic:
]

Goal state after:
x : ℕ
l : List ℕ
⊢ ((x :: l).toFinsupp.sum fun x ↦ id).choose ((x :: l).toFinsupp 0) * ((x :: l).toFinsupp.update 0 0).multinomial =
    (x + l.sum).choose x * l.toFinsupp.multinomial
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 : ℕ
⊢ l.toFinsupp ⋯.choose = l[x]?.getD 0

Tactic:
]

Goal state after:
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 : ℕ
⊢ l.toFinsupp ⋯.choose = l[x]?.getD 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case swap
m : Multiset ℕ
l✝ l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (y + (x + l.sum)).choose (x + l.sum) * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial

Tactic:
]

Goal state after:
case swap
m : Multiset ℕ
l✝ l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (y + (x + l.sum)).choose (x + l.sum) * (x + l.sum).choose x * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ rα (a₁, b₁).1 (a₂, b₂).1 ∧ (a₁, b₁).2 = (a₂, b₂).2 ∨ rβ (a₁, b₁).2 (a₂, b₂).2 ∧ (a₁, b₁).1 = (a₂, b₂).1 ↔
    rα a₁ a₂ ∧ b₁ = b₂ ∨ rβ b₁ b₂ ∧ a₁ = a₂

Tactic:
]

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

Goal state before:
pp: case swap
m : Multiset ℕ
l✝ l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (x + (y + l.sum)).choose x * (y + l.sum).choose (x + l.sum - x) * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial

Tactic:
]

Goal state after:
case swap
m : Multiset ℕ
l✝ l' : List ℕ
x y : ℕ
l : List ℕ
⊢ (x + (y + l.sum)).choose x * (y + l.sum).choose (x + l.sum - x) * l.multinomial =
    (x + (y + l.sum)).choose x * (y + l.sum).choose y * l.multinomial
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case trans
m : Multiset ℕ
l✝ l'✝ l l' l'' : List ℕ
h : l.Perm l'
h' : l'.Perm l''
ih : l.multinomial = l'.multinomial
ih' : l'.multinomial = l''.multinomial
⊢ l''.multinomial = l''.multinomial

Tactic:
]

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₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
rα✝ : α → α → Prop
rβ : β → β → Prop
a : α
b : β
rα : α → α → Prop
a₁ b₁ a₂ b₂ : α
⊢ (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂)) ∧
    (Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) =
      (Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂))
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(b, a₂)

Tactic:
]

Goal state after:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(b, a₂)
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(a₂, b)

Tactic:
]

Goal state after:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(a₂, b)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
⊢ Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩ s(c, d)
      s(a, b) →
    Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
      s(c, d)

Tactic:
]

Goal state after:
case intro.intro.h
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c d : α
⊢ Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩ s(c, d)
      s(a, b) →
    Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
      s(c, d)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum

Tactic:
]

Goal state after:
case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(d, b)

Tactic:
]

Goal state after:
case intro.intro.h.inr.fst
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(d, b)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case intro.intro.h.inr.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(a, c)

Tactic:
]

Goal state after:
case intro.intro.h.inr.snd
α : Type u_1
rα : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α}, Acc rα b → Acc (Sym2.GameAdd rα) s(y, b)
b✝ b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc (Sym2.lift₂ ⟨fun a₁ b₁ a₂ b₂ ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂), ⋯⟩)
    s(a, c)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)

Tactic:
]

Goal state after:
case succ
m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ (m.sum + k • m.sum).choose m.sum * m.multinomial *
      ((Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k) =
    ((m.sum + ∑ i ∈ Finset.range k, m.sum).choose m.sum * Nat.multinomial (Finset.range k) fun x ↦ m.sum) *
      (m.multinomial * m.multinomial ^ k)
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 (InvImage (DFinsupp.Lex r fun x ↦ s) toDFinsupp) x

Tactic:
]

Goal state after:
α : 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 (InvImage (DFinsupp.Lex r fun x ↦ s) toDFinsupp) x
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x₁ i) (x₁ i)
hi : r i i
⊢ s i (x₁ i) (x₁ i)

Tactic:
]

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x₁ i) (x₁ i)
hi : r i i
⊢ s i (x₁ i) (x₁ i)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ x₁ j = x₁ j

Tactic:
]

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

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = x j

Tactic:
]

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = x j
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
j : ι
h₁ : r j i ∧ j ∉ p
⊢ x₂ j = x₂ j

Tactic:
]

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x₂ i) (x₂ i)
hi : r i i
⊢ s i (x₂ i) (x₂ i)

Tactic:
]

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x₂ i) (x₂ i)
hi : r i i
⊢ s i (x₂ i) (x₂ i)
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ x₁ j = x₁ j

Tactic:
]

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 + b)

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn (a + b)