mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
·

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

pp: case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Tactic:
·

Goal state after:
case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)

Tactic:
·

Goal state after:
case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ b.digitsAux h (n✝ + 1) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n

pp: case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Tactic:
·

Goal state after:
case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : m = 0
⊢ val 0 ^ m < n

pp: case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n

Tactic:
·

Goal state after:
case pos
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : m = 0
⊢ val 0 ^ m < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n

Tactic:
·

Goal state after:
case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
hxy : x ≠ 0 ∨ 0 ≠ 0
⊢ (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0

pp: case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (b + 2).digits (x + (b + 2) * (n✝ + 1)) = x :: (b + 2).digits (n✝ + 1)

Tactic:
·

Goal state after:
case zero
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
hxy : x ≠ 0 ∨ 0 ≠ 0
⊢ (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Tactic:
·

Goal state after:
case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)

pp: case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)

Tactic:
·

Goal state after:
case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.e_head
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) = x

pp: case succ.e_tail.e_a
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) / (b + 2) = n✝ + 1

Tactic:
·

Goal state after:
case succ.e_head
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) = x
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.e_tail.e_a
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) / (b + 2) = n✝ + 1

Tactic:
·

Goal state after:
case succ.e_tail.e_a
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) / (b + 2) = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)

Tactic:
·

Goal state after:
case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ m < n
⊢ (a ^ m).val = a.val ^ m

Tactic:
by
  induction m with
  | zero => simp [ZMod.val_one]
  | succ m ih =>
    have : a.val ^ m < n := by
      obtain rfl | ha := eq_or_ne a 0
      · by_cases hm : m = 0
        · cases hm; simp [ilt.out]
        · simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]
      · exact lt_of_le_of_lt
         (Nat.pow_le_pow_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h
    rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

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

Goal state before:
pp: case inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs

pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Tactic:
·

Goal state after:
case inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k

pp: case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝ : NonAssocRing R
f : R →+* ZMod 0
k : ZMod 0
⊢ f k.cast = k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k

Tactic:
·

Goal state after:
case succ
R : Type u_1
inst✝ : NonAssocRing R
n✝ : ℕ
f : R →+* ZMod (n✝ + 1)
k : ZMod (n✝ + 1)
⊢ f k.cast = k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 → AddSubgroup.zmultiples ↑n ≤ f.ker

pp: case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ f.ker → f ↑n = 0

Tactic:
·

Goal state after:
case mp
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ f ↑n = 0 → AddSubgroup.zmultiples ↑n ≤ f.ker
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ f.ker → f ↑n = 0

Tactic:
·

Goal state after:
case mpr
n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
f : ℤ →+ A
⊢ AddSubgroup.zmultiples ↑n ≤ f.ker → f ↑n = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_1
m k n : ℕ
x✝ : ∃ y, n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ ↑n = ↑k

pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y

Tactic:
·

Goal state after:
case refine_1
m k n : ℕ
x✝ : ∃ y, n = k + m * y
a : ℕ
ha : n = k + m * a
⊢ ↑n = ↑k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y

Tactic:
·

Goal state after:
case refine_2
m k n : ℕ
x✝ : ↑n = ↑k ∧ k ≤ n
H₁ : ↑n = ↑k
H₂ : k ≤ n
⊢ ∃ y, n = k + m * y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case fst
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).1 = p.1

pp: case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2

Tactic:
·

Goal state after:
case fst
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).1 = p.1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2

Tactic:
·

Goal state after:
case snd
N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ ((fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p)).2 = p.2
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddCommMonoid M
⊢ Subsingleton (Module (ZMod 0) M)

pp: case succ
M : Type u_1
inst✝ : AddCommMonoid M
n : ℕ
⊢ Subsingleton (Module (ZMod (n + 1)) M)

Tactic:
·

Goal state after:
case zero
M : Type u_1
inst✝ : AddCommMonoid M
⊢ Subsingleton (Module (ZMod 0) M)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d :: b.digits (ofDigits b L) = d :: L

pp: case cons.hxb
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d < b

pp: case cons.hxy
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
·

Goal state after:
case cons
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d :: b.digits (ofDigits b L) = d :: L
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.w₁
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ l ∈ L, l < b

pp: case cons.w₂
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ (h : L ≠ []), L.getLast h ≠ 0

Tactic:
·

Goal state after:
case cons.w₁
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ l ∈ L, l < b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.w₂
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ (h : L ≠ []), L.getLast h ≠ 0

Tactic:
·

Goal state after:
case cons.w₂
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ (h : L ≠ []), L.getLast h ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.hxb
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d < b

pp: case cons.hxy
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
·

Goal state after:
case cons.hxb
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d < b
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.hxy
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
·

Goal state after:
case cons.hxy
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case pos
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

pp: case neg
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
·

Goal state after:
case pos
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case neg
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
·

Goal state after:
case neg
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
Module: Mathlib.Data.Nat.Digits.Defs

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

pp: case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n

Tactic:
·

Goal state after:
case zero
n : ℕ
⊢ ofDigits 0 (digits 0 n) = n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero.zero
⊢ ofDigits 0 (digits 0 0) = 0

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

Tactic:
·

Goal state after:
case zero.zero
⊢ ofDigits 0 (digits 0 0) = 0
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
·

Goal state after:
case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
·

Goal state after:
case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n
Module: Mathlib.Data.Nat.Digits.Defs

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

pp: case succ.succ
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
·

Goal state after:
case succ.zero
n : ℕ
⊢ ofDigits (0 + 1) ((0 + 1).digits n) = n
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
·

Goal state after:
case succ.succ
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1

Tactic:
·

Goal state after:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1

Tactic:
·

Goal state after:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case mp
b n : ℕ
⊢ b.digits n = [] → n = 0

pp: case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []

Tactic:
·

Goal state after:
case mp
b n : ℕ
⊢ b.digits n = [] → n = 0
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
·

Goal state after:
case mpr
b n : ℕ
⊢ n = 0 → b.digits n = []
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
· rintro rfl
    simp

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

Goal state before:
pp: case pos
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

pp: case neg
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
·

Goal state after:
case pos
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case case2
n p✝ p : ℕ
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
e q : ℕ
heq : go n (p * p) ⋯ = (e, q)
hqp : ¬q % p = 0
ih : (go n (p * p) ⋯).snd * (p * p) ^ (go n (p * p) ⋯).fst = n ∧ ¬p * p ∣ (go n (p * p) ⋯).snd
⊢ (2 * e, q).snd * p ^ (2 * e, q).fst = n ∧ ¬p ∣ (2 * e, q).snd

Tactic:
| case2 p hp hmod e q heq hqp ih =>

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

Goal state before:
pp: p✝ n : ℕ
hn : n ≠ 0
p : ℕ
⊢ 1 < p + 2

Tactic:
by lia

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

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

pp: case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n

Tactic:
·

Goal state after:
case inl
p : ℕ
⊢ padicValNat p 0 ≤ 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n

Tactic:
·

Goal state after:
case inr
p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n ≤ n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n

pp: case inr
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
·

Goal state after:
case inl
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n

Tactic:
·

Goal state after:
case inr
p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
hp₁ : 1 < p
⊢ p ^ k ∣ n ↔ k ≤ padicValNat p n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inl
n k l : ℕ
hn : n ≠ 0
h : 0 ^ k * l = n
hl : ¬0 ∣ l
⊢ maxPowDvdDiv 0 n = (k, l)

pp: case inr.inl
n k l : ℕ
hn : n ≠ 0
h : 1 ^ k * l = n
hl : ¬1 ∣ l
⊢ maxPowDvdDiv 1 n = (k, l)

pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
·

Goal state after:
case inl
n k l : ℕ
hn : n ≠ 0
h : 0 ^ k * l = n
hl : ¬0 ∣ l
⊢ maxPowDvdDiv 0 n = (k, l)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inl
n k l : ℕ
hn : n ≠ 0
h : 1 ^ k * l = n
hl : ¬1 ∣ l
⊢ maxPowDvdDiv 1 n = (k, l)

pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
·

Goal state after:
case inr.inl
n k l : ℕ
hn : n ≠ 0
h : 1 ^ k * l = n
hl : ¬1 ∣ l
⊢ maxPowDvdDiv 1 n = (k, l)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)

Tactic:
·

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ p.maxPowDvdDiv n = (k, l)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k = (p.maxPowDvdDiv n).fst

Tactic:
·

Goal state after:
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k = (p.maxPowDvdDiv n).fst
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ (p.maxPowDvdDiv n).fst

pp: case h₂
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ k

Tactic:
·

Goal state after:
case h₁
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ k ≤ (p.maxPowDvdDiv n).fst
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h₂
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ k

Tactic:
·

Goal state after:
case h₂
p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
hp : 1 < p
⊢ (p.maxPowDvdDiv n).fst ≤ k
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)

pp: case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst

Tactic:
·

Goal state after:
case inr.inr
p n k l : ℕ
hn : n ≠ 0
h : l = n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ p.maxPowDvdDiv n = (k, l)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst

Tactic:
·

Goal state after:
case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case hn
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n ≠ 0

pp: case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n

pp: case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p

Tactic:
·

Goal state after:
case hn
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ k * n ≠ 0
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case h
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ p ^ (padicValNat p n + k) * n.divMaxPow p = p ^ k * n

pp: case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p

Tactic:
·

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

Goal state before:
pp: case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p

Tactic:
·

Goal state after:
case hl
p n : ℕ
hp : 1 < p
hn : n ≠ 0
k : ℕ
⊢ ¬p ∣ n.divMaxPow p
Module: Mathlib.Data.Nat.MaxPowDiv

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

pp: case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

pp: case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
·

Goal state after:
case pos
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1