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

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L

pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)

Tactic:
·

Goal state after:
case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
⊢ ∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p a < multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0

pp: case succ.inr
n k : ℕ
ih : (n ^ k).factorization = k • n.factorization
hn : n ≠ 0
⊢ (n ^ (k + 1)).factorization = (k + 1) • n.factorization

Tactic:
·

Goal state after:
case succ.inl
k : ℕ
ih : (0 ^ k).factorization = k • factorization 0
⊢ (0 ^ (k + 1)).factorization = (k + 1) • factorization 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
h✝ : multiplicity p a = multiplicity p b
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1.refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ L.tail.length = l

pp: case refine_1.refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∀ x ∈ L.tail, x < b

Tactic:
·

Goal state after:
case refine_1.refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ L.tail.length = l
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
ha : FiniteMultiplicity p a
hb : FiniteMultiplicity p b
h : multiplicity p a ≠ multiplicity p b
hab : multiplicity p b < multiplicity p a
⊢ multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1.refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∀ x ∈ L.tail, x < b

Tactic:
·

Goal state after:
case refine_1.refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ fixedLengthDigits hb (l + 1)
hL₁ : L.length = l + 1
hL₂ : ∀ x ∈ L, x < b
hL₃ : L ≠ []
⊢ ∀ x ∈ L.tail, x < b
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)

Tactic:
·

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ (∃ a < b, ∃ a_1 ∈ fixedLengthDigits hb l, a :: a_1 = L) → L ∈ fixedLengthDigits hb (l + 1)
Module: Mathlib.Data.Nat.Digits.Lemmas

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

Tactic:
by
  ext L
  simp_rw [Finset.disjiUnion_eq_biUnion, Finset.mem_biUnion, Finset.mem_range,
    consFixedLengthDigits, Finset.mem_image]
  refine ⟨fun hL ↦ ?_, ?_⟩
  · have hL₁ : L.length = l + 1 := ((mem_fixedLengthDigits_iff hb).mp hL).1
    have hL₂ : ∀ x ∈ L, x < b := ((mem_fixedLengthDigits_iff hb).mp hL).2
    have hL₃ : L ≠ [] := by simp [ne_nil_iff_length_pos, hL₁]
    refine ⟨L.head hL₃, hL₂ _ (L.head_mem hL₃), L.tail, ?_, cons_head_tail hL₃⟩
    refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
    · rw [length_tail, hL₁, Nat.add_sub_cancel_right]
    · exact fun x hx ↦ hL₂ _ <| mem_of_mem_tail hx
  · rintro ⟨d, hd₁, T, hT, rfl⟩
    exact cons_mem_fixedLengthDigits_succ hb l d hd₁ hT

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ n ≠ 1

Tactic:
by lia

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) (Set.Iio (orderOf x))

Tactic:
simpa only [mul_left_iterate_apply_one]
    using! iterate_injOn_Iio_minimalPeriod (f := (x * ·)) (x := 1)

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

Goal state before:
pp: case pos
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
·

Goal state after:
case pos
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : l = 0
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case inl
f : ℕ →₀ ℕ
hf : f ≤ factorization 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ 0

pp: case inr
n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
hn : n ≠ 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
·

Goal state after:
case inl
f : ℕ →₀ ℕ
hf : f ≤ factorization 0
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ 0
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

pp: case neg
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:
·

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
rw [ha.multiplicity_eq_iff]

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
⊢ a ^ 1 ∣ a ∧ ¬a ^ (1 + 1) ∣ a
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False

pp: case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Tactic:
·

Goal state after:
case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False
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
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

pp: case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False

Tactic:
·

Goal state after:
case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
v : α
ha : FiniteMultiplicity 0 0
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
ha : ¬FiniteMultiplicity a a
⊢ multiplicity a a = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ 1 < orderOf x

Tactic:
by lia

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

Goal state before:
pp: case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ (fixedLengthDigits hb l).card * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * b.choose 2) = (l + 1) * b ^ l * b.choose 2

Tactic:
card_fixedLengthDigits,

Goal state after:
case neg
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
hl : ¬l = 0
⊢ b ^ l * (b * (b - 1) / 2) + b * (l * b ^ (l - 1) * b.choose 2) = (l + 1) * b ^ l * b.choose 2
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

pp: case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Tactic:
·

Goal state after:
case refine_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0

Tactic:
·

Goal state after:
case refine_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x

Tactic:
·

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x

Tactic:
·

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ IsOfFinOrder x
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2

Tactic:
rw [← List.sum_fixedLengthDigits_sum hb]
  refine (Finset.sum_nbij (ofDigits b) (by exact (bijOn_ofDigits' hb l).1)
    (bijOn_ofDigits' hb l).2.1 (bijOn_ofDigits' hb l).2.2 fun L hL ↦ ?_).symm
  rw [sum_digits_ofDigits_eq_sum hb ((List.mem_fixedLengthDigits_iff hb).mp hL)]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n

pp: case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n

Tactic:
·

Goal state after:
case hk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n

Tactic:
·

Goal state after:
case hsucc
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n

pp: case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n

Tactic:
·

Goal state after:
case pos
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ n.factorization p < n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n

Tactic:
·

Goal state after:
case neg
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ n.factorization p < n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

pp: case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
·

Goal state after:
case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization
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
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

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

Tactic:
·

Goal state after:
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

pp: case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q

pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
·

Goal state after:
case inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
·

Goal state after:
case inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q
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))

pp: case neg
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:
·

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 ∣ (orderOf x).lcm (orderOf (x * y))
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 ∣ 0

Tactic:
apply dvd_zero

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

Goal state before:
pp: case ha
p k : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p ≠ 0

pp: case hb
p k : ℕ
hp : Prime p
⊢ 1 ≠ 0

pp: case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1

Tactic:
·

Goal state after:
case ha
p k : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hb
p k : ℕ
hp : Prime p
⊢ 1 ≠ 0

pp: case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1

Tactic:
·

Goal state after:
case hb
p k : ℕ
hp : Prime p
⊢ 1 ≠ 0
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1

Tactic:
·

Goal state after:
case h
p k : ℕ
hp : Prime p
⊢ ∀ (p_1 : ℕ), (p ^ k / p ^ (p ^ k).factorization p).factorization p_1 = (factorization 1) p_1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mp
n p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n → n = 0 ∨ ¬p ∣ n

pp: case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n

Tactic:
·

Goal state after:
case mp
n p : ℕ
hp : Prime p
⊢ n / p ^ n.factorization p = n → n = 0 ∨ ¬p ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case pos
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : n = 0
⊢ n = 0 ∨ ¬p ∣ n

pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
·

Goal state after:
case pos
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : n = 0
⊢ n = 0 ∨ ¬p ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
·

Goal state after:
case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n

Tactic:
·

Goal state after:
case mpr
n p : ℕ
hp : Prime p
⊢ n = 0 ∨ ¬p ∣ n → n / p ^ n.factorization p = n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr.inl
n p : ℕ
hp : Prime p
n_eq_zero : n = 0
⊢ n / p ^ n.factorization p = n

pp: case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n

Tactic:
·

Goal state after:
case mpr.inl
n p : ℕ
hp : Prime p
n_eq_zero : n = 0
⊢ n / p ^ n.factorization p = n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n

Tactic:
·

Goal state after:
case mpr.inr
n p : ℕ
hp : Prime p
not_dvd : ¬p ∣ n
⊢ n / p ^ n.factorization p = n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hx
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y

pp: case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p

Tactic:
·

Goal state after:
case hx
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n

pp: case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
·

Goal state after:
case a
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p + k.factorization p ≤ n