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

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) l1 l2)

Tactic:
by

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) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    ↑hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
rw [sum_range_succ, 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: b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ 0 < b + 2

Tactic:
by

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

Goal state before:
pp: b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2

Tactic:
by

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

Goal state before:
pp: b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
⊢ d < b

Tactic:
by

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

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ b + 2 ≤ b + 2

Tactic:
by

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

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ 0 ≤ b + 2

Tactic:
by

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

Goal state before:
pp: b hd : ℕ
tl : List ℕ
IH : (∀ x ∈ tl, x < b + 2) → ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
this✝ : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
this : hd < b + 2
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)

Tactic:
by

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

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

Goal state before:
pp: b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
⊢ ofDigits b l < b ^ l.length

Tactic:
by

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

Goal state before:
pp: b m : ℕ
⊢ m < (b + 2) ^ ((b + 2).digits m).length

Tactic:
by

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
⊢ m < b ^ (b.digits m).length

Tactic:
by

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ 0 < b * m

Tactic:
by

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ 0 < ?m.22

Tactic:
by

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b * m) = 0 :: b.digits m

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ 0 < b ^ k * m

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b m n : ℕ
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

Tactic:
by

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

Goal state before:
pp: p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L

Tactic:
by

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

Goal state before:
pp: p n : ℕ
⊢ (p.digits n).sum ≤ n

Tactic:
by

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

Goal state before:
pp: p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p = ofDigits p digits.tail

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n / p ^ i = ofDigits p (List.drop i (p.digits n))

Tactic:
by

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

Goal state before:
pp: p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ FiniteMultiplicity a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ multiplicity a b = n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑(multiplicity a b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑n ↔ multiplicity a b = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = ↑n ↔ multiplicity a b = n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
L : List ℕ
⊢ k ∣ ofDigits a L - ofDigits b L

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ ↑(multiplicity a b) ≤ emultiplicity a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ multiplicity a b = multiplicity c d

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b ≤ ↑n
⊢ multiplicity a b ≤ n

Tactic:
by

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

Goal state before:
pp: case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k

Tactic:
conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]

Goal state after:
case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ emultiplicity a b ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n ≤ multiplicity a b
⊢ ↑n ≤ emultiplicity a b

Tactic:
by

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

Goal state before:
pp: b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ emultiplicity a b
⊢ n ≤ multiplicity a b

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b l % b = l.head! % b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b < ↑n
⊢ multiplicity a b < n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ emultiplicity a b < ↑n

Tactic:
by

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

Goal state before:
pp: p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ i = ofDigits p (List.take i digits)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n < multiplicity a b
⊢ ↑n < emultiplicity a b

Tactic:
by

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

Goal state before:
pp: p i n : ℕ
h : 2 ≤ p
⊢ n % p ^ i = ofDigits p (List.take i (p.digits n))

Tactic:
by

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

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

Tactic:
· 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:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < emultiplicity a b
⊢ n < multiplicity a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ 0 < emultiplicity a b ↔ 0 < multiplicity a b

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
⊢ emultiplicity ↑a ↑b = emultiplicity a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ a ^ zero ∣ b

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

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

Goal state before:
pp: b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : emultiplicity a b < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
by

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

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ¬a ^ m ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ emultiplicity a b = ↑k

Tactic:
by

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

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ (b'.digits n).sum [MOD b]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
k : ℕ
⊢ a ^ k ∣ b ↔ k ≤ multiplicity a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ ¬a ^ k ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hf : FiniteMultiplicity a b
⊢ multiplicity a b < k ↔ ¬a ^ k ∣ b

Tactic:
by

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

Goal state before:
pp: b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

Tactic:
by

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

Goal state before:
pp: n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e.succ → n / b < b ^ e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ emultiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
n : ℕ
⊢ multiplicity a b = n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a : α
ha : FiniteMultiplicity a 1
⊢ multiplicity a 1 = 0

Tactic:
by

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

Goal state before:
pp: b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ↑n ≡ ofDigits c (b'.digits n) [ZMOD ↑b]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: R : Type u_3
inst✝¹ : CommMonoidWithZero R
inst✝ : Subsingleton Rˣ
a b : R
ha : Irreducible a
hb : Irreducible b
h : a ≠ b
x✝ : Associated a b
u : Rˣ
h✝ : a * ↑u = b
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
⊢ multiplicity a b ≠ 0 ↔ a ∣ b

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
by

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

Goal state before:
pp: b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ n < b * b ^ (e + 1)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : DivisionMonoid G
x : G
⊢ IsOfFinOrder x ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ofDigits (-1) [n] = (List.map (fun n ↦ ↑n) [n]).alternatingSum

Tactic:
by

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

Goal state before:
pp: a b : ℕ
t : List ℕ
⊢ ofDigits (-1) (a :: b :: t) = (List.map (fun n ↦ ↑n) (a :: b :: t)).alternatingSum

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
⊢ ¬IsOfFinOrder x

Tactic:
by

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

Goal state before:
pp: b f n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore f n []).length ≤ e

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n m : ℕ
hm : 0 < m
ha : a ^ m = 1
⊢ (a ^ n) ^ m = 1

Tactic:
by

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

Goal state before:
pp: n i b : ℕ
h : 2 ≤ b
⊢ (b.digits n).getD i 0 = n / b ^ i % b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder a → IsOfFinOrder (a ^ n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digitsAppend l n).length = l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
m : ℕ
hm : 0 < m
ha : (a ^ n) ^ m = 1
⊢ a ^ (n * m) = 1

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p n) = emultiplicity p n

Tactic:
by

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

Goal state before:
pp: p n : ℕ
⊢ (emultiplicity p n).toNat = padicValNat p n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : IsOfFinOrder (a ^ n)
hn : n ≠ 0
⊢ IsOfFinOrder a

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
⊢ emultiplicity a b ≤ emultiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by

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

Goal state before:
pp: a b n : ℕ
ha : Nat.Prime a
hb : b ≠ 0
⊢ n ≤ padicValNat a b ↔ replicate n a <+~ b.primeFactorsList

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digitsAppend l n
⊢ i < b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Monoid α
inst✝ : Monoid β
a b : α
c d : β
hab : FiniteMultiplicity a b
hcd : FiniteMultiplicity c d
⊢ multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a b : α
n : ℕ
⊢ a ^ n ∣ b → f a ^ n ∣ f b

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
x✝³ : List ℕ
x✝² : x✝³ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
x✝¹ : List ℕ
x✝ : x✝¹ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
h : ofDigits b x✝³ = ofDigits b x✝¹
⊢ x✝³.length = x✝¹.length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : Monoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a b : α
⊢ emultiplicity (f a) (f b) = emultiplicity a b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdvd : a ∣ b
⊢ multiplicity a b ≠ 0

Tactic:
by

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

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
x✝³ : List ℕ
x✝² : x✝³ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
x✝¹ : List ℕ
x✝ : x✝¹ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
h : ofDigits b x✝³ = ofDigits b x✝¹
⊢ ∀ l ∈ x✝³, l < b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
⊢ ¬IsOfFinOrder a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
inst✝ : IsMulTorsionFree G
a : G
ha : IsOfFinOrder a
⊢ a = 1

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
x✝³ : List ℕ
x✝² : x✝³ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
x✝¹ : List ℕ
x✝ : x✝¹ ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
h : ofDigits b x✝³ = ofDigits b x✝¹
⊢ ∀ l ∈ x✝¹, l < b

Tactic:
by

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

Goal state before:
pp: a b m n✝ p n : ℕ
⊢ ∀ (a : ℕ), a ∈ n.primeFactors ↔ (if Prime a then padicValNat a n else 0) ≠ 0

Tactic:
by

Goal state after: