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

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ n.factorization p = padicValNat p n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : ∀ (n : ℕ), a ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ count p n.primeFactorsList = n.factorization p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b✝ : ℕ
hb : ¬b✝ = 0
b : ℕ
h : ∀ (n : ℕ), (b + 2) ^ n ∣ b✝
ha : b + 2 ≠ 0
ha1 : b + 2 ≠ 1
x✝ : b + 2 ≤ 1
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
H : Submonoid G
x : ↥H
⊢ IsOfFinOrder ↑x ↔ IsOfFinOrder x

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.factorization = Multiset.toFinsupp ↑n.primeFactorsList

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ FiniteMultiplicity a b ↔ a ≠ 1 ∧ 0 < b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
⊢ emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
⊢ 0 < n.factorization p

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝¹ : ℕ
x✝ : x✝¹ ∈ {n | n < b ^ l}
⊢ ofDigits b (b.digitsAppend l x✝¹) = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
a b : α
h : FiniteMultiplicity a b
n : ℕ
hn : ¬a ^ (n + 1) ∣ b
hb : b = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ y ^ n = 1

Tactic:
by

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

Goal state before:
pp: n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ multiplicity p n = n.factorization p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
⊢ IsOfFinOrder x → IsOfFinOrder y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
hf : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ofDigits b (b.digitsAppend l (ofDigits b L)) = ofDigits b L

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ f x ^ n = 1

Tactic:
by

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), a.factorization p = b.factorization p
⊢ a.primeFactorsList ~ b.primeFactorsList

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
p a b : α
⊢ min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ f x ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b

Tactic:
by

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

Goal state before:
pp: a : ℕ
ha : a ∈ {x | x ≠ 0}
b : ℕ
hb : b ∈ {x | x ≠ 0}
h : a.factorization = b.factorization
p : ℕ
⊢ a.factorization p = b.factorization p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ emultiplicity a (-b) = emultiplicity a b

Tactic:
by

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

Goal state before:
pp: ⊢ factorization 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
by

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

Goal state before:
pp: ⊢ factorization 1 = 0

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.InvOn (b.digitsAppend l) (ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} {n | n < b ^ l}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝ : Monoid G
a b x y : G
n m : ℕ
hx : IsOfFinOrder x
⊢ Group ↥(powers x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Subsingleton G
x : G
⊢ orderOf x = 1

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ n.factorization p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a : ℕ
b : ℤ
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
x✝ : emultiplicity p b = ⊤
⊢ False

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hp : ¬Prime p
⊢ n.factorization p = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ x ^ orderOf x = 1

Tactic:
by

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

Goal state before:
pp: n p : ℕ
h : ¬p ∣ n
⊢ n.factorization p = 0

Tactic:
by

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

Goal state before:
pp: n p : ℕ
h : ¬p ∣ n
⊢ n.factorization p = 0

Tactic:
by
  simp [factorization_eq_zero_iff, h]

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digits (ofDigits b L)).sum = L.sum

Tactic:
by

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

Goal state before:
pp: p r i : ℕ
hr : ¬p ∣ r
⊢ (p * i + r).factorization p = 0

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Finset (List ℕ)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ orderOf x = 0

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb l ↔ L.length = l ∧ ∀ x ∈ L, x < b

Tactic:
by

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: M₀ : Type u_6
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
⊢ orderOf 0 = 0

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) ↑(fixedLengthDigits hb l) ↑(Finset.range (b ^ l))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = emultiplicity p b

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) ↑(Finset.range (b ^ l)) ↑(fixedLengthDigits hb l)

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 0 = {[]}

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ fixedLengthDigits hb 1 = Finset.image (fun x ↦ [x]) (Finset.range b)

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (fixedLengthDigits hb l).card = b ^ l

Tactic:
by

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ d ∣ n

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a - b) = emultiplicity p b

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
⊢ L.head ⋯ = d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (a - b) = multiplicity p b

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ d :: L ∈ fixedLengthDigits hb (l + 1)

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ (↑(Finset.range b)).PairwiseDisjoint fun d ↦ consFixedLengthDigits hb l d

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : 0 < n
⊢ orderOf x = n ↔ x ^ n = 1 ∧ ∀ m < n, 0 < m → x ^ m ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ 0 < orderOf x ↔ IsOfFinOrder x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : IsOfFinOrder x
h : orderOf y ∣ orderOf x
⊢ IsOfFinOrder y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
⊢ emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
h : x ^ n = 1
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) n 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
⊢ L ≠ []

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
⊢ orderOf 1 = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 1 ↔ x = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n

