mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = count x l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = count x l
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = count x l

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0

Tactic:
· rw [h, count_map_of_injective l (·, y) (by simp [Function.Injective])]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0
Module: Mathlib.Data.Nat.Choose.Basic

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

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

Tactic:
·

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) → (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y

pp: case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y

Tactic:
·

Goal state after:
case mp
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) → (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y

Tactic:
·

Goal state after:
case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : 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
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

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
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
·

Goal state after:
case pos
α : 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
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'
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 k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
·

Goal state after:
case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (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
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
·

Goal state after:
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
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k s : ℕ
hsk : s ≤ k
hnk : n < k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

pp: case inr
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
·

Goal state after:
case inl
n k s : ℕ
hsk : s ≤ k
hnk : n < k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : a = a✝
⊢ r (⋯ ▸ b₁) (⋯ ▸ b₂)

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : a = a✝
⊢ r (⋯ ▸ b₁) (⋯ ▸ b₂)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)
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})
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
⊢ 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
⊢ 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: case pos
α : 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'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

pp: case neg
α : 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'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
·

Goal state after:
case pos
α : 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'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
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 + 1).choose (k + 1) * (n + 1 - (k + 1))

pp: case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
·

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

Goal state before:
pp: case neg
α : 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'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
·

Goal state after:
case neg
α : 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'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
·

Goal state after:
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
⊢ #({x ∈ s ×ˢ s | x.1 < x.2}) = (#s).choose 2

Tactic:
by
  set u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
  set v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
  have disj : Disjoint u v := by grind [disjoint_left]
  have union : u.disjUnion v disj = s.offDiag := by grind
  have swap : #u = #v := Finset.card_equiv (Equiv.prodComm α α) (by grind)
  grind [Nat.mul_sub_one, offDiag_card, Nat.choose_two_right]

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
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a

pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a
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)

pp: case neg.hf
α : 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),
    a_1 ∈ t a →
      ((t a').bind fun a_3 ↦ map (fun x ↦ Pi.cons (a' ::ₘ m) a a_1 (Pi.cons m a' a_3 x)) n) ≍
        (t a').bind fun a_3 ↦ map (fun x ↦ Pi.cons (a ::ₘ m) a' a_3 (Pi.cons m a a_1 x)) n

Tactic:
·

Goal state after:
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)
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)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!

Tactic:
by lia

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
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:
by lia

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)! * ((p + 1) * (m + 1))

Tactic:
by lia

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)

pp: case neg.hf.hf
α : 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'),
    a_1 ∈ t a' →
      map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n ≍
        map (fun x ↦ Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n

Tactic:
·

Goal state after:
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)
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 ! * ((p + 1) * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))

Tactic:
by lia

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)! * (m + 1)) =
    (m + 1) * (m * (p + 1) + p).choose p * ((m * (p + 1))! * (p + 1)!)

Tactic:
by lia

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)

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

Tactic:
·

Goal state after:
case pos
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
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:
·

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
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)

pp: case neg.hf.hf.hf
α : 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 : α) → a ∈ m → β a),
    a_1 ∈ n → Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' a_1) ≍ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b a_1)

Tactic:
·

Goal state after:
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)
Module: Mathlib.Data.Nat.Choose.Basic

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

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

Tactic:
·

Goal state after:
case zero
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅

pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅
Module: Mathlib.Data.Nat.Choose.Basic

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

pp: case zero.succ
n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) = (n✝ + 1)! * (0 + (n✝ + 1) - 1).choose (n✝ + 1)

Tactic:
·

Goal state after:
case zero.zero
⊢ ascFactorial 0 0 = 0! * (0 + 0 - 1).choose 0
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
·

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

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

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

Tactic:
·

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

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

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

Tactic:
·

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

Goal state before:
pp: case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

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

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case inl
n k : ℕ
hk : k < n
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

pp: case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

pp: case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
·

Goal state after:
case inl
n k : ℕ
hk : k < n
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k

pp: case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
·

Goal state after:
case inr.inl
k : ℕ
⊢ k.choose k = 1 ↔ k = 0 ∨ k = k
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
·

Goal state after:
case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k
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 α),
    (s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup) →
      (a ::ₘ s).Nodup → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup

Tactic:
by
      intro a s ih hs ht
      have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
      have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
      simp only [pi_cons, nodup_bind]
      refine
        ⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
          ?_⟩
      refine (ht a <| mem_cons_self _ _).pairwise ?_
      exact fun b₁ _ b₂ _ neb =>
        disjoint_map_map.2 fun f _ g _ eq =>
          have : Pi.cons s a b₁ f a (mem_cons_self _ _) =
            Pi.cons s a b₂ g a (mem_cons_self _ _) := by rw [eq]
          neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this

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

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
⊢ f ∈ pi 0 t ↔ ∀ (a : α) (h : a ∈ 0), f a h ∈ t a

Tactic:
have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
⊢ f ∈ pi 0 t ↔ ∀ (a : α) (h : a ∈ 0), f a h ∈ t a