mathlib-initiative/mathlib-tactics huggingface dataset:
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 * a ^ k)

Tactic:
]

Goal state after:
α : 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 * a ^ k)
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
⊢ ψ 1 = 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ ψ 1 = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ y ∈ fixedLengthDigits hb l, ∑ x ∈ Finset.range b, (x + y.sum) = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ f ≤ n.factorization

pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0

Tactic:
]

Goal state after:
case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ f ≤ n.factorization

n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
]

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ a ^ 1 ∣ a ∧ ¬a ^ (1 + 1) ∣ a

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ a ^ 1 ∣ a ∧ ¬a ^ (1 + 1) ∣ a
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 = x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = a ^ 2 * v
⊢ False

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : a * 1 = a ^ 2 * v
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card • ∑ x ∈ Finset.range b, x +
      ∑ x ∈ fixedLengthDigits hb l, (Finset.range b).card • x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
Finset.sum_nsmul,

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card • ∑ x ∈ Finset.range b, x +
      (Finset.range b).card • ∑ x ∈ fixedLengthDigits hb l, x.sum =
    (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n * (f - n.factorization).prod HPow.hPow

Tactic:
]

Goal state after:
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : n.factorization ≤ f
⊢ n ∣ n * (f - n.factorization).prod HPow.hPow
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 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
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 * p ^ multiplicity p b ∣ a * b

Tactic:
]

Goal state after:
α : 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 * p ^ multiplicity p b ∣ a * b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun x1 x2 ↦ x1 ^ x2
⊢ f ≤ n.factorization

Tactic:
]

Goal state after:
n d : ℕ
hd : d ≠ 0
hn : n ≠ 0
x✝ : ∃ f ≤ n.factorization, d = f.prod fun x1 x2 ↦ x1 ^ x2
f : ℕ →₀ ℕ
hle : f ≤ n.factorization
hprod : d = f.prod fun x1 x2 ↦ x1 ^ x2
⊢ f ≤ n.factorization
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 = x

Tactic:
]

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ a.factorization q + b.factorization q = a.factorization q + b.factorization q

Tactic:
]

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
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Tactic:
]

Goal state after:
α : 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
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n

Tactic:
]

Goal state after:
n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l = b ^ l

Tactic:
]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList

Tactic:
]

Goal state after:
n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ ∀ (i : ℕ), a.factorization i ≤ b.factorization i

Tactic:
]

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ ∀ (i : ℕ), a.factorization i ≤ b.factorization i
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b * b ^ (l - 1) * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) =
    (l + 1) * (b * b ^ (l - 1)) * (b * (b - 1) / 2)

Tactic:
]

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b * b ^ (l - 1) * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * (b * (b - 1) / 2)) =
    (l + 1) * (b * b ^ (l - 1)) * (b * (b - 1) / 2)
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 : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n

Tactic:
]

Goal state after:
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 : ℕ
h : ¬a = 1
b : ℕ
ha : n = orderOf x * b * a.minFac
hb : a = b * a.minFac
⊢ a.minFac ∣ n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : 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:
]

Goal state after:
case pos
α : 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)
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b
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
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

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
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x

Tactic:
]

Goal state after:
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
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

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
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r

Tactic:
]

Goal state after:
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ r

Tactic:
]

Goal state after:
case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ r
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n : ℕ
⊢ Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1

Tactic:
]

Goal state after:
n : ℕ
⊢ Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ ((single p k).prod fun x1 x2 ↦ x1 ^ x2) = p ^ k
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = ∑ L ∈ List.fixedLengthDigits hb l, L.sum

Tactic:
]

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = ∑ L ∈ List.fixedLengthDigits hb l, L.sum
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

Tactic:
classical
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_isUnit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ List.fixedLengthDigits hb l
⊢ L.sum = L.sum

Tactic:
]

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
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
]

Goal state after:
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
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ ∃ n, 0 < n ∧ x ^ n = 1
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
exact_mod_cast (ha.pow hp).emultiplicity_eq_multiplicity ▸
    ha.emultiplicity_eq_multiplicity ▸ emultiplicity_pow hp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n

Tactic:
]

Goal state after:
case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / (p ^ a.factorization p * p ^ b.factorization p) = a * b / (p ^ a.factorization p * p ^ b.factorization p)

Tactic:
]

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p + n !.factorization p = (n + 1).factorization p + n !.factorization p

Tactic:
]

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ (n + 1).factorization p = #({i ∈ Ico 1 b | p ^ i ∣ n + 1})
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Monoid G
x : G
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
⊢ 0 < orderOf x ↔ 0 < orderOf x

Tactic:
]

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 : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p = 1
⊢ False

Tactic:
]

Goal state after:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p = 1
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≠ 1 ∧ b ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Tactic:
]

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization

Tactic:
]

Goal state after:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d.factorization ≤ n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
]

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

Goal state before:
pp: case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b

Tactic:
]

Goal state after:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
]

Goal state after:
a b : ℕ
ha : a ≠ 0
⊢ b.factorization ≤ (b * a).factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ k ≤ n.factorization p ↔ k ≤ n.factorization p

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : n ≠ 0
dvd : n ∣ orderOf x
⊢ orderOf x / n = orderOf x / n

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ n = n

pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a

Tactic:
]

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ p, a.factorization p < b.factorization p

Tactic:
by
  have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
  contrapose! hab
  rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
  exact le_of_dvd ha.bot_lt hab

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf y = orderOf y

Tactic:
]

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

Goal state before:
pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ n.factorization = n.factorization

Tactic:
]

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

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

Tactic:
]

Goal state after:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n / p ^ n.factorization p).factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
]

Goal state after:
n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬1 ≤ (n.factorization - (p ^ n.factorization p).factorization) p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf y = orderOf y

Tactic:
]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p + ((n + 1).factorization p + 1) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x ↦ a ^ x) (Finset.range (orderOf a)))).Finite

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x ↦ a ^ x) (Finset.range (orderOf a)))).Finite
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
⊢ minimalPeriod ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) 1 ∣ (orderOf x).lcm (orderOf y)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q

Tactic:
]

Goal state after:
case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i ∈ Ico 1 (log p n + 1), n / p ^ i ≤ n / (p - 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0

Tactic:
]

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n k p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n / p ^ n.factorization p

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) 1 = orderOf x * orderOf y

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hco : (orderOf x).Coprime (orderOf y)
⊢ minimalPeriod ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) 1 = orderOf x * orderOf y
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ ¬p ∣ n / p ^ n.factorization p

Tactic:
]

Goal state after:
case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ ¬p ∣ n / p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ m / p ^ m.factorization p = m

Tactic:
]

Goal state after:
m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ m / p ^ m.factorization p = m
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: k m p : ℕ
hp : Prime p
⊢ m = 0 ∨ ¬p ∣ m ↔ m = 0 ∨ ¬p ∣ m

Tactic:
]

Goal state after: