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

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n).choose n * (2 * n + 1))

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n

Tactic:
by

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

Goal state before:
pp: m : ℕ
inst✝¹ : NeZero m
n : ℕ
inst✝ : NeZero n
a : ZMod m
⊢ a.cast.val < m

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = (-a).val % n

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val + a.val ≡ n - a.val + a.val [MOD n]

Tactic:
by

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) = 4 * 4 ^ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * 4 ^ n < 4 * (n * n.centralBinom)

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ (-a).val = if a = 0 then 0 else n - a.val

Tactic:
by

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

Goal state before:
pp: n : ℕ
nz : NeZero n
a : ZMod n
na : NeZero a
⊢ (-a).val = n - a.val

Tactic:
by

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
by

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

Goal state before:
pp: n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom

Tactic:
by

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

Goal state before:
pp: x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1

Tactic:
by

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

Goal state before:
pp: x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2

Tactic:
by

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

Goal state before:
pp: x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3

Tactic:
by

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

Goal state before:
pp: n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * (n + 4) * (n + 4).centralBinom

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ 2 ∣ (n + 1).centralBinom

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 0 < n
⊢ 2 ∣ n.centralBinom

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (n + 1).Coprime (2 * n + 1)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < n
⊢ ?m.35 ≠ 0

Tactic:
by

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

Goal state before:
pp: m n : ℕ
nzm : NeZero m
a : ZMod m
h : a.val < n
⊢ a.cast.val = a.val

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n + 1 ∣ n.centralBinom

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast.cast = a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
h : 1 < 0
⊢ ¬1 < 0

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
h : 1 < 1
⊢ ¬1 < 1

Tactic:
by

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

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

Tactic:
by

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

Tactic:
cases hm; simp [ilt.out]

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

Goal state before:
pp: b x : ℕ
hx : x ≠ 0
hxb : x < b
⊢ b.digits x = [x]

Tactic:
by

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

Goal state before:
pp: 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 > 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ a.val ^ m < n

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: m n : ℕ
inst✝ : Fact (1 < n)
a : ZMod n
⊢ (a ^ m).val ≤ a.val ^ m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun x y ↦ ↑x + b * y) 0 L

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ ofDigits b [n] = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
h : ℕ
L : List ℕ
⊢ ofDigits 1 (h :: L) = ↑h + ofDigits 1 L

Tactic:
by

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

Goal state before:
pp: n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
by

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

Goal state before:
pp: b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
⊢ f = g

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
f g : ZMod n ≃+* R
⊢ f = g

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b (l ++ [0]) = ofDigits b l

Tactic:
by

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

Goal state before:
pp: b k : ℕ
⊢ ofDigits b (List.replicate k 0) = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
· dsimp [ZMod.cast]
    rw [map_natCast, natCast_zmod_val]

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
R : Type u_1
A : Type u_2
inst✝ : AddGroup A
⊢ ∀ (x : ℤ →+ A), x ↑n = 0 ↔ (Int.castAddHom (ZMod n)).ker ≤ x.ker

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
A : Type u_2
inst✝ : AddGroup A
f : { f // f ↑n = 0 }
⊢ Injective ⇑((lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ ofDigits b (0 :: l).reverse = ofDigits b l.reverse

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Type u_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : SetLike S G
inst✝¹ : AddSubgroupClass S G
K : S
inst✝ : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (a : ZMod n), a • x ∈ K

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod n) G
x : G
⊢ n • x = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Nontrivial G
inst✝ : Module (ZMod 1) G
x : G
hx : x ≠ 0
⊢ x = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : Nontrivial G
⊢ n ≠ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : Module (ZMod n) G
inst✝¹ : NeZero n
inst✝ : Nontrivial G
⊢ 2 ≤ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
G : Type u_2
inst✝² : AddCommGroup G
inst✝¹ : Module (ZMod n) G
inst✝ : NeZero n
x y : G
⊢ IsPeriodicPt (fun x_1 ↦ x + x_1) n y

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ x + x = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x : G
⊢ -x = x

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y : G
⊢ x - y = x + y

Tactic:
by

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

Goal state before:
pp: G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y z : G
⊢ x + y + (y + z) = x + z

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ (↑n)⁻¹.val) ^ n = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
n : ℕ
hn : (Nat.card α).gcd n = 1
a : α
⊢ (a ^ n) ^ (↑n)⁻¹.val = a

Tactic:
by

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

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

Goal state before:
pp: m k : ℕ
⊢ (Set.range fun n ↦ m * n + k) = {n | ↑n = ↑k ∧ k ≤ n}

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : AddCommMonoid M
⊢ Subsingleton (Module (ZMod n) M)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p✝ n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ 1 < p * p ∧ n ≠ 0

Tactic:
by

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

Goal state before:
pp: n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : p ∣ n
⊢ n / (p * p) < n / p

Tactic:
rcases hmod with ⟨m, rfl⟩

Goal state after:
p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
⊢ p * m / (p * p) < p * m / p
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p m : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ p * m ≠ 0
hp₀ : 0 < p
⊢ 0 < m

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ ofDigits b (b.digits n) = n

Tactic:
by

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

Goal state before:
pp: L : List ℕ
⊢ ofDigits 1 L = L.sum

Tactic:
by

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

Goal state before:
pp: b n : ℕ
h : b.digits n = []
⊢ ofDigits b (b.digits n) = ofDigits b []

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ b.digits n = [] ↔ n = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hnp : 1 < p ∧ n ≠ 0
⊢ (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ padicValNat 0 n = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.divMaxPow 0 = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ padicValNat 1 n = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.divMaxPow 1 = n

Tactic:
by

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

Goal state before:
pp: n b : ℕ
l : List ℕ
⊢ n * ofDigits b l = ofDigits b (List.map (fun x ↦ n * x) l)

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ p.maxPowDvdDiv 0 = (0, 0)

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ padicValNat p 0 = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ divMaxPow 0 p = 0

Tactic:
by

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

Goal state before:
pp: p n : ℕ
h : ¬p ∣ n
⊢ p.maxPowDvdDiv n = (0, n)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ padicValNat p 1 = 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
⊢ divMaxPow 1 p = 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ padicValNat p n < n

Tactic:
by

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

Goal state before:
pp: p n : ℕ
⊢ padicValNat p n ≤ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p k n a b : ℕ
hp : 1 < p
hn : n ≠ 0
hab : p ^ a * b = n
hb : ¬p ∣ b
⊢ p ^ k ∣ n ↔ k ≤ a

Tactic:
by

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

Goal state before:
pp: p k n : ℕ
hp : p ≠ 1
hn : n ≠ 0
⊢ p = 0 ∨ 1 < p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p n k l : ℕ
hn : n ≠ 0
h : p ^ k * l = n
hl : ¬p ∣ l
⊢ p = 0 ∨ p = 1 ∨ 1 < p

Tactic:
by

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : p ≠ 0
n k : ℕ
⊢ p = 1 ∨ 1 < p

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
this :
  List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length) =
    List.zipWith (fun a i ↦ b * (a * b ^ i)) l (List.range l.length)
⊢ (List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i ↦ a * b ^ i) l (List.range l.length)).sum

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
⊢ (List.zipWith (fun a i ↦ a * b ^ (i + 1)) l (List.range l.length)).sum =
    b * (List.zipWith (fun a i ↦ a * b ^ i) l (List.range l.length)).sum

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : ℕ
L : List ℕ
⊢ ofDigits b L = (List.mapIdx (fun i a ↦ a * b ^ i) L).sum

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ 0 < b ^ k

Tactic:
by

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

Goal state before:
pp: b k : ℕ
hb : 1 < b
n : ℕ
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
by

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

Goal state before:
pp: b k : ℕ
hb : 1 < b
n : ℕ
⊢ k < (b.digits n).length ↔ b ^ k ≤ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : ℕ
hb : 1 < b
L1 L2 : List ℕ
len : L1.length = L2.length
w1 : ∀ l ∈ L1, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b L1 = ofDigits b L2
⊢ L1 = L2

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ 0 < l.getLast hl

Tactic:
rwa [pos_iff_ne_zero]

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ 0 < l.getLast hl

Tactic:
by

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

Goal state before:
pp: b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Tactic:
by

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

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Tactic:
by

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

Goal state before:
pp: b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Tactic:
by

Goal state after: