mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
·

Goal state after:
case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun

pp: case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
·

Goal state after:
case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ LeftInverse inv_fun to_fun
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
·

Goal state after:
case inl.right
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⋯
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) := ⋯
hmn0 : 0 * 1 = 0
⊢ RightInverse inv_fun to_fun
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
h : ∑ x ∈ properDivisors 0, x ∣ 0
⊢ ∑ x ∈ properDivisors 0, x = 1 ∨ ∑ x ∈ properDivisors 0, x = 0

pp: case succ
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1

Tactic:
·

Goal state after:
case zero
h : ∑ x ∈ properDivisors 0, x ∣ 0
⊢ ∑ x ∈ properDivisors 0, x = 1 ∨ ∑ x ∈ properDivisors 0, x = 0
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
·

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

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

pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1

Tactic:
·

Goal state after:
case succ.zero
h : ∑ x ∈ (0 + 1).properDivisors, x ∣ 0 + 1
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (0 + 1).properDivisors, x = 0 + 1
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
·

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

Goal state after:
case inr
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun ∧ RightInverse inv_fun to_fun
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun

pp: case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
·

Goal state after:
case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ LeftInverse inv_fun to_fun
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
⊢ ∑ x ∈ properDivisors 0, x = 1 ↔ Prime 0

pp: case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)

Tactic:
·

Goal state after:
case zero
⊢ ∑ x ∈ properDivisors 0, x = 1 ↔ Prime 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun

Tactic:
·

Goal state after:
case inr.right
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⋯
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) := ⋯
hmn0 : 1 * 0 = 0
⊢ RightInverse inv_fun to_fun
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
·

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

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

pp: case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
·

Goal state after:
case succ.zero
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ↔ Prime (0 + 1)
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
·

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

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

pp: case mpr
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ j, ∃ (_ : j < k), x = p ^ j) → (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k

Tactic:
·

Goal state after:
case mp
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k → ∃ j, ∃ (_ : j < k), x = p ^ j
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case zero
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

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

Tactic:
·

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

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

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.Divisors

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

pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
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
Module: Mathlib.NumberTheory.Divisors

Goal state before:
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
⊢ Set.InjOn (HDiv.hDiv n) ↑n.divisors
Module: Mathlib.Algebra.Order.Ring.GeomSum

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

Tactic:
by lia

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 lia

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 lia

Goal state after:
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.val ≡ x.val [MOD m]

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.val ≡ x.val [MOD n]

Tactic:
·

Goal state after:
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.val ≡ x.val [MOD m]
Module: Mathlib.NumberTheory.Divisors

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

pp: case mpr
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n → n1 * n2 = n ∧ ¬n = 0

Tactic:
·

Goal state after:
case mp
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ n1 * n2 = n ∧ ¬n = 0 → ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
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.val ≡ x.val [MOD n]

Tactic:
·

Goal state after:
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.val ≡ x.val [MOD n]
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
·

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

Goal state before:
pp: case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1

pp: case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.zero
⊢ Subsingleton (ZMod 0) → 0 = 1

pp: case mp.succ.zero
⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
·

Goal state after:
case mp.zero
⊢ Subsingleton (ZMod 0) → 0 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.succ.zero
⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
·

Goal state after:
case mp.succ.zero
⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
·

Goal state after:
case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
·

Goal state after:
case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
ext; simp [mem_divisorsAntidiag]

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

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

Tactic:
← ZMod.coe_unitOfCoprime 2 hn,

Goal state after:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a * ↑(unitOfCoprime 2 hn) = 0 ↔ a = 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
simp [pos_iff_ne_zero]

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

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

pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
·

Goal state after:
case zero
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0
Module: Mathlib.Data.ZMod.Basic

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

pp: case succ.mpr
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1 → n✝ + 1 ∣ 2 * a.val

Tactic:
·

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

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

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

Tactic:
·

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

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

pp: case inr
n k : ℕ
h : n < k
⊢ n.choose k ≤ (n + 1 - k) ^ k

Tactic:
·

Goal state after:
case inl
n k : ℕ
h : k ≤ n
⊢ n.choose k ≤ (n + 1 - k) ^ k
Module: Mathlib.Data.Nat.Choose.Bounds

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

Tactic:
·

Goal state after:
case inr
n k : ℕ
h : n < k
⊢ n.choose k ≤ (n + 1 - k) ^ k
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)
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) * (0 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 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) * (0 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1
Module: Mathlib.Data.Nat.Choose.Bounds

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

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

Tactic:
·

Goal state after:
case pos
n k : ℕ
lt : n + 1 < k
⊢ (n + 1).choose k ≤ 2 ^ n
Module: Mathlib.Data.Nat.Choose.Bounds

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

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case succ.mpr.inl
n✝ : ℕ
⊢ n✝ + 1 ∣ 2 * val 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
apply dvd_zero

Goal state after:
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 ∣ 2 * a.val

Tactic:
·

Goal state after:
case succ.mpr.inr
n✝ : ℕ
a : ZMod (n✝ + 1)
h : 2 * a.val = n✝ + 1
⊢ n✝ + 1 ∣ 2 * a.val
Module: Mathlib.Data.ZMod.Basic

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

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

Tactic:
·

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

Goal state before:
pp: case inl
k : ℕ
⊢ choose 0 k ≤ 2 ^ 0

pp: case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n

Tactic:
·

Goal state after:
case inl
k : ℕ
⊢ choose 0 k ≤ 2 ^ 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n

Tactic:
·

Goal state after:
case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n
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
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝¹ : NeZero n
m : ℕ
inst✝ : NeZero (m + 1)
a : ZMod (m + 1)
h : n ≤ m
⊢ a.cast.val < m + 1
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom

pp: case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

pp: case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
·

Goal state after:
case h.inl
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4

pp: case h.inr.inr
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
·

Goal state after:
case h.inr.inl
IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4
Module: Mathlib.Data.ZMod.Basic

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

pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.ZMod.Basic

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

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

Tactic:
·

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
⊢ (a - b).val = a.val - b.val