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

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k.succ + 1) * (n - k.succ)! = (n - k.succ).succ * (n - k.succ)!

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)

Tactic:
]

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α × α), List.count a l.offDiag ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α × α), List.count a l.offDiag ≤ 1
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
x y : α
⊢ (List.count x l * List.count y l - if x = y then List.count x l else 0) ≤ 1
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 2 * List.count a l ≤ List.count a l * List.count a l

Tactic:
]

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 2 * List.count a l ≤ List.count a l * List.count a l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ (n + 1) * n ! = (n + 1) * n !

Tactic:
]

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ (a'' ∈ a' ::ₘ a ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a' : α
f : (a'_1 : α) → a'_1 ∈ a' ::ₘ m → δ a'_1
h' : a' ∈ a' ::ₘ m
⊢ f a' ⋯ = f a' h'

Tactic:
]

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

Goal state before:
pp: case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!

Tactic:
]

Goal state after:
case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f a' ⋯ = f a' h'

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.domRestrict a = s.domRestrict b → f a = f b

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.domRestrict a = s.domRestrict b → f a = f b
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∃ e, f = e ∘ s.domRestrict) ↔ ∃ g, f = g ∘ s.domRestrict

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)

Tactic:
]

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ (i + j)! / (i ! * j !) = (i + j)! / (i ! * j !)

Tactic:
]

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

Goal state before:
pp: i j : ℕ
⊢ (i + j).choose j * j ! * i ! = (i + j).choose j * j ! * i !

Tactic:
]

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₁ a' h' = f₁ a' ⋯

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Tactic:
]

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₂ a' this = cons s a b f₂ a' this

Tactic:
]

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

Goal state before:
pp: i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
]

Goal state after:
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ #({x ∈ s ×ˢ t | p x.1 = q x.2}) = #({x ∈ s ×ˢ t | p x.1 ∧ q x.2} ∪ {x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})

α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
p : α → Prop
q : β → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint ({x ∈ s ×ˢ t | p x.1 ∧ q x.2}) ({x ∈ s ×ˢ t | ¬p x.1 ∧ ¬q x.2})
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₂ a' ⋯ = f₂ a' h'

Tactic:
]

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n ! / (k ! * (n - k)!) = n ! / (k ! * (n - k)!)

Tactic:
]

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

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
]

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ (a + b).choose a = (a + b).choose b

Tactic:
]

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ (a + b).choose a = (a + b).choose b
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m : ℕ
⊢ 1 + (m + m) = 1 + (m + m)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ cons s a b e₂ e ⋯ = cons s a b e₂ e ⋯

Tactic:
]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).choose (k + 1) * (k + 1) = n.succ.choose k.succ * (k + 1)

Tactic:
]

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

Goal state before:
pp: n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose k * (n - k) = n.choose k * (n - k)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val.dedup = ((t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)).val

Tactic:
]

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((insert a s).pi t).val.dedup = ((t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)).val
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((t a).val.bind fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup

Tactic:
]

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((t a).val.bind fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n + 1 + 1 = n + 1 + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s ^ 2 - #s

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
⊢ #s.offDiag = #s ^ 2 - #s
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #s = #s

Tactic:
]

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

Goal state before:
pp: case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (n + 1)

Tactic:
]

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

Goal state before:
pp: case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)

Tactic:
]

Goal state after:
m n : ℕ
hn : n ≠ 0
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose (n - 1) * ((m * n)! * n !)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g a ∈ t a

Tactic:
]

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
g : (a : α) → a ∈ univ → δ a
hg : ∀ (a : α), g a ⋯ ∈ t a
hgf : { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g = f
a : α
⊢ { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } g a ∈ t a
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1))! = (m * (p + 1) + (p + 1))!

Tactic:
]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p + 1) * (m * (p + 1) + p)!

Tactic:
]

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p)! * ((p + 1) * (m + 1))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

Tactic:
]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))

Tactic:
]

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

Goal state before:
pp: case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
simp only [hm, Nat.zero_mul, Nat.choose_eq_zero_iff]

Goal state after:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ 0 < n
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (p + 1) * (p * n + n - 1).choose (n - 1) = (p + 1) * (p * n + n - 1).choose (n - 1)

Tactic:
]

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

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
set p := m - 1; have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm
    simp only [hp]
    rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !

Tactic:
]

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

Tactic:
]

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

Goal state before:
pp: n k : ℕ
⊢ n ! * (n + 1).ascFactorial k = n ! * (n + 1).ascFactorial k

Tactic:
]

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

Goal state before:
pp: case zero.zero
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case zero
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k

Tactic:
cases k
    · rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
    · simp only [zero_ascFactorial, Nat.zero_add, succ_sub_succ_eq_sub,
        Nat.sub_zero, choose_succ_self, Nat.mul_zero]

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

Goal state before:
pp: case succ
k n✝ : ℕ
⊢ k ! * (n✝ + k).choose k = k ! * (n✝ + 1 + k - 1).choose k

Tactic:
]

Goal state after:
case succ
k n✝ : ℕ
⊢ k ! * (n✝ + k).choose k = k ! * (n✝ + 1 + k - 1).choose k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)

Tactic:
]

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
h : n < k
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !

Tactic:
]

Goal state after:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ (n - k)! * n.descFactorial k = (n - k)! * n.descFactorial k

Tactic:
]

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

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)

Tactic:
]

Goal state after:
r n : ℕ
h : r < n / 2
⊢ n.choose (r + 1) * (r + 1) ≤ n.choose (r + 1) * (n - r)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ r * 2 < n

Tactic:
]

Goal state after:
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose (n - r) ≤ n.choose (n / 2)

Tactic:
]

Goal state after:
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose (n - r) ≤ n.choose (n / 2)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
r n : ℕ
b : n < r
⊢ 0 ≤ n.choose (n / 2)

Tactic:
]

Goal state after:
case inr
r n : ℕ
b : n < r
⊢ 0 ≤ n.choose (n / 2)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (↑(Fintype.piFinset t)).Finite

Tactic:
]

Goal state after:
case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (↑(Fintype.piFinset t)).Finite
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
⊢ Pi.cons s a b₂ g a ⋯ = Pi.cons s a b₂ g a ⋯

Tactic:
]

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

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1

Tactic:
]

Goal state after:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
this : b₁ = b₂
⊢ b₁ = b₂

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
this : b₁ = b₂
⊢ b₁ = b₂
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ

Tactic:
]

Goal state after:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + k).choose k + (n + k).choose k.succ
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
b : β a'
hb : b ∈ t a'
ha' : a' ∈ a' ::ₘ m
⊢ b ∈ t a'

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
b : β a'
hb : b ∈ t a'
ha' : a' ∈ a' ::ₘ m
⊢ b ∈ t a'
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' ⋯ ∈ t a'

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' ⋯ ∈ t a'
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)