Tactic:
by

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

Goal state before:
pp: n k : ℕ
⊢ (n ^ k).factorization = k • n.factorization

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : orderOf x ∣ n
⊢ x ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
⊢ 2 * (r + 1) = 2 * r + 1 + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
⊢ a * b = p * (p ^ (n + m) * s)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : n = 0
⊢ False

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.factorization = single p 1

Tactic:
by

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

Goal state before:
pp: p k : ℕ
hp : Prime p
⊢ (p ^ k).factorization = single p k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
⊢ x ^ (2 * (r + 1)) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
x✝ : p ^ (n - 1 + 1) ∣ x
y : α
hy : x = p ^ (n - 1 + 1) * y
⊢ p * x * p = p ^ (n + 1) * y * p

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ¬p ^ (n.factorization p + 1) ∣ n

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n r : ℕ
hx : x ^ (2 * r + 1) = 1
key : x ^ (2 * (r + 1)) = x
⊢ x ^ n = x ^ (2 * ((r + 1) * n))

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ n ≠ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ n.factorization n.minFac ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hx : x ^ p = 1
hp : Odd p
n : ℕ
⊢ ∃ m, x ^ n = x ^ (2 * m)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this✝ : p ∣ a * b
x✝ : p ∣ a
x : α
hx : a = p * x
hn0 : 0 < n
hpx : ¬p ^ (n - 1 + 1) ∣ x
this : 1 ≤ n + m
⊢ x * b * p = p ^ (n - 1 + m + 1) * s * p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ orderOf (x ^ n) ∣ orderOf x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : m = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) (Set.Iio (orderOf x))

Tactic:
by

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

Goal state before:
pp: f : ℕ →₀ ℕ
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2).factorization = f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n a : ℕ
hx : x ^ n = 1
c : ℕ
h : a ≡ a + c [MOD n]
hle : a ≤ a + c
⊢ n ∣ c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝² : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝¹ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
x✝ : p ^ (m - 1 + 1) ∣ x
y : α
hy : x = p ^ (m - 1 + 1) * y
⊢ p * x * p = p ^ (m + 1) * y * p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n b : ℕ
hx : x ^ n = 1
c : ℕ
h : b + c ≡ b [MOD n]
hle : b ≤ b + c
⊢ n ∣ c

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization ↔ (f.prod fun x1 x2 ↦ x1 ^ x2) = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
hp : Prime p
a b : α
n m : ℕ
ha : ¬p ^ (n + 1) ∣ a
hb : ¬p ^ (m + 1) ∣ b
x✝¹ : p ^ (n + m + 1) ∣ a * b
s : α
hs : a * b = p ^ (n + m + 1) * s
this : p ∣ a * b
x✝ : p ∣ b
x : α
hx : b = p * x
hm0 : 0 < m
hpx : ¬p ^ (m - 1 + 1) ∣ x
⊢ a * x * p = p ^ (n + (m - 1) + 1) * s * p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n a b : ℕ
h : a ≡ b [MOD n]
hx : x ^ n = 1
⊢ x ^ a = x ^ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k : ℕ
x✝ : FiniteMultiplicity p a
⊢ ¬p ^ (0 + 1) ∣ a ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (ψ x) ∣ orderOf x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a ^ (k + 1))

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ (x ^ n) ^ 1 = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ ∀ (a : ℕ), a ^ 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
⊢ multiplicity a a = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
hfin : FiniteMultiplicity a a
⊢ emultiplicity a a = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ (x ^ n) ^ 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ 1 < orderOf x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b

Tactic:
by

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by

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

Goal state before:
pp: p a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization p = a.factorization p + b.factorization p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x

Tactic:
by

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
this : a = 1
⊢ orderOf x = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ p ^ n.factorization p ∣ n

Tactic:
by

Goal state after: