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

Goal state before:
pp: p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ p.maxPowDvdDiv (p * n) = (padicValNat p n + 1, n.divMaxPow p)

Tactic:
simpa using

Goal state after:
p n : ℕ
hp : 1 < p
hn : n ≠ 0
⊢ p.maxPowDvdDiv (p * n) = (padicValNat p n + 1, n.divMaxPow p)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≠ 0
n : ℕ
⊢ (p * n).divMaxPow p = n.divMaxPow p

Tactic:
simpa using

Goal state after:
p : ℕ
hp : p ≠ 0
n : ℕ
⊢ (p * n).divMaxPow p = n.divMaxPow p
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k) = (k, 1)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : 1 < p
k : ℕ
⊢ p.maxPowDvdDiv (p ^ k) = (k, 1)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≠ 0
k : ℕ
⊢ (p ^ k).divMaxPow p = 1

Tactic:
simpa using

Goal state after:
p : ℕ
hp : p ≠ 0
k : ℕ
⊢ (p ^ k).divMaxPow p = 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ p.maxPowDvdDiv p = (1, 1)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : 1 < p
⊢ p.maxPowDvdDiv p = (1, 1)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1

Tactic:
simpa using

Goal state after:
p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : p ≠ 0
⊢ p.divMaxPow p = 1

Tactic:
simpa using

Goal state after:
p : ℕ
hp : p ≠ 0
⊢ p.divMaxPow p = 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b
⊢ D = d

Tactic:
simpa using

Goal state after:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ}, L.length = L2.length → (∀ l ∈ L, l < b) → (∀ l ∈ L2, l < b) → ofDigits b L = ofDigits b L2 → L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b
⊢ D = d
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
simpa using

Goal state after:
case inr.inr
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b : ℕ
l : List ℕ
hl : ∀ x ∈ l, x < b + 2
⊢ ofDigits (b + 2) l < (b + 2) ^ l.length

Tactic:
induction l with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.length_cons, pow_succ]
    have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
    suffices ↑hd < b + 2 by linarith
    exact hl hd List.mem_cons_self

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

Goal state before:
pp: case inr.inr
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
simp [lt_one_iff.mp h]
    cases n
    all_goals simp

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

Goal state before:
pp: case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit false n) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

Tactic:
rw [digits_def' one_lt_two]

Goal state after:
case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

case bit.false
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ 0 < bit false n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b n : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits n).head! = n % b

pp: case neg
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b

Tactic:
· rcases n with _ | n
    · simp
    · nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
      rw [Nat.ofDigits_mod_eq_head! _ _]
      exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm

Goal state after:
case neg
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ ∀ (n : ℕ), a ^ n.succ ∣ b

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ ∀ (n : ℕ), a ^ (n + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : n✝ + 1 ≤ Nat.find h✝
⊢ a ^ (n✝ + 1) ∣ b

Tactic:
simpa using

Goal state after:
case succ.isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
n✝ : ℕ
h✝ : FiniteMultiplicity a b
hk : n✝ + 1 ≤ Nat.find h✝
⊢ a ^ (n✝ + 1) ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ a ∣ b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: n e : ℕ
⊢ 0 < e → n < 10 ^ e → n.repr.length ≤ e

Tactic:
simpa using

Goal state after:
n e : ℕ
⊢ 0 < e → n < 10 ^ e → (toDigits 10 n).length ≤ e
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
simpa using

Goal state after:
case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ ¬p ∣ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) 1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
n : ℕ
hn : 0 < n
han : a ^ n = 1
⊢ a = 1 ∨ n = 0
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
simpa using

Goal state after:
n p : ℕ
pp : Prime p
⊢ ¬Prime p → 0 = padicValNat p n
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:
simpa using

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : ℕ), a.factorization p = b.factorization p
⊢ ∀ (a_1 : ℕ), a.factorization a_1 = b.factorization a_1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b

Tactic:
rw [dvd_add_right]

Goal state after:
case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ b

case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ (multiplicity p b + 1) ∣ a
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
ext
  simp [fixedLengthDigits]
  grind

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

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

Tactic:
simpa using

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l d : ℕ
hd : d < b
L : List ℕ
hL : L ∈ fixedLengthDigits hb l
⊢ L.length = l
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
simpa using

Goal state after:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization
⊢ False
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
rwa [← factorization_le_iff_dvd ?_ hn, factorization_prod_pow_eq_self_of_le_factorization hf]

Goal state after:
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ≠ 0
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
simpa using

Goal state after:
case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
this : IsUnit a
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Tactic:
simpa using

Goal state after:
case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False
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:
simpa using

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.RingTheory.Multiplicity

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

Tactic:
simpa using

Goal state after:
case insert
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : a ∉ s
ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
⊢ emultiplicity p (f a * ∏ x ∈ s, f x) = emultiplicity p (f a) + emultiplicity p (∏ x ∈ s, f x)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p q : ℕ
hp : Prime p
h : p.factorization q ≠ 0
⊢ p = q

Tactic:
simpa using

Goal state after:
p q : ℕ
hp : Prime p
h : p.factorization q ≠ 0
⊢ p = q
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ n.factorization p

Tactic:
simpa using

Goal state after:
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n
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
⊢ p ∣ a

Tactic:
simpa using

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
⊢ p ∣ a
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
⊢ p ∣ b

Tactic:
simpa using

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
⊢ p ∣ b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ Nat.card ↑↑(powers a) ≤ orderOf a

Tactic:
simpa using

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))) ≤ orderOf a
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ x / p / p ^ (x / p).factorization p = x / p ^ x.factorization p

Tactic:
simpa using

Goal state after:
x p : ℕ
hp : Prime p
hx : p ∣ x
⊢ x / p / p ^ (x / p).factorization p = x / p ^ x.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hx : IsOfFinOrder x
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x
⊢ orderOf (x * y) = orderOf x

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hx : IsOfFinOrder x
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x
⊢ orderOf (y * x) = orderOf x
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
simpa using

Goal state after:
case hg1
R : Type u_6
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : ¬ringChar R = 2
⊢ ¬ringChar R = 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 ≤ n + n - n

Tactic:
add_tsub_cancel_left

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

Goal state before:
pp: case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ n.succ.factorization p = 0

Tactic:
factorization_eq_zero_of_lt h

Goal state after:
case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ 0 = 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b

Tactic:
simpa using

Goal state after:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : ¬Prime a
⊢ a ∣ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b

Tactic:
simpa using

Goal state after:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : ¬Prime b
⊢ a ∣ b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b

Tactic:
simpa using

Goal state after:
case inr
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
hb0 : b ≠ 0
pa : Prime a
pb : Prime b
hab : ¬a = b
⊢ b * a ∣ b
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : x ^ (m + k) = x ^ m
hk : x ^ k = 1
⊢ orderOf x ∣ k
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1})) =
    ↑(∑ i ∈ Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))

Tactic:
rw [sum_add_distrib, sum_boole]

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

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ m + k ≡ m + 0 [MOD orderOf x]

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
h : m + k ≡ m [MOD orderOf x]
⊢ orderOf x ∣ k
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
simpa using

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

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

Tactic:
by
    rw [← this, factorization_prod_pow_eq_self_of_le_factorization inf_le_left]

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
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
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
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
a : ↥(zpowers x)
⊢ x ^ ↑((finEquivZPowers hx).symm a) = ↑a

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
hx : IsOfFinOrder x
a : ↥(zpowers x)
⊢ x ^ ↑((finEquivZPowers hx).symm a) = ↑a
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:
· simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]

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}
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
val✝ : Fintype G
⊢ orderOf x ≤ Nat.card G

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
x : G
inst✝ : Finite G
val✝ : Fintype G
⊢ orderOf x ≤ card G
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:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ x ^ n = 1
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
  rw [mul_comm]
  exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb

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:
simpa using

Goal state after:
G : Type u_6
inst✝ : Group G
s : Subgroup G
x : G
hx : x ∈ s
⊢ orderOf x ∣ Nat.card ↥s
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:
simpa using

Goal state after:
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
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:
exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

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

Goal state before:
pp: case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), g + d ≠ g'

Tactic:
simpa using

Goal state after:
case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), ¬g' = g + d
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
simpa using

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n = ∏ x ∈ n.primeFactors, x ^ n.factorization x
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr.h
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
⊢ ∀ (d : G), d + g ≠ g'

Tactic:
simpa using

Goal state after:
case inr.h
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
⊢ ∀ (d : G), ¬g' = g + d
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:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
⊢ of' k G g %ᵒᶠ g = 0
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr.h
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), g + d ≠ g'

Tactic:
simpa using

Goal state after:
case inr.h
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), ¬g' = g + d
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:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.divX = 0
⊢ p = C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case φ_k
R : Type u
inst✝ : Semiring R
p f : R[X]
⊢ f.natDegree < 1 → divX_hom f = 0

Tactic:
simpa using

Goal state after:
case φ_k
R : Type u
inst✝ : Semiring R
p f : R[X]
⊢ f.natDegree = 0 → f = C (f.coeff 0)
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:
simpa using

Goal state after:
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
⊢ ¬p.coeff 0 = 0