awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
e_a : ∀ (i : ℕ) (hi : i ∈ range n.succ), f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i)
    (∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x))

Tactic:
refine prod_congr rfl fun i hi ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
e_a e_a₁ : f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose i
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)

Tactic:
rw [choose_symm (this _ hi)]

Premises used: Nat.choose_symm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i ∈ range (n + 2), (↑((n + 1).choose i) : R) * f i (n + 1 - i) =
    HAdd.hAdd (α := R) (∑ i ∈ range (n + 1), (↑(n.choose i) : R) * f i (n + 1 - i))
      (∑ i ∈ range (n + 1), (↑(n.choose i) : R) * f (i + 1) (n - i))

Tactic:
simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n

Premises used: Finset.sum_choose_succ_nsmul, nsmul_eq_mul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (↑((n + 1).choose ij.1) : R) * f ij.1 ij.2 =
    HAdd.hAdd (α := R) (∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (↑(n.choose ij.1) : R) * f ij.1 (ij.2 + 1))
      (∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (↑(n.choose ij.2) : R) * f (ij.1 + 1) ij.2)

Tactic:
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n

Premises used: Finset.sum_antidiagonal_choose_succ_nsmul, nsmul_eq_mul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
d : ℕ
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
d n : ℕ
hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
succ :
  (d + (0, n + 1).2).choose d + ∑ p ∈ @antidiagonal _ instAddMonoid _ n, (d + (p.1 + 1, p.2).2).choose d =
    (d + (n + 1) + 1).choose (d + 1)
succ₁ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1) + 1).choose (d + 1)
succ₂ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1)).choose d + (d + (n + 1)).choose d.succ
succ₃ succ₄ : (d + n + 1).choose d + (d + n + 1).choose (d + 1) = (d + n + 1).choose d + (d + n + 1).choose d.succ
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)

Tactic:
rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

Premises used: add_assoc, Nat.choose_succ_succ, HAdd.hAdd, OfNat.ofNat, Finset.Nat.sum_antidiagonal_succ
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
d n : ℕ
zero : ∑ ij ∈ @antidiagonal _ instAddMonoid _ 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)
succ :
  ∀ (n : ℕ) (hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)),
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)

Tactic:
induction n with
  | zero => simp
  | succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

Premises used: add_assoc, Nat.choose_succ_succ, HAdd.hAdd, Nat.zero, OfNat.ofNat, Nat.succ, Finset.Nat.sum_antidiagonal_succ
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
m n k : ℕ
rw : (m + n).choose k = (↑((m + n).choose k) : ℕ)
rw₁ rw₂ : (m + n).choose k = (m + n).choose k
⊢ (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k

Tactic:
rw [coeff_X_add_one_pow, cast_id]

Premises used: Nat.cast_id, Polynomial.coeff_X_add_one_pow
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
m n k : ℕ
rw rw₁ :
  (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k =
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k
⊢ (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k =
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k

Tactic:
rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
m n k : ℕ
rw :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m).coeff x.1 * (HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff x.2 = m.choose x.1 * n.choose x.2
⊢ (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2

Tactic:
rw [coeff_mul, Finset.sum_congr rfl]

Premises used: Polynomial.coeff_mul, Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
m n k : ℕ
⊢ ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m).coeff x.1 * (HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff x.2 = m.choose x.1 * n.choose x.2

Tactic:
simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

Premises used: Nat.cast_id, imp_true_iff, Polynomial.coeff_X_add_one_pow
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
m n k : ℕ
k₁ : (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k
k₂ :
  (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k =
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k
k₃ :
  (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2
⊢ (m + n).choose k = ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2

Tactic:
calc
    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]

Premises used: Nat.choose, Polynomial.coeff, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Polynomial.X, Finset.HasAntidiagonal.antidiagonal
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
n : ℕ
rw :
  Eq (α := ℕ) (∑ i ∈ range (n + 1), HPow.hPow (β := ℕ) (n.choose i) 2)
    (∑ k ∈ range n.succ, n.choose (k, n - k).1 * n.choose (k, n - k).2)
⊢ ∑ i ∈ range (n + 1), HPow.hPow (β := ℕ) (n.choose i) 2 = (2 * n).choose n

Tactic:
rw [two_mul, add_choose_eq, sum_antidiagonal_eq_sum_range_succ_mk]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, two_mul, Nat.add_choose_eq
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
n : ℕ
a : ∀ (x : ℕ) (h : x ∈ range n.succ), HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose (x, n - x).2
⊢ Eq (α := ℕ) (∑ i ∈ range (n + 1), HPow.hPow (β := ℕ) (n.choose i) 2)
    (∑ k ∈ range n.succ, n.choose (k, n - k).1 * n.choose (k, n - k).2)

Tactic:
congr! 1 with _ h
-- Module: Mathlib.Data.Nat.Choose.Vandermonde
Goal:
n x : ℕ
h : x ∈ range n.succ
a : HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose x
a₁ a₂ : n.choose x * n.choose x = n.choose (x, n - x).1 * n.choose x
⊢ HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose (x, n - x).2

Tactic:
rw [choose_symm (Finset.mem_range_succ_iff.mp h), sq]

Premises used: Finset.mem_range_succ_iff, sq, Nat.choose_symm, Iff.mp
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
⊢ count p 0 = 0

Tactic:
simp [count]

Premises used: Nat.count
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x

Tactic:
simp
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
rw : (List.filter (fun (b : ℕ) ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})
⊢ count p n = #({x ∈ range n | p x})

Tactic:
rw [count, List.countP_eq_length_filter]

Premises used: List.countP_eq_length_filter, Nat.count
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ (List.filter (fun (b : ℕ) ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
H : ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x
⊢ count p n = Fintype.card { k : ℕ // k < n ∧ p k }

Tactic:
rw [count_eq_card_filter_range, Fintype.card_of_subtype]

Premises used: Nat.count_eq_card_filter_range, Fintype.card_of_subtype
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
rw : #({x ∈ range n | p x}) ≤ n
⊢ count p n ≤ n

Tactic:
rw [count_eq_card_filter_range]

Premises used: Nat.count_eq_card_filter_range
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ n

Tactic:
(card_filter_le _ _).trans_eq (card_range _)

Premises used: LE.le.trans_eq, Finset.card_range, Finset.card_filter_le
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ n

Tactic:
exact (card_filter_le _ _).trans_eq (card_range _)

Premises used: LE.le.trans_eq, Finset.card_range, Finset.card_filter_le
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + if p n then 1 else 0

Tactic:
grind [count, List.range_succ]

Premises used: Nat.count, List.range_succ
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
⊢ ∀ (n : ℕ), count p n ≤ count p (n + 1)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count p a + count (fun (k : ℕ) ↦ p (a + k)) b

Tactic:
simp [count, List.range_add, Function.comp_def]

Premises used: List.range_add, Function.comp_def, Nat.count
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
rw : count (fun (k : ℕ) ↦ p (b + k)) a + count p b = count (fun (k : ℕ) ↦ p (k + b)) a + count p b
⊢ count p (a + b) = count (fun (k : ℕ) ↦ p (k + b)) a + count p b

Tactic:
rw [add_comm, count_add, add_comm]

Premises used: add_comm, Nat.count_add
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
⊢ count (fun (k : ℕ) ↦ p (b + k)) a + count p b = count (fun (k : ℕ) ↦ p (k + b)) a + count p b

Tactic:
simp_rw [add_comm b]

Premises used: add_comm
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
⊢ count p 1 = if p 0 then 1 else 0

Tactic:
simp [count_succ]

Premises used: Nat.count_succ
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
rw : count (fun (k : ℕ) ↦ p (k + 1)) n + count p 1 = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
rw₁ rw₂ :
  (count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0) = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
⊢ count p (n + 1) = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0

Tactic:
rw [count_add', count_one]

Premises used: Nat.count_add', Nat.count_one
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n < count p (n + 1) ↔ p n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + 1 ↔ p n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n ↔ ¬p n

Tactic:
grind
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
h : count p a < count p b
⊢ a < b

Tactic:
(count_monotone p).reflect_lt h

Premises used: Monotone.reflect_lt, Nat.count_monotone
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hmn : m < n
⊢ count p m < count p n

Tactic:
(count_lt_count_succ_iff.2 hm).trans_le <| count_monotone _ (Nat.succ_le_iff.2 hmn)

Premises used: Iff.mpr, Nat.count_monotone, LT.lt.trans_le, Nat.count_lt_count_succ_iff, Nat.succ_le_iff
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
by_contra : ∀ (h : m ≠ n), False
⊢ m = n

Tactic:
by_contra h : m ≠ n
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
inr :
  ∀
    (this :
      ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n)
        (h : m ≠ n) (hmn : m < n), False)
    (hmn : ¬m < n), False
wlog :
  ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) (h : m ≠ n)
    (hmn : m < n), False
⊢ False

Tactic:
wlog hmn : m < n
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this :
  ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) (h : m ≠ n)
    (hmn : m < n), False
hmn : ¬m < n
⊢ n < m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this :
  ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) (h : m ≠ n)
    (hmn : m < n), False
hmn : ¬m < n
⊢ False

Tactic:
exact this hn hm heq.symm h.symm (by grind)

Premises used: Ne.symm, Eq.symm
-- Module: Mathlib.Data.Nat.Count
Goal:
p_1 : ℕ → Prop
inst : DecidablePred p_1
p : ℕ → Prop
inst_1 : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False

Tactic:
simpa [heq] using count_strict_mono hm hmn

Premises used: Nat.count_strict_mono
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Finite
n : ℕ
rw : #({x ∈ range n | p x}) ≤ #(hp.toFinset (s := setOf p))
⊢ count p n ≤ #(hp.toFinset (s := setOf p))

Tactic:
rw [count_eq_card_filter_range]

Premises used: Nat.count_eq_card_filter_range
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Finite
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ #(hp.toFinset (s := setOf p))

Tactic:
Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2

Premises used: Iff.mpr, Set.Finite.mem_toFinset, And.right, Iff.mp, Finset.mem_filter, Finset.card_mono
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Finite
n : ℕ
⊢ #({x ∈ range n | p x}) ≤ #(hp.toFinset (s := setOf p))

Tactic:
exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2

Premises used: Iff.mpr, Set.Finite.mem_toFinset, And.right, Iff.mp, Finset.mem_filter, Finset.card_mono
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hp : (setOf p).Finite
hpn : p n
⊢ count p n < #(hp.toFinset (s := setOf p))

Tactic:
(count_lt_count_succ_iff.2 hpn).trans_le (count_le_card hp _)

Premises used: Iff.mpr, Nat.count_le_card, LT.lt.trans_le, Nat.count_lt_count_succ_iff
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n = n ↔ ∀ n' < n, p n'

Tactic:
simpa [count_eq_card_filter_range, card_range, mem_range] using
    card_filter_eq_iff (p := p) (s := range n)

Premises used: Nat.count_eq_card_filter_range, Finset.card_filter_eq_iff, Finset.card_range, Finset.mem_range
-- Module: Mathlib.Data.Nat.Count
Goal:
n : ℕ
⊢ count (fun (x : ℕ) ↦ True) n = n

Tactic:
count_of_forall fun _ _ ↦ trivial

Premises used: trivial, Nat.count_of_forall
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n = 0 ↔ ∀ m < n, ¬p m

Tactic:
simp [count_eq_card_filter_range]

Premises used: Nat.count_eq_card_filter_range
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n ≠ 0 ↔ ∃ m < n, p m

Tactic:
simp [Nat.count_iff_forall_not]

Premises used: Nat.count_iff_forall_not
-- Module: Mathlib.Data.Nat.Count
Goal:
n : ℕ
⊢ count (fun (x : ℕ) ↦ False) n = 0

Tactic:
count_of_forall_not fun _ _ ↦ id

Premises used: id, Nat.count_of_forall_not
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
h : count p a < count p b
obtain : ∀ (k : ℕ) (h : count p a < count p (a + k + 1)), ∃ x ∈ Set.Ico a (a + k + 1), p x
⊢ ∃ x ∈ Set.Ico a b, p x

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt (lt_of_count_lt_count h)

Premises used: Nat.lt_of_count_lt_count, Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a k : ℕ
h : count p a < count p (a + k + 1)
⊢ 0 < count (fun (k : ℕ) ↦ p (a + k)) (k + 1)

Tactic:
rw [add_assoc, count_add, Nat.lt_add_right_iff_pos] at h

Premises used: Nat.lt_add_right_iff_pos, add_assoc, Nat.count_add
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a k : ℕ
h : 0 < count (fun (k : ℕ) ↦ p (a + k)) (k + 1)
obtain : ∀ (t : ℕ) (ht : t < k + 1) (hp : p (a + t)), ∃ x ∈ Set.Ico a (a + k + 1), p x
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x

Tactic:
obtain ⟨t, ht, hp⟩ := count_ne_iff_exists.mp h.ne'

Premises used: Nat.count_ne_iff_exists, LT.lt.ne', Iff.mp
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a k : ℕ
h : 0 < count (fun (k : ℕ) ↦ p (a + k)) (k + 1)
t : ℕ
ht : t < k + 1
hp : p (a + t)
⊢ (a ≤ a + t ∧ a + t < a + k + 1) ∧ p (a + t)

Tactic:
grind
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
a k : ℕ
h : 0 < count (fun (k : ℕ) ↦ p (a + k)) (k + 1)
t : ℕ
ht : t < k + 1
hp : p (a + t)
⊢ ∃ (x : ℕ), (a ≤ x ∧ x < a + k + 1) ∧ p x

Tactic:
exact ⟨a + t, by grind⟩
-- Module: Mathlib.Data.Nat.Count
Goal:
p : ℕ → Prop
inst : DecidablePred p
q : ℕ → Prop
inst_1 : DecidablePred q
n : ℕ
hpq : ∀ k < n, p k → q k
⊢ ∀ x ∈ List.range n, decide (p x) = true → decide (q x) = true

Tactic:
simpa
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
⊢ (n + 1) / b < n.succ

Tactic:
Nat.div_lt_self (Nat.succ_pos _) h

Premises used: Nat.div_lt_self, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
⊢ (n + 1) / b < n.succ

Tactic:
exact Nat.div_lt_self (Nat.succ_pos _) h

Premises used: Nat.div_lt_self, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
⊢ (n + 1) / b < n.succ

Tactic:
decreasing_by exact Nat.div_lt_self (Nat.succ_pos _) h

Premises used: Nat.div_lt_self, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
⊢ b.digitsAux h 0 = []

Tactic:
rfl

Premises used: WellFounded.Nat.fix, Nat.digitsAux, WellFounded.Nat.fix.go, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
zero : ∀ (w : LT.lt (α := ℕ) 0 0), b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)
succ : ∀ (n : ℕ) (w : 0 < n + 1), b.digitsAux h (n + 1) = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
w : LT.lt (α := ℕ) 0 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

Tactic:
cases w
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n + 1
succ succ₁ : (n + 1) % b :: b.digitsAux h ((n + 1) / b) = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
⊢ b.digitsAux h (n + 1) = (n + 1) % b :: b.digitsAux h ((n + 1) / b)

Tactic:
rw [digitsAux]

Premises used: Nat.digitsAux
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
⊢ 2 ≤ b + 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
zero : digits 0 0 = []
succ : (HAdd.hAdd (α := ℕ) 0 1).digits 0 = []
succ₁ : ∀ (n : ℕ), (n + 1 + 1).digits 0 = []
⊢ b.digits 0 = []

Tactic:
rcases b with (_ | ⟨_ | ⟨_⟩⟩)
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
⊢ digits 0 0 = []

Tactic:
simp [digits, digitsAux0, digitsAux1]

Premises used: Nat.digitsAux1, Nat.digits, Nat.digitsAux0
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1).digits 0 = []

Tactic:
simp [digits, digitsAux0, digitsAux1]

Premises used: Nat.digitsAux1, Nat.digits, Nat.digitsAux0
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
⊢ (n + 1 + 1).digits 0 = []

Tactic:
simp [digits, digitsAux0, digitsAux1]

Premises used: Nat.digitsAux1, Nat.digits, Nat.digitsAux0
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
⊢ digits 0 0 = []

Tactic:
rfl

Premises used: Nat.digits, Nat.digitsAux0, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
⊢ digits 0 n.succ = [n + 1]

Tactic:
rfl

Premises used: Nat.digits, Nat.digitsAux0, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
⊢ digits 1 n = List.replicate n 1

Tactic:
rfl

Premises used: Nat.digitsAux1, Nat.digits, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
⊢ digits 1 (n + 1) = 1 :: digits 1 n

Tactic:
rfl

Premises used: List.replicate, Nat.digitsAux1, Nat.digits, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
⊢ (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))

Tactic:
simp [digits, digitsAux_def]

Premises used: Nat.digitsAux_def, Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
hb : 2 ≤ b
hn : 0 < n
rw : (b - 2 + 2).digits n = n % (b - 2 + 2) :: (b - 2 + 2).digits (n / (b - 2 + 2))
rw₁ :
  (b - 2 + 2).digits (n - succ 0 + succ 0) =
    (n - succ 0 + succ 0) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + succ 0) / (b - 2 + 2))
rw₂ rw₃ :
  (n - succ 0 + 1) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + 1) / (b - 2 + 2)) =
    (n - succ 0 + succ 0) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + succ 0) / (b - 2 + 2))
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]

Premises used: Nat.digits_add_two_add_one, Nat.eq_add_of_sub_eq, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
h : LT.lt (α := ℕ) 1 0
⊢ ¬LT.lt (α := ℕ) 1 0

Tactic:
decide
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
h : LT.lt (α := ℕ) 1 1
⊢ ¬LT.lt (α := ℕ) 1 1

Tactic:
decide
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
h : 1 < b + 2
⊢ 2 ≤ b + 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b x : ℕ
hx : x ≠ 0
hxb : x < b
rcases : ∀ (x : ℕ) (hx : x.succ ≠ 0) (hxb : x.succ < b), b.digits x.succ = [x.succ]
⊢ b.digits x = [x]

Tactic:
rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b x : ℕ
hx : x.succ ≠ 0
hxb : x.succ < b
rcases : ∀ (b : ℕ) (hxb : x.succ < b + succ 1), (b + succ 1).digits x.succ = [x.succ]
⊢ b.digits x.succ = [x.succ]

Tactic:
rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩

Premises used: Nat.le_add_left, Nat.exists_eq_add_of_le', OfNat.ofNat, LE.le.trans_lt, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
rw : (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]
rw₁ : (x + 1) % (b + 2) :: (b + 2).digits 0 = [x.succ]
rw₂ : [(x + 1) % (b + 2)] = [x.succ]
rw₃ rw₄ : [x.succ] = [x.succ]
⊢ (b + succ 1).digits x.succ = [x.succ]

Tactic:
rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]

Premises used: Nat.digits_add_two_add_one, Nat.mod_eq_of_lt, Nat.digits_zero, Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
x y : ℕ
hxb : x < b
hxy : x ≠ 0 ∨ y ≠ 0
rcases : ∀ (b : ℕ) (h : 1 < b + 2) (hxb : x < b + 2), (b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y
⊢ b.digits (x + b * y) = x :: b.digits y

Tactic:
rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x y : ℕ
hxy : x ≠ 0 ∨ y ≠ 0
b : ℕ
h : 1 < b + 2
hxb : x < b + 2
zero : ∀ (hxy : x ≠ 0 ∨ Ne (α := ℕ) 0 0), (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0
succ : ∀ (n : ℕ) (hxy : x ≠ 0 ∨ n + 1 ≠ 0), (b + 2).digits (x + (b + 2) * (n + 1)) = x :: (b + 2).digits (n + 1)
⊢ (b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y

Tactic:
cases y
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
hxy : x ≠ 0 ∨ Ne (α := ℕ) 0 0
⊢ (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0

Tactic:
simp [hxb, hxy.resolve_right (absurd rfl)]

Premises used: absurd, Or.resolve_right, rfl