mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : LeftCancelMonoid G
inst✝² : Finite G
x y : G
n : ℕ
H : Type u_6
inst✝¹ : RightCancelMonoid H
inst✝ : Finite H
⊢ Group H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
x y : G
h : orderOf x = orderOf y
n : ℕ
⊢ (powersEquivPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : Finite Gˣ
x : G
⊢ IsOfFinOrder x ↔ IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G₀ : Type u_6
inst✝¹ : GroupWithZero G₀
inst✝ : Finite G₀
a : G₀
⊢ orderOf a = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]

Tactic:
by

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
m n : ℤ
⊢ x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ (fun n ↦ x ^ n) ↑n = (fun n ↦ x ^ n) 0

Tactic:
by

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

Goal state before:
pp: β : Type u_1
inst✝ : CommMonoid β
m n : ℕ
f : ℕ → β
⊢ (m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ ↑p * x
⊢ r ∣ (x + y) ^ p - y ^ p

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
by

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
⊢ emultiplicity p ((n + k).choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}))

Tactic:
by

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

Goal state before:
pp: n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ {i | i ≠ 0 ∧ p ^ i ∣ n} = Set.Icc 1 (n.factorization p)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ x = y ∨ x⁻¹ = y → zpowers x = zpowers y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : NonAssocRing R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Finite R
⊢ p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
⊢ x ∈ zpowers y

Tactic:
by

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ emultiplicity p (n.choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
hx_mem : x ∈ zpowers y
⊢ y ∈ zpowers x

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
x✝ : ℕ
⊢ emultiplicity p x✝ ≤ emultiplicity p (x✝.choose 0) + emultiplicity p 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n✝ : ℕ
⊢ emultiplicity p 0 ≤ emultiplicity p (choose 0 (n✝ + 1)) + emultiplicity p (n✝ + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ Nat.Prime (ringChar R)

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n k : ℕ
⊢ emultiplicity p (n + 1) ≤ emultiplicity p ((n + 1).choose (k + 1)) + emultiplicity p (k + 1)

Tactic:
by

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ Disjoint ({i ∈ Ico 1 n.succ | p ^ i ≤ k % p ^ i + (p ^ n - k) % p ^ i}) ({i ∈ Ico 1 n.succ | p ^ i ∣ k})

Tactic:
by

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

Goal state before:
pp: n p : ℕ
pp : Prime p
⊢ Icc 1 (n.factorization p) = {i ∈ Ico 1 n | p ^ i ∣ n}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p n : ℕ
inst✝ : ExpChar R p
⊢ iterateFrobenius R p n = frobenius R p ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 1) x = x ^ p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p 0) x = x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m * n)) x = (⇑(iterateFrobenius R p m))^[n] x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
f : R →* S
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : ExpChar S p
x : R
n : ℕ
⊢ f ((iterateFrobenius R p n) x) = (iterateFrobenius S p n) (f x)

Tactic:
by

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

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : 0 ^ i ∣ n
⊢ i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers y ↔ x = y ∨ x⁻¹ = y

Tactic:
by

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

Goal state before:
pp: n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n < p ^ b
⊢ {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Ico 1 b | p ^ i ∣ n}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1

Tactic:
by

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

Goal state before:
pp: b m n : ℕ
hm : Prime m
hn : 0 < n
hb : n < m ^ b
⊢ n.factorization m = #({i ∈ Ico 1 b | m ^ i ∣ n})

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℕ
⊢ g ∈ zpowers (g ^ k) ↔ k.gcd (orderOf g) = 1

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k ≠ p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
by

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
⊢ p ∣ (p ^ n).choose k ↔ k ≠ 0 ∧ k ≠ p ^ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
x y : G
inst✝ : Finite G
h : orderOf x = orderOf y
n : ℕ
⊢ (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
s : Set G
⊢ ∀ x ∈ s, IsOfFinOrder x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ card ↥(zpowers a) ≤ k

Tactic:
by

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

Goal state before:
pp: h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 (2 * n)! < ↑(2 * n)

Tactic:
by

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b ↔ ∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ orderOf x ∣ card G

Tactic:
by

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

Goal state before:
pp: h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this✝ : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
this : emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
x : G
⊢ orderOf x ∣ Nat.card G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Subgroup G
x : G
hx : x ∈ s
⊢ orderOf x ∣ Nat.card ↥s

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ orderOf x ≤ Nat.card ↥s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ x ^ card G = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
g : G
⊢ 0 /ᵒᶠ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
⊢ x /ᵒᶠ 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x y : k[G]
g : G
⊢ (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a b : G
⊢ x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
x : k[G]
⊢ of' k G a * x /ᵒᶠ a = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
a : G
⊢ x * of' k G a /ᵒᶠ a = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
a : G
⊢ of' k G a /ᵒᶠ a = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x %ᵒᶠ g).coeff g' = x.coeff g'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ ¬¬∃ g₂, g' = g + g₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
⊢ g ^ H.index ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ (x %ᵒᶠ g).coeff g' = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℕ
⊢ a ^ (n % card G) = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℤ
⊢ a ^ (n % ↑(card G)) = a ^ n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G) = a ^ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
m : ℕ
pr : n < m
⊢ ∏ p ∈ Finset.range m with Prime p, p ^ padicValNat p n = n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n % ↑(Nat.card G)) = a ^ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n = ∏ p, ↑p ^ n.factorization ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g : G
⊢ x * of' k G g %ᵒᶠ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0

Tactic:
by

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

Goal state before:
pp: case refine_2
n : ℕ
p1 p2 : ↥n.primeFactors
hp : p1 ≠ p2
⊢ Prime ↑p2

Tactic:
· exact Nat.prime_of_mem_primeFactors p2.2

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

Goal state before:
pp: n : ℕ
⊢ _root_.Pairwise (Function.onFun Coprime fun p ↦ ↑p ^ n.factorization ↑p)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ∣ (∏ p ∈ n.primeFactors, p) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ n ∣ k ^ n ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.divX.coeff n = p.coeff (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (p.divX * X + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ), (X * p.divX + C (p.coeff 0)).coeff n = p.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a).divX.coeff n = coeff 0 n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a).divX.coeff n = coeff 0 n

Tactic:
by simp [coeff_divX]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.divX = 0
⊢ p = C (p.coeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = C (p.coeff 0)
⊢ p.divX = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ (n : ℕ), (p + q).divX.coeff n = (p.divX + q.divX).coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ divX 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
⊢ (C a * p).divX = C a * p.divX

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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
⊢ (fun g ↦ g ^ (Nat.card G).gcdB n) ((fun g ↦ g ^ n) g) = g

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (∃ m, n ∣ k ^ m) ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
⊢ (X ^ n).divX = if n = 0 then 0 else X ^ (n - 1)

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ #({e ∈ Finset.range n | p ∣ e + 1}) = n / p

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ #({x ∈ Ioc 0 n | p ∣ x}) = n / p

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✝² : Group G✝
x✝ y : G✝
inst✝¹ : Fintype G✝
x : G✝
n : ℕ
G : Type u_6
inst✝ : Group G
h : (Nat.card G).Coprime n
g : G
⊢ (fun g ↦ g ^ n) ((fun g ↦ g ^ (Nat.card G).gcdB n) g) = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.divX.natDegree = p.natDegree - 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
x : G
inst✝ : DecidableEq G
⊢ Finset.image (fun i ↦ x ^ i) (Finset.range (orderOf x)) = (↑(zpowers x)).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a * X ^ n).divX = if n = 0 then 0 else C a * X ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ C (p.coeff 0) ≠ 0

Tactic:
by

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

Goal state before:
pp: N n : ℕ
⊢ #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ g • a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ¬C ((C (p.coeff 0)).coeff 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ p.divX.degree < (p.divX * X + C (p.coeff 0)).degree

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g • a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX ≠ 0

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
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
n : ℕ
⊢ a ^ (n + 1) ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.leadingCoeff * X.leadingCoeff ≠ 0

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
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
pow_mem : ∀ a ∈ S, ∀ (n : ℕ), a ^ (n + 1) ∈ S
⊢ 1 ∈ S

Tactic:
by

Goal state after: