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

Goal state before:
pp: case zero
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n
⊢ ZMod 0 ≃+* ZMod n

pp: case succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n m : ℕ
h : m + 1 = n
⊢ ZMod (m + 1) ≃+* ZMod n

Tactic:
<;>

Goal state after:
case zero
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n : ℕ
h : 0 = n
⊢ ZMod 0 ≃+* ZMod n

case succ
n✝ : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n✝
n m : ℕ
h : m + 1 = n
⊢ ZMod (m + 1) ≃+* ZMod n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod 0)

pp: case succ
n✝ : ℕ
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod (n✝ + 1))

Tactic:
<;>

Goal state after:
case zero
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod 0)

case succ
n✝ : ℕ
⊢ ringEquivCongr ⋯ = RingEquiv.refl (ZMod (n✝ + 1))
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

pp: case succ
n✝ : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
<;>

Goal state after:
case zero
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

case succ
n✝ : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

pp: case succ
n✝ : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
<;>

Goal state after:
case zero
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

case succ
n✝ : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
x : ZMod 0
⊢ ((ringEquivCongr ⋯) x).val = x.val

pp: case succ
n✝ : ℕ
x : ZMod (n✝ + 1)
⊢ ((ringEquivCongr ⋯) x).val = x.val

Tactic:
<;>

Goal state after:
case zero
x : ZMod 0
⊢ ((ringEquivCongr ⋯) x).val = x.val

case succ
n✝ : ℕ
x : ZMod (n✝ + 1)
⊢ ((ringEquivCongr ⋯) x).val = x.val
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
x y : ι → G
⊢ (QuotientGroup.leftRel (pi Set.univ H)) x y ↔ piSetoid x y

Tactic:
QuotientGroup.leftRel_pi

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
H : ι → Subgroup G
x y : ι → G
⊢ piSetoid x y ↔ piSetoid x y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑z.val + ↑p * k

pp: case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑z.val + ↑p * k) → ↑n = z

Tactic:
· rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_intCast, Int.emod_add_mul_ediv]

Goal state after:
case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑z.val + ↑p * k) → ↑n = z
Module: Mathlib.Data.ZMod.Basic

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

pp: case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ a.val * b.val < n → (a * b).val = a.val * b.val

Tactic:
<;>

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

case mpr
n : ℕ
inst✝ : NeZero n
a b : ZMod n
⊢ a.val * b.val < n → (a * b).val = a.val * b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero.inl
⊢ (↑1).val.Coprime 0

pp: case zero.inr
⊢ (↑(-1)).val.Coprime 0

Tactic:
<;>

Goal state after:
case zero.inl
⊢ (↑1).val.Coprime 0

case zero.inr
⊢ (↑(-1)).val.Coprime 0
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n

pp: case mpr
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n → ∑ i ∈ n.properDivisors, i = n

Tactic:
<;>

Goal state after:
case mp
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n

case mpr
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n → ∑ i ∈ n.properDivisors, i = n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
h✝ : ¬Even n.succ.succ
this : 1 < ∑ i ∈ range n.succ.succ, x ^ i
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
· exact (zero_lt_one.trans this).ne'

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n.properDivisors = {1}
⊢ Prime n

Tactic:
Nat.prime_def_lt

Goal state after:
n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ x ∈ Ico (0 + 1) n.succ, a / b ^ x

pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (0 + 1) n.succ

Tactic:
<;>

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / b ^ 0 + ∑ x ∈ Ico (0 + 1) n.succ, a / b ^ x

b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (0 + 1) n.succ
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «0»
⊢ -(fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

pp: case «1»
⊢ -(fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
<;>

Goal state after:
case «0»
⊢ -(fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

case «1»
⊢ -(fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case «0»
⊢ ↑(-(fun i ↦ i) ⟨0, ⋯⟩) = ↑((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
⊢ ↑(-(fun i ↦ i) ⟨1, ⋯⟩) = ↑((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
⊢ ↑(-(fun i ↦ i) ⟨0, ⋯⟩) = ↑((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
⊢ ↑(-(fun i ↦ i) ⟨1, ⋯⟩) = ↑((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inl
a : ℤ
h✝ : a ≤ 0
⊢ ↑|a| = ↑a

pp: case inr
a : ℤ
h✝ : 0 ≤ a
⊢ ↑|a| = ↑a

Tactic:
<;>

Goal state after:
case inl
a : ℤ
h✝ : a ≤ 0
⊢ ↑|a| = ↑a

case inr
a : ℤ
h✝ : 0 ≤ a
⊢ ↑|a| = ↑a
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
⊢ (-↑0).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (Nat.divisorsAntidiagonal 0)).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯

pp: case succ
n✝ : ℕ
⊢ (-↑(n✝ + 1)).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (n✝ + 1).divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (n✝ + 1).divisorsAntidiagonal) ⋯

Tactic:
<;>

Goal state after:
case zero
⊢ (-↑0).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (Nat.divisorsAntidiagonal 0)).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯

case succ
n✝ : ℕ
⊢ (-↑(n✝ + 1)).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) (n✝ + 1).divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) (n✝ + 1).divisorsAntidiagonal) ⋯
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case neg.zero.zero
lt : ¬0 + 1 < 0
⊢ (0 + 1).choose 0 ≤ 2 ^ 0

pp: case neg.zero.succ
n✝ : ℕ
lt : ¬0 + 1 < n✝ + 1
⊢ (0 + 1).choose (n✝ + 1) ≤ 2 ^ 0

Tactic:
<;>

Goal state after:
case neg.zero.zero
lt : ¬0 + 1 < 0
⊢ (0 + 1).choose 0 ≤ 2 ^ 0

case neg.zero.succ
n✝ : ℕ
lt : ¬0 + 1 < n✝ + 1
⊢ (0 + 1).choose (n✝ + 1) ≤ 2 ^ 0
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: case inl.zero
⊢ choose 0 0 ≤ 2 ^ 0

pp: case inl.succ
n✝ : ℕ
⊢ choose 0 (n✝ + 1) ≤ 2 ^ 0

Tactic:
<;>

Goal state after:
case inl.zero
⊢ choose 0 0 ≤ 2 ^ 0

case inl.succ
n✝ : ℕ
⊢ choose 0 (n✝ + 1) ≤ 2 ^ 0
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
  by_cases hb : b = 0
  · cases hb; simp
  · have : NeZero b := ⟨hb⟩
    rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
    apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

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

Goal state before:
pp: case zero
⊢ digits 0 0 = []

pp: case succ.zero
⊢ (0 + 1).digits 0 = []

pp: case succ.succ
n✝ : ℕ
⊢ (n✝ + 1 + 1).digits 0 = []

Tactic:
<;>

Goal state after:
case zero
⊢ digits 0 0 = []

case succ.zero
⊢ (0 + 1).digits 0 = []

case succ.succ
n✝ : ℕ
⊢ (n✝ + 1 + 1).digits 0 = []
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
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
this : a.val ^ m < n
⊢ (a ^ m).val * a.val % n = a.val ^ (m + 1)

Tactic:
ih this,

Goal state after:
case succ
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
this : a.val ^ m < n
⊢ a.val ^ m * a.val % n = a.val ^ (m + 1)
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:
simp [neg_eq_self, sub_eq_add_neg]

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

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

Tactic:
intro h
    have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
    convert! this
    rw [ofDigits_digits]

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

Goal state before:
pp: case inl
⊢ maxPowDvdDiv 1 1 = (0, 1)

pp: case inr
p : ℕ
hp : p ≠ 1
⊢ p.maxPowDvdDiv 1 = (0, 1)

Tactic:
<;>

Goal state after:
case inl
⊢ maxPowDvdDiv 1 1 = (0, 1)

case inr
p : ℕ
hp : p ≠ 1
⊢ p.maxPowDvdDiv 1 = (0, 1)
Module: Mathlib.Data.Nat.MaxPowDiv

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

pp: case inl.inr
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
hk : k > 0
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n

Tactic:
<;>

Goal state after:
case inl.inl
n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
⊢ 0 ^ 0 ∣ n ↔ 0 ≤ padicValNat 0 n

case inl.inr
k n : ℕ
hn : n ≠ 0
hp : 0 ≠ 1
hk : k > 0
⊢ 0 ^ k ∣ n ↔ k ≤ padicValNat 0 n
Module: Mathlib.Data.Nat.MaxPowDiv

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

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

Tactic:
<;>

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

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case inr.refine_1.inl
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits n
⊢ l < b

pp: case inr.refine_1.inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits m
⊢ l < b

Tactic:
<;>

Goal state after:
case inr.refine_1.inl
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits n
⊢ l < b

case inr.refine_1.inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits m
⊢ l < b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inr.inl.«0»
b n : ℕ
hn : n ≠ 0
hb : 0 ≤ 1
⊢ (digits 0 n).length ≤ (digits 0 (n + 1)).length

pp: case inr.inl.«1»
b n : ℕ
hn : n ≠ 0
hb : 1 ≤ 1
⊢ (digits 1 n).length ≤ (digits 1 (n + 1)).length

Tactic:
<;>

Goal state after:
case inr.inl.«0»
b n : ℕ
hn : n ≠ 0
hb : 0 ≤ 1
⊢ (digits 0 n).length ≤ (digits 0 (n + 1)).length

case inr.inl.«1»
b n : ℕ
hn : n ≠ 0
hb : 1 ≤ 1
⊢ (digits 1 n).length ≤ (digits 1 (n + 1)).length
Module: Mathlib.Data.Nat.Digits.Lemmas

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

pp: case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m ≠ 0 → (0 + 1) ^ ((0 + 1).digits m).length ≤ (0 + 1) * m

pp: case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m

Tactic:
<;>

Goal state after:
case zero
m : ℕ
hb : 1 < 0
⊢ m ≠ 0 → 0 ^ (digits 0 m).length ≤ 0 * m

case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m ≠ 0 → (0 + 1) ^ ((0 + 1).digits m).length ≤ (0 + 1) * m

case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case ind.succ.tail.a.hLtN
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 0 < n + 1

pp: case ind.succ.tail.a.hLtK
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 1 < b + 2

Tactic:
<;>

Goal state after:
case ind.succ.tail.a.hLtN
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 0 < n + 1

case ind.succ.tail.a.hLtK
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
a✝ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 1 < b + 2
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
m d : ℕ
hb : 1 < 0
hd : d ∈ digits 0 m
⊢ d < 0

pp: case succ.zero
m d : ℕ
hb : 1 < 0 + 1
hd : d ∈ (0 + 1).digits m
⊢ d < 0 + 1

pp: case succ.succ
m d b : ℕ
hb : 1 < b + 1 + 1
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Tactic:
<;>

Goal state after:
case zero
m d : ℕ
hb : 1 < 0
hd : d ∈ digits 0 m
⊢ d < 0

case succ.zero
m d : ℕ
hb : 1 < 0 + 1
hd : d ∈ (0 + 1).digits m
⊢ d < 0 + 1

case succ.succ
m d b : ℕ
hb : 1 < b + 1 + 1
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1
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
⊢ ofDigits (b + 2) (hd :: tl) < (b + 2) ^ (hd :: tl).length

Tactic:
rw [ofDigits, List.length_cons, pow_succ]
    have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
    suffices ↑hd < b + 2 by linarith
    exact hl hd List.mem_cons_self

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

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

pp: case succ.zero
l : List ℕ
hb : 1 < 0 + 1
hl : ∀ x ∈ l, x < 0 + 1
⊢ ofDigits (0 + 1) l < (0 + 1) ^ l.length

pp: case succ.succ
l : List ℕ
b : ℕ
hb : 1 < b + 1 + 1
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length

Tactic:
<;>

Goal state after:
case zero
l : List ℕ
hb : 1 < 0
hl : ∀ x ∈ l, x < 0
⊢ ofDigits 0 l < 0 ^ l.length

case succ.zero
l : List ℕ
hb : 1 < 0 + 1
hl : ∀ x ∈ l, x < 0 + 1
⊢ ofDigits (0 + 1) l < (0 + 1) ^ l.length

case succ.succ
l : List ℕ
b : ℕ
hb : 1 < b + 1 + 1
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length
Module: Mathlib.Data.Nat.Digits.Defs

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

pp: case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m < (0 + 1) ^ ((0 + 1).digits m).length

pp: case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Tactic:
<;>

Goal state after:
case zero
m : ℕ
hb : 1 < 0
⊢ m < 0 ^ (digits 0 m).length

case succ.zero
m : ℕ
hb : 1 < 0 + 1
⊢ m < (0 + 1) ^ ((0 + 1).digits m).length

case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
induction L with
  | nil => change k ∣ 0 - 0; simp
  | cons d L ih =>
    simp only [ofDigits, add_sub_add_left_eq_sub]
    exact dvd_mul_sub_mul h ih

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

Goal state before:
pp: case nil
b : ℕ
⊢ ofDigits b [] % b = [].head! % b

pp: case cons
b head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ofDigits b tail✝ % b = tail✝.head! % b
⊢ ofDigits b (head✝ :: tail✝) % b = (head✝ :: tail✝).head! % b

Tactic:
<;>

Goal state after:
case nil
b : ℕ
⊢ ofDigits b [] % b = [].head! % b

case cons
b head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ofDigits b tail✝ % b = tail✝.head! % b
⊢ ofDigits b (head✝ :: tail✝) % b = (head✝ :: tail✝).head! % b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case neg.zero
b : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits 0).head! = 0 % b

pp: case neg.succ
b : ℕ
h : b ≠ 1
hb : ¬1 < b
n✝ : ℕ
⊢ (b.digits (n✝ + 1)).head! = (n✝ + 1) % b

Tactic:
<;>

Goal state after:
case neg.zero
b : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits 0).head! = 0 % b

case neg.succ
b : ℕ
h : b ≠ 1
hb : ¬1 < b
n✝ : ℕ
⊢ (b.digits (n✝ + 1)).head! = (n✝ + 1) % b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case h₂
a b : ℕ
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, ¬a ^ (n + 1) ∣ b
x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b

pp: case h₁
a b x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b

Tactic:
<;>

Goal state after:
case h₂
a b : ℕ
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, ¬a ^ (n + 1) ∣ b
x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ b

case h₁
a b x✝ : ℕ
⊢ ↑a ^ (x✝ + 1) ∣ ↑b ↔ a ^ (x✝ + 1) ∣ 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
⊢ ¬a ^ m ∣ b

Tactic:
apply not_pow_dvd_of_emultiplicity_lt
  rw [hf.emultiplicity_eq_multiplicity]
  norm_cast

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
  simp [IsOfFinOrder, mem_periodicPts, isPeriodicPt_mul_iff_pow_eq_one]

Goal state after:
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 = 1
h : n = ↑n.natAbs
⊢ x ^ n.natAbs = 1

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 = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
· rwa [h, zpow_natCast] at hn'

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 = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
a b : ℕ
h✝ : a = 1
⊢ ∀ (n : ℕ), a ^ n ∣ b

pp: case inr
a b : ℕ
h✝ : b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
<;>

Goal state after:
case inl
a b : ℕ
h✝ : a = 1
⊢ ∀ (n : ℕ), a ^ n ∣ b

case inr
a b : ℕ
h✝ : b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

pp: case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

Tactic:
<;>

Goal state after:
case inl
a : ℕ
b : ℤ
h : b = ↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b

case inr
a : ℕ
b : ℤ
h : b = -↑b.natAbs
⊢ emultiplicity a b.natAbs = emultiplicity (↑a) b
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 b

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 b

α : 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 b

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 b

α : 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.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ L ∈ (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

Tactic:
simp_rw [Finset.disjiUnion_eq_biUnion, Finset.mem_biUnion, Finset.mem_range,
    consFixedLengthDigits, Finset.mem_image]

Goal state after:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb (l + 1) ↔ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case h_t
p : ℕ
hp : Prime p
q : ℕ
⊢ 1 = ?m.41

pp: case h_e
p : ℕ
hp : Prime p
q : ℕ
⊢ 0 = ?m.42

pp: p : ℕ
hp : Prime p
q : ℕ
⊢ ℕ

pp: p : ℕ
hp : Prime p
q : ℕ
⊢ ℕ

Tactic:
<;>

Goal state after:
case h_t
p : ℕ
hp : Prime p
q : ℕ
⊢ 1 = ?m.41

case h_e
p : ℕ
hp : Prime p
q : ℕ
⊢ 0 = ?m.42

p : ℕ
hp : Prime p
q : ℕ
⊢ ℕ

p : ℕ
hp : Prime p
q : ℕ
⊢ ℕ
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case mp
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization → (f.prod fun x1 x2 ↦ x1 ^ x2) = n

pp: case mpr
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) = n → f = n.factorization

Tactic:
<;>

Goal state after:
case mp
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ f = n.factorization → (f.prod fun x1 x2 ↦ x1 ^ x2) = n

case mpr
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ p ∈ f.support, Prime p
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) = n → f = n.factorization
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
h0,

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime 0
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ 0 ^ a.factorization 0 ∣ 0 ^ b.factorization 0 ↔ a.factorization 0 ≤ b.factorization 0

pp: case succ.zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (0 + 1) ^ a.factorization (0 + 1) ∣ (0 + 1) ^ b.factorization (0 + 1) ↔
    a.factorization (0 + 1) ≤ b.factorization (0 + 1)

pp: case succ.succ
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (p + 1 + 1) ^ a.factorization (p + 1 + 1) ∣ (p + 1 + 1) ^ b.factorization (p + 1 + 1) ↔
    a.factorization (p + 1 + 1) ≤ b.factorization (p + 1 + 1)

Tactic:
<;>

Goal state after:
case zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ 0 ^ a.factorization 0 ∣ 0 ^ b.factorization 0 ↔ a.factorization 0 ≤ b.factorization 0

case succ.zero
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (0 + 1) ^ a.factorization (0 + 1) ∣ (0 + 1) ^ b.factorization (0 + 1) ↔
    a.factorization (0 + 1) ≤ b.factorization (0 + 1)

case succ.succ
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (p + 1 + 1) ^ a.factorization (p + 1 + 1) ∣ (p + 1 + 1) ^ b.factorization (p + 1 + 1) ↔
    a.factorization (p + 1 + 1) ≤ b.factorization (p + 1 + 1)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ (orderOf x).lcm (orderOf (x * y))

Tactic:
h0,

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ Nat.lcm 0 (orderOf (x * y))