mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a b : G
⊢ ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) b → a = b

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a b : G
⊢ ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) b → a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
x✝ : n + 2 ≠ 1
⊢ 1 < n + 2

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ 1 ∈ n.divisors ↔ n ≠ 0

Tactic:
simp

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

Goal state before:
pp: R M : Type u
inst✝¹ : Semiring R
inst✝ : Fintype M
⊢ #R[M] = #R ^ card M

Tactic:
simp

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

Goal state before:
pp: R M : Type u
inst✝² : Semiring R
inst✝¹ : Infinite M
inst✝ : Nontrivial R
⊢ #R[M] = max #R #M

Tactic:
simp

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

Goal state before:
pp: R M : Type u
inst✝² : Semiring R
inst✝¹ : Nonempty M
inst✝ : Infinite R
⊢ #R[M] = max #R #M

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < x ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ List.Pairwise (fun x1 x2 ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ ∀ (a : ℕ × ℕ), ¬a.1 < a.1

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
⊢ n ∈ divisors 0 → n ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝ : ℕ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝ : ℕ
⊢ a✝ ∈ properDivisors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝ : ℕ
⊢ a✝ ∈ divisors 1 ↔ a✝ ∈ {1}

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 0 ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
hx' : 0 ≤ x
⊢ n + 1 + 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℤ
⊢ n % ↑2 = 1 % ↑2 ↔ n % 2 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.inl
⊢ (↑1).val.Coprime 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.inr
⊢ (↑(-1)).val.Coprime 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ map ({ toFun := fun d ↦ (n / d, d), inj' := ⋯ }.trans (Equiv.prodComm ℕ ℕ).toEmbedding) n.divisors ↔
    a✝ ∈ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

Tactic:
rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]

Goal state after:
case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ -1 * -1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : { x // x.val.Coprime n }
val✝ : ZMod n
property✝ : val✝.val.Coprime n
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ unitOfCoprime (↑x).val ⋯) ⟨val✝, property✝⟩) = ⟨val✝, property✝⟩

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
← zero_add (∑ x ∈ s, x),

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 + ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + (0 + ∑ x ∈ s, x)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
h : ∑ x ∈ properDivisors 0, x ∣ 0
⊢ ∑ x ∈ properDivisors 0, x = 1 ∨ ∑ x ∈ properDivisors 0, x = 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ x ∈ n.divisors, f x = f x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ x ∈ Ico (0 + 1) n.succ, a / b ^ x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (0 + 1) n.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m✝ n✝ m n : ℕ
h : m.Coprime n
to_fun : ZMod (m * n) → ZMod m × ZMod n := ⇑(castHom ⋯ (ZMod m × ZMod n))
inv_fun : ZMod m × ZMod n → ZMod (m * n) :=
  fun x ↦
    if m * n = 0 then
      if m = 1 then ((RingHom.snd (ZMod m) (ZMod n)) x).cast else ((RingHom.fst (ZMod m) (ZMod n)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
left_inv : LeftInverse inv_fun to_fun
⊢ Fintype.card (ZMod m × ZMod n) ≤ Fintype.card (ZMod (m * n))

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ 1 ∈ z.divisors ↔ z ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ -1 ∈ z.divisors ↔ z ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: a✝ : ℤ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z a✝ : ℤ
⊢ a✝ ∈ (-z).divisors ↔ a✝ ∈ z.divisors

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.zero
⊢ Subsingleton (ZMod 0) → 0 = 1

pp: case mp.succ.zero
⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
· simpa [ZMod] using not_subsingleton _

Goal state after:
case mp.succ.zero
⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
· simpa [ZMod] using not_subsingleton _

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: xy : ℤ × ℤ
z : ℤ
⊢ -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «0»
⊢ ↑(-(fun i ↦ i) ⟨0, ⋯⟩) = ↑((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «1»
⊢ ↑(-(fun i ↦ i) ⟨1, ⋯⟩) = ↑((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

Goal state after:
case «1»
⊢ ↑(-1) = 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs = ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ZMod 0
⊢ 2 * a = 0 ↔ a = 0 ∨ 2 * a.val = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 ≤ n✝ + 1 + 1

Tactic:
simp

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

Goal state before:
pp: case inl.zero
⊢ choose 0 0 ≤ 2 ^ 0

Tactic:
simp

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

Goal state before:
pp: case inl.succ
n✝ : ℕ
⊢ choose 0 (n✝ + 1) ≤ 2 ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos.refl
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val 0 ≤ a.val
⊢ (a - 0).val = a.val - val 0

Tactic:
simp

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

Goal state before:
pp: n b : ℕ
⊢ 2 ≤ b + 2

Tactic:
simp

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

Goal state before:
pp: n✝ b : ℕ
x✝ : 1 < b + 2
⊢ 2 ≤ b + 2

Tactic:
simp

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ℤ
k : ℤ
⊢ f ↑k = k

Tactic:
simp

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

Goal state before:
pp: b k : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * ofDigits b (List.replicate k 0) = ofDigits b l

Tactic:
simp

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

Goal state before:
pp: b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b l.reverse + b ^ l.reverse.length * ofDigits b [d] = ofDigits b l.reverse + b ^ l.length * d

Tactic:
simp

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

Goal state before:
pp: case nil
b : ℕ
h : 1 < b
w₁ : ∀ l ∈ [], l < b
w₂ : ∀ (h : [] ≠ []), [].getLast h ≠ 0
⊢ b.digits (ofDigits b []) = []

Tactic:
simp

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

Goal state before:
pp: b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ d :: L ≠ []

Tactic:
simp

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

Goal state before:
pp: case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1

Tactic:
simp

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

Goal state before:
pp: case mpr
b : ℕ
⊢ b.digits 0 = []

Tactic:
simp

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

Goal state before:
pp: case case2
p n : ℕ
h : ¬(1 < p ∧ n ≠ 0)
⊢ (0, n).snd * p ^ (0, n).fst = n

Tactic:
simp

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

Goal state before:
pp: p n : ℕ
⊢ n = p ^ padicValNat p n * n.divMaxPow p

Tactic:
simp

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

Goal state before:
pp: case inl
p : ℕ
⊢ padicValNat p 0 ≤ 0

Tactic:
simp

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

Goal state before:
pp: case inl
n k : ℕ
hp : 1 ≠ 0
⊢ (1 ^ k * n).divMaxPow 1 = n.divMaxPow 1

Tactic:
simp

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

Goal state before:
pp: case nil
b : ℕ
⊢ List.foldr (fun x y ↦ ↑x + b * y) 0 [] =
    (List.zipWith
        (Function.curry fun x ↦
          match x with
          | (a, i) => a * b ^ i)
        [] (List.range [].length)).sum

Tactic:
simp

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

Goal state before:
pp: case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0

Tactic:
simp

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

Goal state before:
pp: case succ.zero
m : ℕ
hm : m ≠ 0
⊢ ((0 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
simp

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

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0

Tactic:
rcases b with (_ | _ | b)
  · cases m
    · cases hm rfl
    · simp
  · simp
  revert hm
  induction m using Nat.strongRecOn with | ind n IH => ?_
  intro hn
  by_cases! hnb : n < b + 2
  · simpa only [digits_of_lt (b + 2) n hn hnb]
  · rw [digits_getLast n (le_add_left 2 b)]
    refine IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) ?_
    rw [← pos_iff_ne_zero]
    exact Nat.div_pos hnb (zero_lt_succ (succ b))

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

Goal state before:
pp: case inl
m n : ℕ
hb : 0 < succ 0
⊢ (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)

Tactic:
simp

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

Goal state before:
pp: case inl
b : ℕ
⊢ (b.digits 0).length ≤ (b.digits (0 + 1)).length

Tactic:
simp

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

Goal state before:
pp: case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ i ∈ range (hd :: tl).length, ofDigits p (hd :: tl) / p ^ i.succ = ofDigits p (hd :: tl) - (hd :: tl).sum

Tactic:
simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]

Goal state after:
case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    ofDigits p (hd :: tl) - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) *
      (∑ x ∈ range tl.length, ofDigits p (List.drop x.succ (hd :: tl)) +
        ofDigits p (List.drop tl.length.succ (hd :: tl))) =
    ↑hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
Nat.cast_id

Goal state after:
case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) *
      (∑ x ∈ range tl.length, ofDigits p (List.drop x.succ (hd :: tl)) +
        ofDigits p (List.drop tl.length.succ (hd :: tl))) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
hb : 1 < b
m : ℕ
hm : 0 < m
⊢ b.digits (b ^ 0 * m) = List.replicate 0 0 ++ b.digits m

Tactic:
simp

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

Goal state before:
pp: case zero
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ 0 = ofDigits p (List.drop 0 digits)

Tactic:
simp

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

Goal state before:
pp: case succ.nil
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
w₁ : ∀ l ∈ [], l < p
⊢ ofDigits p [] % p ^ (i + 1) = ofDigits p (List.take (i + 1) [])

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inr.inr.zero
p : ℕ
h : p < 1
⊢ 0 = 0 - (digits 0 0).sum

Tactic:
simp

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

Goal state before:
pp: case inr.inr.succ
p : ℕ
h : p < 1
n✝ : ℕ
⊢ 0 = n✝ + 1 - (digits 0 (n✝ + 1)).sum

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ digits 2 0 = List.map (fun b ↦ bif b then 1 else 0) (bits 0)

Tactic:
simp

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

Goal state before:
pp: case one
⊢ digits 2 1 = List.map (fun b ↦ bif b then 1 else 0) (bits 1)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ 0 - 0

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
a b : α
hk : ↑0 ≤ emultiplicity a b
⊢ a ^ 0 ∣ b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ n < n + 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
b : α
⊢ ¬FiniteMultiplicity 1 b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ multiplicity a b = multiplicity a b

Tactic:
simp

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

Goal state before:
pp: case pos
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : n / b = 0
⊢ [(n % b).digitChar].length ≤ e + 1 + 1

Tactic:
simp

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

Goal state before:
pp: case zero
b i : ℕ
⊢ ((b + 2).digits 0)[i]?.getD 0 = 0 / (b + 2) ^ i % (b + 2)

Tactic:
simp

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

Goal state before:
pp: case ind.zero
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
⊢ n.succ % (b + 2) = n.succ / (b + 2) ^ default % (b + 2)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case isFalse
α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
w : ℕ
h_1 : ¬a ^ (w + 1) ∣ b
h✝ : ¬FiniteMultiplicity c d
⊢ ↑(Nat.find ⋯) ≤ ⊤

Tactic:
next h_2 => simp_all only [not_exists, Decidable.not_not, le_top]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ padicValNat p n ∧ ¬padicValNat p n + 1 ≤ padicValNat p n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inl
n : ℕ
⊢ (emultiplicity 1 n).toNat = padicValNat 1 n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inr.inl
p : ℕ
hp : p ≠ 1
⊢ (emultiplicity p 0).toNat = padicValNat p 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: case inl
p : ℕ
⊢ padicValNat p 0 = 0 ↔ p = 1 ∨ 0 = 0 ∨ ¬p ∣ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

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

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Monoid G
a : G
⊢ IsOfFinOrder (a ^ 0) ↔ IsOfFinOrder a ∨ 0 = 0

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a b : α
⊢ ∀ (n : ℕ), a ^ n ∣ -b ↔ a ^ n ∣ b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
simp

Goal state after:
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
⊢ multiplicity p b < multiplicity p b + 1

Tactic:
simp

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l x✝ : ℕ
⊢ x✝ ∈ ↑(Finset.range (b ^ l)) ↔ x✝ ∈ {n | n < b ^ l}

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
⊢ (n ^ 0).factorization = 0 • n.factorization

Tactic:
simp

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

Goal state before:
pp: case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
⊢ ψ x ^ orderOf x = 1

Tactic:
rw [← map_pow, pow_orderOf_eq_one]

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.Factorization.Defs

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

Tactic:
simp

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:
simp

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

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

Tactic:
by
  if pp : p.Prime then
    exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
  else
    simpa [Nat.factorization_eq_zero_of_not_prime n pp] using hn.bot_lt

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
x : G
H : Type u_6
inst✝ : Monoid H
y : H
⊢ orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

Tactic:
simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]

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

Goal state before:
pp: p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ 0!.factorization p = ∑ i ∈ Ico 1 b, 0 / p ^ i

Tactic:
simp

Goal state after: