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

Goal state before:
pp: case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ []
⊢ d < b + 2

Tactic:
]

Goal state after:
case ind.zero
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ []
⊢ d < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
⊢ d < b + 2

Tactic:
]

Goal state after:
case ind.succ
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
⊢ d < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
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
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)

Tactic:
]

Goal state after:
case cons
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
⊢ ↑hd + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
]

Goal state after:
case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: b m : ℕ
⊢ m = m

Tactic:
]

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

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

Tactic:
]

Goal state after:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b * m % b :: b.digits (b * m / b) = 0 :: b.digits m
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
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 :: (List.replicate k 0 ++ b.digits m) = 0 :: (List.replicate k 0 ++ b.digits m)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ n + 1 ≤ n + 1

Tactic:
]

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

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
]

Goal state after:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
]

Goal state after:
case succ.succ
n p : ℕ
a✝¹ : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
a✝ : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih✝ : (∀ l ∈ tl, l < p) → ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p tl = ofDigits p tl

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
]

Goal state after:
case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
]

Goal state after:
case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = 0
h₁ : 1 ≤ tl.length
⊢ p * ofDigits p tl - tl.sum = p * ofDigits p tl - tl.sum

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ↑n = ⊤
⊢ False
Module: Mathlib.Data.Nat.Digits.Defs

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

pp: case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd + p * (ofDigits p tl % p ^ i) < p * p ^ i

Tactic:
]

Goal state after:
case succ.cons
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd + p * (ofDigits p tl % p ^ i) < p * p ^ i
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
]

Goal state after:
case bit
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun b ↦ bif b then 1 else 0) (b :: n.bits)
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
]

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
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b ↦ bif b then 1 else 0) (false :: n.bits)

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 ⊤ = 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ WithTop.untopD 1 ⊤ = 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * (p ^ i - ofDigits p tl % p ^ i)

Tactic:
]

Goal state after:
case succ.cons.hbc
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ), (∀ l ∈ digits, l < p) → ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * (p ^ i - ofDigits p tl % p ^ i)
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
⊢ WithTop.untopD 1 (emultiplicity c d) = WithTop.untopD 1 (emultiplicity c d)

Tactic:
]

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
⊢ ↑(multiplicity a b) ≤ ↑n

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ ↑(multiplicity a b) ≤ ↑n
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ ↑(multiplicity a b)
⊢ n ≤ multiplicity a b
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
⊢ ↑(multiplicity a b) < ↑n

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ ↑(multiplicity a b) < ↑n
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
by_cases hb : 1 < b

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

case neg
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b
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! = ofDigits b (b.digits (n + 1)) % b

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n < ↑(multiplicity a b)
⊢ n < multiplicity a b
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! = (b.digits (n + 1)).head! % b

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
n : ℕ
⊢ 1 ∣ b
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
]

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]
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
⊢ ↑(multiplicity a b) < ↑m

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ↑(multiplicity a b) < ↑m
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
]

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 ↔ multiplicity a b < k

Tactic:
]

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

Goal state after:
case mp.right
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
]

Goal state after:
b b' : ℕ
c : ℤ
h : ↑b' ≡ c [ZMOD ↑b]
n : ℕ
⊢ ofDigits (↑b') (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD ↑b]
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:
]

Goal state after:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b
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
⊢ False

Tactic:
]

Goal state after:
α : 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
⊢ False
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
]

Goal state after:
case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1
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 ^ (e + 1 + 1)

Tactic:
]

Goal state after:
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 ^ (e + 1 + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
n : ℕ
x : G
⊢ x ^ n = 1 ↔ x ^ n = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
]

Goal state after:
G : Type u_6
inst✝ : DivisionMonoid G
x : G
⊢ (∃ n, 0 < n ∧ x ^ n = 1) ↔ ∃ n, n ≠ 0 ∧ x ^ n = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n.natAbs = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
]

Goal state after:
case inl
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n.natAbs = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n.natAbs = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
]

Goal state after:
case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n.natAbs = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < n
hnx : x ^ n = x ^ 0
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
]

Goal state after:
n i b : ℕ
⊢ ((b + 2).digits n)[i]?.getD 0 = n / (b + 2) ^ i % (b + 2)
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:
]

Goal state after:
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)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : Injective fun n ↦ x ^ n
n : ℕ
hn_pos : 0 < 0
hnx : x ^ n = x ^ 0
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
hn : n ≠ 0
⊢ ∃ n, 0 < n ∧ a ^ n = 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
h : ∃ n_1, 0 < n_1 ∧ (a ^ n) ^ n_1 = 1
hn : n ≠ 0
⊢ ∃ n, 0 < n ∧ a ^ n = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ l = l

pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length ≤ l

Tactic:
]

Goal state after:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ (b.digits n).length ≤ l
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ n < b ^ l

Tactic:
]

Goal state after:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
⊢ n < b ^ l
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:
]

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

Goal state after:
p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ padicValNat p n ∧ ¬padicValNat p n + 1 ≤ padicValNat p n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
⊢ i < b

Tactic:
]

Goal state after:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
⊢ i < b
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

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

Tactic:
]

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:
rcases Decidable.eq_or_ne n 0 with rfl | hn
  · simp
  · exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

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
⊢ (∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d) ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d

Tactic:
]

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, 0 < n ∧ a ^ n = 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Monoid G
a : G
inst✝ : IsMulTorsionFree G
ha : a ≠ 1
⊢ ¬∃ n, 0 < n ∧ a ^ n = 1
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
]

Goal state after: