mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ (d / d).factorization = d.factorization - d.factorization → d ∣ d

pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
⊢ (n / d).factorization = n.factorization - d.factorization → d ∣ n

Tactic:
·

Goal state after:
case inl
d : ℕ
hd : d ≠ 0
hdn : d ≤ d
⊢ (d / d).factorization = d.factorization - d.factorization → d ∣ d
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
·

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case pos
p n k : ℕ
h : (n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

pp: case neg
p n k : ℕ
h : ¬(n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
·

Goal state after:
case pos
p n k : ℕ
h : (n.choose k).factorization p = 0
⊢ (n.choose k).factorization p ≤ log p n
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1

pp: case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1

Tactic:
·

Goal state after:
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ (n.choose k).factorization p = 0

pp: case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ (n.choose k).factorization p = 0

Tactic:
·

Goal state after:
case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0

pp: case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
·

Goal state after:
case inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi : i < log p n + 1
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
rcases eq_or_lt_of_le hi₁ with (rfl | hi)

Goal state after:
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1

case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1

pp: case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
·

Goal state after:
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi₁ : 1 ≤ 1
hi : 1 < log p n + 1
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

pp: case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
·

Goal state after:
case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1

pp: case neg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ orderOf (-1) = 2

Tactic:
·

Goal state after:
case pos
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ringChar R = 2
⊢ orderOf (-1) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p

pp: case inr.inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
ha0 : a ≠ 0
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
·

Goal state after:
case inr.inl
b : ℕ
hb0 : b ≠ 0
p : ℕ
pp : Prime p
hab : 0 ∣ b
⊢ p ^ (factorization 0) p ∣ p ^ b.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg.hg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1

pp: case hg1
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ -1 ≠ 1

Tactic:
·

Goal state after:
case neg.hg
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ (-1) ^ 2 = 1
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i

Tactic:
·

Goal state after:
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi₁ : 1 ≤ i
hi✝ : i < log p n + 1
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

pp: case inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
·

Goal state after:
case inl
a b : ℕ
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2

pp: case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n

Tactic:
·

Goal state after:
case refine_1
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n

Tactic:
·

Goal state after:
case refine_2
p n : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p

pp: case inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
·

Goal state after:
case inr.inl
a p : ℕ
pp : Prime p
hab : a ∣ 0
⊢ a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

pp: G : Type u_1
inst✝ : Monoid G
x : G
n✝ m✝ : ℕ
hx : IsOfFinOrder x
n m : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Monoid G
x : G
n m : ℕ
hx : IsOfFinOrder x
this : ∀ {n m : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

pp: case neg
p n k : ℕ
h : n < p
hnk : k ≤ n
⊢ (n.choose k).factorization p = 0

Tactic:
·

Goal state after:
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ (factorization 0) p ∣ b / p ^ b.factorization p

pp: case inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
⊢ a / p ^ a.factorization p ∣ b / p ^ b.factorization p

Tactic:
·

Goal state after:
case inr.inr.inl
b p : ℕ
pp : Prime p
hb0 : b ≠ 0
hab : 0 ∣ b
⊢ 0 / p ^ (factorization 0) p ∣ b / p ^ b.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case h
n k : ℕ
hkn : k ≤ n
⊢ (n.choose k).factorization.support ⊆ Finset.range (n + 1)

pp: case hf
n k : ℕ
hkn : k ≤ n
⊢ ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) x ((n.choose k).factorization x) = 1

Tactic:
·

Goal state after:
case h
n k : ℕ
hkn : k ≤ n
⊢ (n.choose k).factorization.support ⊆ Finset.range (n + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ a.factorization q ≠ 0
hb : b / q ^ b.factorization q ≠ 0
⊢ (Finsupp.erase q a.factorization) q ≤ (Finsupp.erase q b.factorization) q

pp: case inr.inr.inr.inr
a b : ℕ
hab : a ∣ b
p : ℕ
pp : Prime p
hb0 : b ≠ 0
ha0 : a ≠ 0
ha : a / p ^ a.factorization p ≠ 0
hb : b / p ^ b.factorization p ≠ 0
q : ℕ
hqp : q ≠ p
⊢ (Finsupp.erase p a.factorization) q ≤ (Finsupp.erase p b.factorization) q

Tactic:
·

Goal state after:
case inr.inr.inr.inl
a b : ℕ
hab : a ∣ b
hb0 : b ≠ 0
ha0 : a ≠ 0
q : ℕ
pp : Prime q
ha : a / q ^ a.factorization q ≠ 0
hb : b / q ^ b.factorization q ≠ 0
⊢ (Finsupp.erase q a.factorization) q ≤ (Finsupp.erase q b.factorization) q
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case hf
n k : ℕ
hkn : k ≤ n
⊢ ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) x ((n.choose k).factorization x) = 1

Tactic:
·

Goal state after:
case hf
n k : ℕ
hkn : k ≤ n
⊢ ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support → (fun x1 x2 ↦ x1 ^ x2) x ((n.choose k).factorization x) = 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0

pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
⊢ a ∣ b

Tactic:
·

Goal state after:
case inl
a : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ 0 / p ^ (factorization 0) p
⊢ a ∣ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
h : orderOf x = 0
n m : ℕ
⊢ x ^ n = x ^ m ↔ n = m

Tactic:
rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]

Goal state after:
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i < b

pp: case succ
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
m : ℕ
hm : m + 1 ≠ 1
hb : log (m + 1) n < b
fin : FiniteMultiplicity (m + 1) n
h : (m + 1) ^ i ∣ n
⊢ i < b

Tactic:
·

Goal state after:
case zero
n b : ℕ
hn : 0 < n
i : ℕ
hi : 1 ≤ i
hm : 0 ≠ 1
hb : log 0 n < b
fin : FiniteMultiplicity 0 n
h : 0 ^ i ∣ n
⊢ i < b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0

pp: case inr
n d : ℕ
hn : n ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
·

Goal state after:
case inl
d : ℕ
⊢ d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n

pp: case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
·

Goal state after:
case inr.inl
n : ℕ
hn : n ≠ 0
⊢ 0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n✝ m n : ℕ
hmn : m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m n : ℕ
this : ∀ {m n : ℕ}, m ≤ n → (x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x])
hmn : ¬m ≤ n
⊢ x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mp
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m → m + k ≡ m [MOD orderOf x]

pp: case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ (m + k) = x ^ m → m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n d : ℕ
⊢ d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  rcases eq_or_ne d 0 with (rfl | hd)
  · simp only [zero_dvd_iff, hn, false_iff, not_forall]
    exact ⟨2, n, prime_two, dvd_zero _, mt (le_of_dvd hn.bot_lt) (n.lt_two_pow_self).not_ge⟩
  refine ⟨fun h p k _ hpkd => dvd_trans hpkd h, ?_⟩
  rw [← factorization_prime_le_iff_dvd hd hn]
  intro h p pp
  simp_rw [← pp.pow_dvd_iff_le_factorization hn]
  exact h p _ pp (ordProj_dvd _ _)

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
·

Goal state after:
case pos
n : ℕ
hn : n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n

Tactic:
·

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
⊢ ∏ p ∈ n.primeFactors, p ∣ n
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ k ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk✝ : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ p ^ n - k ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ a

pp: case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
·

Goal state after:
case hda
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b

pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
·

Goal state after:
case hdb
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ((a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2) ∣ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : RightCancelMonoid G
a : G
ha : ¬IsOfFinOrder a
⊢ Nat.card ↥(powers a) = orderOf a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
·

Goal state after:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
⊢ ∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 = x ^ 1 + y ^ 1

pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 = x ^ 1 + y ^ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ -↑i ↔ x ^ (-↑i) = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n

pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
x y : R
n : ℕ
h : Commute x y
inst✝ : CharZero R
⊢ (x + y) ^ 1 ^ n = x ^ 1 ^ n + y ^ 1 ^ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

pp: case hd.inr
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
he_pos : e ≠ 0
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
·

Goal state after:
case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

pp: case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar✝ : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
⊢ orderOf 1 ≤ 1

pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1

Tactic:
·

Goal state after:
case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
⊢ orderOf 1 ≤ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : IsMulTorsionFree G
g : G
ha : g ≠ 1
⊢ orderOf g ≤ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (↑n.divisors).PairwiseDisjoint fun m ↦ {x | orderOf x = m}

pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ (↑n.divisors).PairwiseDisjoint fun m ↦ {x | orderOf x = m}
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝² : Monoid G
n : ℕ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hn : n ≠ 0
⊢ #(n.divisors.biUnion fun m ↦ {x | orderOf x = m}) = #{x | x ^ n = 1}