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

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.2 ∈ n.divisors

Tactic:
by

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

Goal state before:
pp: n x : ℕ
h : x.Coprime n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.fst n.divisorsAntidiagonal = n.divisors

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ ↑(↑m)⁻¹.val * ↑m = 1

Tactic:
by

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

Goal state before:
pp: m n✝ n x : ℕ
h : x.Coprime n
⊢ (↑x)⁻¹ * ↑x = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
by

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
h : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u).val.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ IsUnit ↑m ↔ m.Coprime n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
this : (m % n).gcd n = m.gcd n
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ m % n ≡ m [MOD n]

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ (m % n).Coprime n ↔ m.Coprime n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ p.divisors = {1, p}

Tactic:
by

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

Goal state before:
pp: p d a : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ IsUnit ↑a ↔ ¬p ∣ a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
⊢ p.properDivisors = {1}

Tactic:
by

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

Goal state before:
pp: p d : ℕ
hp : Nat.Prime p
hd : 0 < d
⊢ ¬IsUnit ↑p

Tactic:
by

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
⊢ 0 < ∑ i ∈ range n, x ^ i ↔ Odd n ∨ 0 < x + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).divisors = map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range (k + 1))

Tactic:
by

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

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u)⁻¹ = ↑u⁻¹

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod n
h : IsUnit a
⊢ a * a⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod n
h : IsUnit a
⊢ a⁻¹ * a = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ -1 * -1 = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
by
  -- ideally, this would be `ha.inv_mul_eq_one`, but `ZMod n` is not a `DivisionMonoid`...
  -- (see the "TODO" above)
  refine ⟨fun H ↦ ?_, fun H ↦ H ▸ a.inv_mul_of_unit ha⟩
  apply_fun (a * ·) at H
  rwa [← mul_assoc, a.mul_inv_of_unit ha, one_mul, mul_one, eq_comm] at H

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : { x // x.val.Coprime n }
val✝ : ZMod n
property✝ : val✝.val.Coprime n
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ unitOfCoprime (↑x).val ⋯) ⟨val✝, property✝⟩) = ⟨val✝, property✝⟩

Tactic:
by

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
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
by

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
x✝ : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ ∑ i ∈ range n, x ^ i = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors

Tactic:
by

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
⊢ ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : ∑ x ∈ n.properDivisors, x ∣ n
⊢ ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.properDivisors, f x = f 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.divisors, f x = f p * f 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ 1 ∈ n.properDivisors

Tactic:
by

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
⊢ ∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors = {1} ↔ Prime n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.zero
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ↔ Prime (0 + 1)

Tactic:
simp [Nat.not_prime_one]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ n.properDivisors, x = 1 ↔ Prime n

Tactic:
by

Goal state after:
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
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).properDivisors = map { toFun := fun x ↦ p ^ x, inj' := ⋯ } (range k)

Tactic:
by

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:
← Nat.div_div_eq_div_mul

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: α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).properDivisors, f x = ∏ x ∈ range k, f (p ^ x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ (p ^ k).divisors, f x = ∏ x ∈ range (k + 1), f (p ^ x)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = {p ∈ n.divisors | Prime p}

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
⊢ {p ∈ n.primeFactors | p ∣ m} = m.primeFactors

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ image (fun x ↦ n / x) n.divisors = n.divisors

Tactic:
by

Goal state after:
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 / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, f x = f x

Tactic:
by

Goal state after:
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 = ∑ i ∈ range n.succ, a / b ^ i

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 1 ≤ b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
by

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

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ 0 < m

Tactic:
by

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

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ Disjoint (filter IsPrimePow a.divisors) (filter IsPrimePow b.divisors)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
⊢ n.divisorsAntidiagonal = {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}

Tactic:
by

Goal state after:
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
⊢ LeftInverse inv_fun to_fun

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: q : ℕ
hq : 1 < q
k : ℕ
⊢ map ({ toFun := fun k ↦ q ^ k, inj' := ⋯ }.prodMap { toFun := fun k ↦ q ^ k, inj' := ⋯ }) (antidiagonal k) ⊆
    (q ^ k).divisorsAntidiagonal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z✝ z : ℤ
s : Finset ℕ := z.natAbs.divisors
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z : ℤ
n : ℕ
s : Finset (ℕ × ℕ) := n.divisorsAntidiagonal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp +contextual [s, disjoint_left, eq_comm]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z : ℤ
n : ℕ
s : Finset (ℕ × ℕ) := n.divisorsAntidiagonal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
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
left_inv : LeftInverse inv_fun to_fun
⊢ Fintype.card (ZMod m × ZMod n) ≤ Fintype.card (ZMod (m * n))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z : ℤ
n : ℕ
s : Finset (ℕ × ℕ) := (n + 1).divisorsAntidiagonal
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x z : ℤ
⊢ x ∈ z.divisors ↔ ∃ y ∈ z.natAbs.divisors, ↑y = x ∨ -↑y = x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x z : ℤ
y : ℕ
⊢ ↑y = x ∨ -↑y = x ↔ y = x.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x z : ℤ
⊢ x ∈ z.divisors ↔ x ∣ z ∧ z ≠ 0

Tactic:
by

Goal state after:
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
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ 1 ∈ z.divisors ↔ z ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ -1 ∈ z.divisors ↔ z ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z✝ : ℤ
x✝ : z✝.divisors.Nonempty
hx : z✝ = 0
z : ℤ
hz : z ∈ z✝.divisors
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ z.divisors = ∅ ↔ z = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisors = z.divisors

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Subsingleton (ZMod n) ↔ n = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Nontrivial (ZMod n) ↔ n ≠ 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ
⊢ ∀ (a : (ZMod 2)ˣ), a = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.fst z.divisorsAntidiag = z.divisors

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.snd z.divisorsAntidiag = z.divisors

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: x y z : ℤ
hz : z ≠ 0
⊢ (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : Odd n
a : ZMod n
⊢ a + a = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ (-z).divisorsAntidiag = map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
x y z : ℤ
n : ℕ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : ZMod 2
⊢ -a = a

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ ↑|a| = ↑a

Tactic:
by

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

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs = ↑a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ (-↑n).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) n.divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ 0 < a.val ↔ a ≠ 0

Tactic:
by

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

Goal state before:
pp: hn : 1 < 0
x✝ : ZMod 0
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
by

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

Goal state before:
pp: hn : 1 < 1
x✝ : ZMod 1
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝¹ : 1 < n + 2
x✝ : ZMod (n + 2)
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
by

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

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

Tactic:
by

Goal state after:
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.choose k) < ↑n ^ k / ↑k !

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ 1 < k !

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
⊢ a * b ∈ {1, 2, 3} ↔
    (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
by

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

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ (n + 1 - k) ^ k

Tactic:
by

Goal state after:
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)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ a * b ∈ {0, 1, 2, 3, 4} ↔
    (a, b) ∈
      {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
        (-4, -1), (-1, -4), (2, 2), (-2, -2)}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).choose k ≤ 2 ^ n

Tactic:
by

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

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ n.choose k < 2 ^ n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (n : ℕ), n.centralBinom < (n + 1).centralBinom

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.centralBinom ≤ 4 ^ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ n.centralBinom < 4 ^ n

Tactic:
by

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

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

Tactic:
by

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

Goal state after: