mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

pp: case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0

Tactic:
;

Goal state after:
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0

case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
Module: Mathlib.Algebra.Algebra.ZMod

Goal state before:
pp: R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z

Tactic:
;

Goal state after:
R✝ : Type u_1
inst✝⁴ : Ring R✝
n : ℕ
R : Type u_2
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module (ZMod n) R
inst✝ : Module R M
this : Algebra (ZMod n) R := algebraOfModule n R
m₂ : Module (ZMod n) M := Module.compHom M (algebraMap (ZMod n) R)
x : ZMod n
y : R
z : M
⊢ (algebraMap (ZMod n) R) x • y • z = x • y • z
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ n ≠ 0

Tactic:
;

Goal state after:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
⊢ n ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a b : ZMod 0
h : a.val + b.val < 0
⊢ False

Tactic:
;

Goal state after:
a b : ZMod 0
h : a.val + b.val < 0
⊢ False
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih

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

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n

Tactic:
;

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
⊢ Nontrivial
    (match 0 with
    | 0 => ℤ
    | n.succ => Fin (n + 1))

Tactic:
;

Goal state after:
m n : ℕ
⊢ Nontrivial
    (match 0 with
    | 0 => ℤ
    | n.succ => Fin (n + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
⊢ ↑↑(a.val.gcd n.succ) = ↑(a.val.gcd n.succ)

Tactic:
;

Goal state after:
n : ℕ
a : ZMod (n + 1)
⊢ ↑↑(a.val.gcd n.succ) = ↑(a.val.gcd n.succ)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
m : ℕ
hmn : m.Coprime 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
simp [m.coprime_zero_right.1 hmn]

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

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)

Tactic:
;

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
this : ↑(u * u⁻¹) = 1
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑(u * u⁻¹)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
x : ZMod (0 * 1)
⊢ inv_fun (to_fun x) = x

Tactic:
;

Goal state after:
case inl.left
m n : ℕ
h : Nat.Coprime 0 1
to_fun : ZMod (0 * 1) → ZMod 0 × ZMod 1 := ⇑(castHom ⋯ (ZMod 0 × ZMod 1))
inv_fun : ZMod 0 × ZMod 1 → ZMod (0 * 1) :=
  fun x ↦
    if 0 * 1 = 0 then
      if 0 = 1 then ((RingHom.snd (ZMod 0) (ZMod 1)) x).cast else ((RingHom.fst (ZMod 0) (ZMod 1)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 0 * 1 = 0
x : ZMod (0 * 1)
⊢ inv_fun (to_fun x) = x
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
· exact geom_sum_ne_zero hx hn

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ cons p p.properDivisors ⋯, f x = f p * f 1

Tactic:
prod_cons,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ f p * ∏ x ∈ p.properDivisors, f x = f p * f 1
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
x : ZMod (1 * 0)
⊢ inv_fun (to_fun x) = x

Tactic:
;

Goal state after:
case inr.left
m n : ℕ
h : Nat.Coprime 1 0
to_fun : ZMod (1 * 0) → ZMod 1 × ZMod 0 := ⇑(castHom ⋯ (ZMod 1 × ZMod 0))
inv_fun : ZMod 1 × ZMod 0 → ZMod (1 * 0) :=
  fun x ↦
    if 1 * 0 = 0 then
      if 1 = 1 then ((RingHom.snd (ZMod 1) (ZMod 0)) x).cast else ((RingHom.fst (ZMod 1) (ZMod 0)) x).cast
    else ↑↑(Nat.chineseRemainder h x.1.val x.2.val)
hmn0 : 1 * 0 = 0
x : ZMod (1 * 0)
⊢ inv_fun (to_fun x) = x
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag

Tactic:
;

Goal state after:
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag

Tactic:
;

Goal state after:
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a✝ ∈ z.divisorsAntidiag
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ (-z).divisorsAntidiag ↔
    a✝ ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
;

Goal state after:
z : ℤ
a✝ : ℤ × ℤ
⊢ a✝ ∈ (-z).divisorsAntidiag ↔
    a✝ ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «1»
⊢ ↑(-1) = 1

Tactic:
;

Goal state after:
case «1»
⊢ ↑(-1) = 1
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.descFactorial k / k ! < n.descFactorial k

Tactic:
;

Goal state after:
n k : ℕ
hk : 2 ≤ k
hkn : k ≤ n
⊢ n.descFactorial k / k ! < n.descFactorial k
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
apply Nat.mul_le_mul_left

Goal state after:
case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ 2 ≤ n✝ + 1 + 1
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
;

Goal state after:
case h.inl
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.ZMod.Basic

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

pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
;

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
;

Goal state after:
case hbc
n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ n < n * n.centralBinom
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:
;

Goal state after:
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
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
;

Goal state after:
case pos.refl
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val 0 ≤ a.val
⊢ (a - 0).val = a.val - val 0
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:
;

Goal state after:
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * (n + 4).centralBinom ≤ 2 * ((n + 4) * (n + 4).centralBinom)
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
;

Goal state after:
m : ℕ
nzm : NeZero (m + 1)
a : ZMod (m + 1)
h : a.val < 0
⊢ False
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y ↦ ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y ↦ ↑x + b * y) 0 L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n

Tactic:
;

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a

Goal state after:
n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
k : ℤ
⊢ f ↑k = g ↑k
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
;

Goal state after:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
;

Goal state after:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m k n y : ℕ
| m * y + k = n

Tactic:
;

Goal state after:
m k n y : ℕ
| m * y + k = n
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:
intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂

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

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

Tactic:
refine iff_of_false (fun hdvd ↦ ?_) (Nat.not_le_of_lt hlt)

Goal state after:
case inl
p k a b : ℕ
hp : 1 < p
hb : ¬p ∣ b
hn : p ^ a * b ≠ 0
hlt : a < k
hdvd : p ^ k ∣ p ^ a * b
⊢ False
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case e_f
b : ℕ
l : List ℕ
⊢ (fun a i ↦ a * b ^ (i + 1)) = fun a i ↦ b * (a * b ^ i)

Tactic:
;

Goal state after:
case e_f
b : ℕ
l : List ℕ
⊢ (fun a i ↦ a * b ^ (i + 1)) = fun a i ↦ b * (a * b ^ i)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case e_f
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * b ^ (x✝ + 1) = b * (x✝¹ * b ^ x✝)

Tactic:
;

Goal state after:
case e_f
b : ℕ
l : List ℕ
x✝¹ x✝ : ℕ
⊢ x✝¹ * b ^ (x✝ + 1) = b * (x✝¹ * b ^ x✝)
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
apply Nat.mul_le_mul_left

Goal state after:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl
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:
rcases b with (_ | _ | b) <;> simp_all [base_pow_length_digits_le']

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

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

Tactic:
;

Goal state after:
case nil
α : Type u_1
inst✝ : CommRing α
a b k : α
h : k ∣ a - b
⊢ k ∣ 0 - 0
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
;

Goal state after:
case zero
b : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → l1.length = l2.length
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length →
      (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
        (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length

Tactic:
;

Goal state after:
case succ
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length →
      (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
        (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ (∀ (n : ℕ), a ^ n ∣ b) → ∀ (x : ℕ), a ^ (x + 1) ∣ b
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
;

Goal state after:
case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
nh : ∀ (n : ℕ), a ^ (n + 1) ∣ b
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hdiv : a ∣ b
h : multiplicity a b = 0
nh : ∀ (n : ℕ), a ^ (n + 1) ∣ b
⊢ False
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
;

Goal state after:
case zero
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

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

pp: case inr
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
;

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

case inr
p n : ℕ
hn₀ : n ≠ 0
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

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

pp: case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
;

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

case inr.inr
p n : ℕ
hn₀ : n ≠ 0
hp₁ : p ≠ 1
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
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:
;

Goal state after:
α : 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
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b

Tactic:
;

Goal state after:
a b : ℕ
h : ∀ (n : ℕ), 0 ^ n ∣ b
hb : ¬b = 0
ha : a = 0
⊢ 0 ∣ b
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b m n✝ p n : ℕ
⊢ ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)

Tactic:
;

Goal state after:
a b m n✝ p n : ℕ
⊢ ∀ (a : ℕ), Prime a → (a ∣ n ∧ ¬n = 0 ↔ ¬a = 1 ∧ ¬n = 0 ∧ a ∣ n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ IsConj (x ^ n) (y ^ n)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x y : G
h : IsConj x y
n : ℕ
n_gt_0 : 0 < n
eq' : x ^ n = 1
⊢ y ^ n = 1

Tactic:
rw [← isConj_one_right, ← eq']; exact h.pow n

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

Goal state before:
pp: a✝ : ℕ
⊢ (factorization 0) a✝ = 0 a✝

Tactic:
;

Goal state after:
a✝ : ℕ
⊢ (factorization 0) a✝ = 0 a✝
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a✝ : ℕ
⊢ (factorization 1) a✝ = 0 a✝

Tactic:
;

Goal state after:
a✝ : ℕ
⊢ (factorization 1) a✝ = 0 a✝
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ Finset (List ℕ)

Tactic:
by
  have : Fintype {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} :=
    Fintype.ofInjective (Set.MapsTo.restrict _ _ _ (mapsTo_ofDigits hb l))
      <| (Set.MapsTo.restrict_inj (mapsTo_ofDigits hb l)).mpr <| injOn_ofDigits hb l
  exact {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset

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

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

Tactic:
;

Goal state after:
b : ℕ
hb : 1 < b
l x✝ : ℕ
⊢ x✝ ∈ ↑(Finset.range (b ^ l)) ↔ x✝ ∈ {n | n < b ^ l}
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b < emultiplicity p a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p a

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y

Tactic:
;

Goal state after:
G : Type u_1
β : Type u_5
inst✝¹ : Monoid G
x : G
inst✝ : Monoid β
y : β
hx : 0 < orderOf x
h : orderOf y ∣ orderOf x
⊢ 0 < orderOf y
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
hfin : FiniteMultiplicity p a
k✝ k : ℕ
ha : FiniteMultiplicity p a
⊢ FiniteMultiplicity p (a * a ^ k)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
exact ⟨1, by rw [h, pow_one, pow_one]⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
inst✝¹ : Monoid G
a b x✝ y : G
n m : ℕ
M : Type ?u.16
inst✝ : Monoid M
x : M
hx : IsOfFinOrder x
⊢ x * x ^ (orderOf x - 1) = 1

Tactic:
by rw [← _root_.pow_succ', tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hx : orderOf x / n * n ≠ 0
hn : n ∣ orderOf x
⊢ orderOf x / n ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

pp: case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
;

Goal state after:
case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization