mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Tactic:
have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
        lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1

Tactic:
]

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ f p * f 1 = f p * f 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Even n → 0 < x + 1 ∨ 0 = x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1

Tactic:
]

Goal state after:
n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}

Tactic:
]

Goal state after:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ {1} = (n✝ + 1 + 1).properDivisors

Tactic:
]

Goal state after:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ {1} = (n✝ + 1 + 1).properDivisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
]

Goal state after:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k ↔ ∃ j, ∃ (_ : j < k), x = p ^ j
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: a b n : ℕ
⊢ ∑ k ∈ range n, a / b ^ (k + 1) * b + a * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i

Tactic:
]

Goal state after:
case h
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisors,
      f ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).2 =
    ∏ i ∈ n.divisors, f i (n / i)

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisors,
      f ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).1 ({ toFun := fun d ↦ (d, n / d), inj' := ⋯ } x).2 =
    ∏ i ∈ n.divisors, f i (n / i)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b

Tactic:
]

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    ∏ i ∈ n.divisors, f (n / i) i

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    ∏ i ∈ n.divisors, f (n / i) i
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b

Tactic:
]

Goal state after:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
| n.divisors

Tactic:
← image_fst_divisorsAntidiagonal,

Goal state after:
n : ℕ
| image Prod.fst n.divisorsAntidiagonal
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)

Tactic:
]

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)

Tactic:
]

Goal state after:
case succ
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a + ∑ i ∈ Ico 1 n.succ, a / b ^ i

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ x ∈ Ico (0 + 1) n.succ, a / b ^ x

pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (0 + 1) n.succ

Tactic:
]

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ x ∈ Ico (0 + 1) n.succ, a / b ^ x

b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (0 + 1) n.succ
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a * b / (b - 1) = a * b / (b - 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.val x.cast.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.val x.cast.val) ≡ x.val [MOD n]

Tactic:
]

Goal state after:
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ ↑(Nat.chineseRemainder h x.cast.val x.cast.val) ≡ x.val [MOD m] ∧
    ↑(Nat.chineseRemainder h x.cast.val x.cast.val) ≡ x.val [MOD n]
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a + a / (b - 1) = a + a / (b - 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
]

Goal state after:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_1
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = x.cast

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2

Tactic:
]

Goal state after:
case mp
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
x : ZMod (m * n)
⊢ x.cast = x.cast

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ¬n = 1 ↔ n ≠ 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
]

Goal state after:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a + a = 0 ↔ a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a = 0 ↔ a = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ ¬a = 0

Tactic:
]

Goal state after:
n : ℕ
hn : Odd n
a : ZMod n
ha : a ≠ 0
⊢ ¬a = 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n

Tactic:
]

Goal state after:
n : ℕ
a : ZMod n
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ ↑k ! * ↑(n.choose k) < ↑n ^ k

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ ↑k ! * ↑(n.choose k) < ↑n ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.descFactorial k < n ^ k

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n k : ℕ
hn : n ≠ 0
hk : 2 ≤ k
⊢ n.descFactorial k < n ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k / k ! ≤ n.descFactorial k

Tactic:
]

Goal state after:
n k : ℕ
⊢ n.descFactorial k / k ! ≤ n.descFactorial k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ n.descFactorial k

Tactic:
by
  rw [choose_eq_descFactorial_div_factorial]
  exact Nat.div_le_self _ _

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

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.descFactorial k / k ! < n.descFactorial k

Tactic:
]

Goal state after:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.descFactorial k / k ! < n.descFactorial k
Module: Mathlib.Data.Nat.Choose.Bounds

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

Tactic:
]

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k / k ! ≤ (n + 1) ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1) ^ k

Tactic:
]

Goal state after:
case inl
k m : ℕ
h : k ≤ k + m
⊢ (m + k).choose k ≤ (m + 1) ^ k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
]

Goal state after:
case succ.mp.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 = 0 ∨ a.val = 0
⊢ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ 0 < ↑r !
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = n✝ + 1
⊢ 2 * a.val = n✝ + 1

Tactic:
]

Goal state after:
case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = n✝ + 1
⊢ 2 * a.val = n✝ + 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ (n✝¹ + 1) * 2 ≤ (n✝¹ + 1) * (n✝ + 1 + 1)

Tactic:
]

Goal state after:
case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ (n✝¹ + 1) * 2 ≤ (n✝¹ + 1) * (n✝ + 1 + 1)
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ 2 ^ (n + 1)

Tactic:
]

Goal state after:
case neg.succ.zero
n : ℕ
lt : ¬n + 1 + 1 < 0
⊢ 1 ≤ 2 ^ (n + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 0

Tactic:
]

Goal state after:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ 2 ^ n + 2 ^ n

Tactic:
]

Goal state after:
case neg.succ.succ
n k : ℕ
lt : ¬n + 1 + 1 < k + 1
⊢ (n + 1).choose k + (n + 1).choose (k + 1) ≤ 2 ^ n + 2 ^ n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ n✝ + 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n a : ℕ
h : a < n
⊢ a = a

Tactic:
]

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

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ 2 ^ (n - succ 0 + succ 0 - 1)

Tactic:
]

Goal state after:
n k : ℕ
p : 0 < n
⊢ (n - succ 0 + succ 0).choose k ≤ 2 ^ (n - succ 0 + succ 0 - 1)
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ 2 ^ n

Tactic:
obtain (rfl | hn) := eq_zero_or_pos n
  · cases k <;> simp
  · exact (Nat.choose_lt_two_pow _ _ hn).le

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < m + 1

pp: case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1

Tactic:
]

Goal state after:
case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < m + 1

case pos
m : ℕ
inst✝¹ : NeZero (m + 1)
a : ZMod (m + 1)
n : ℕ
inst✝ : NeZero (n + 1)
h : m < n + 1
⊢ a.val < n + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: r n : ℕ
⊢ (2 * n).choose n = (2 * n).choose n

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ 2 ^ (2 * n) ≤ 2 ^ (2 * n)

Tactic:
]

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.centralBinom < 2 ^ (2 * n)

Tactic:
]

Goal state after:
n : ℕ
h : n ≠ 0
⊢ n.centralBinom < 2 ^ (2 * n)
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
]

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

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

Tactic:
by ring

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = (-a).val

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * 4 ^ n = 4 * 4 ^ n

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val

Tactic:
]

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
]

Goal state after:
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * n.centralBinom ≤ 2 * (2 * n + 1) * n.centralBinom
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)

Tactic:
]

Goal state after:
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val

Tactic:
]

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h
n : ℕ
⊢ 2 * (n + 1 + n).choose n = 2 * (n + 1 + n).choose n

Tactic:
]

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

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom

Tactic:
]

Goal state after:
n : ℕ
h : 0 < n
⊢ 2 ∣ n.pred.succ.centralBinom
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ Coprime 1 n

Tactic:
]

Goal state after:
n : ℕ
⊢ Coprime 1 n
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom

Tactic:
]

Goal state after:
n : ℕ
h_s : (n + 1).Coprime (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * (n + 1).centralBinom
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ (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))

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ [x.succ] = [x.succ]

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)

pp: case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)

Tactic:
]

Goal state after:
case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)

case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a ≠ 0

Tactic:
]

Goal state after:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ a.val ^ (m + 1) = a.val ^ (m + 1)

Tactic:
]

Goal state after: