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

Goal state before:
pp: case zero
a : ℕ
ha : Prime a
b : ℕ
hb : b ≠ 0
⊢ replicate 0 a <+~ b.primeFactorsList ↔ a ^ 0 ∣ b

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (comap f (map f H)).relIndex (comap f (map f K))

Tactic:
relIndex_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (map f H).relIndex (map f (comap f (map f K)))
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
K : Subgroup G
f : G →* G'
⊢ (comap f ⊥).relIndex K = Nat.card ↥(map f K)

Tactic:
relIndex_comap,

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
K : Subgroup G
f : G →* G'
⊢ ⊥.relIndex (map f K) = Nat.card ↥(map f K)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.relIndex K ≠ 0 ↔ (H.subgroupOf K).index ≠ 0

Tactic:
relIndex

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H.subgroupOf K).index ≠ 0 ↔ (H.subgroupOf K).index ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ Function.Injective ⇑((MulDistribMulAction.toMonoidEnd H G) h)

Tactic:
intro a

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
a : G
⊢ ∀ ⦃a₂ : G⦄, ((MulDistribMulAction.toMonoidEnd H G) h) a = ((MulDistribMulAction.toMonoidEnd H G) h) a₂ → a = a₂
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ Function.Injective ⇑((DistribMulAction.toAddMonoidEnd H G) h)

Tactic:
intro a

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
a : G
⊢ ∀ ⦃a₂ : G⦄, ((DistribMulAction.toAddMonoidEnd H G) h) a = ((DistribMulAction.toAddMonoidEnd H G) h) a₂ → a = a₂
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
n : ℕ
nzm : NeZero 0
h : 0 ≤ n
⊢ Injective cast

Tactic:
| zero =>

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

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Injective val

Tactic:
intro a

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ∀ ⦃a₂ : ZMod (n✝ + 1)⦄, a.val = a₂.val → a = a₂
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
simp [divisors]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
⊢ if Even 0 then ∑ i ∈ range 0, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range 0, x ^ i

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x + 1 < 0
hn : 1 < n
hx0 : x < 0
⊢ if Even 2 then ∑ i ∈ range 2, x ^ i < 0 else 1 < ∑ i ∈ range 2, x ^ i

Tactic:
simp only [geom_sum_two, lt_add_iff_pos_left, ite_true, hx, even_two]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
n : ℕ
h : 0 ∣ n ∧ n ≠ 0
⊢ 0 < 0

Tactic:
zero_dvd_iff (a := n)

Goal state after:
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < 0
Module: Mathlib.Data.Nat.Choose.Bounds

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

Tactic:
| zero =>

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

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

Tactic:
exact two_dvd_centralBinom_succ n.pred

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

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Tactic:
simp [Nat.ne_of_gt, *]

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

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

Tactic:
simp [Nat.ne_of_gt, *]

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:
simpa using maxPowDvdDiv_base_pow_mul hp hn 1

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

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

Tactic:
tsub_add_cancel_of_le

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

case neg
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n
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
  induction L1 generalizing L2 with
  | nil =>
    simp only [List.length_nil] at len
    exact (List.length_eq_zero_iff.mp len.symm).symm
  | cons D L ih => ?_
  obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm
  simp only [List.length_cons, add_left_inj] at len
  simp only [ofDigits_cons] at h
  have eqd : D = d := by
    have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]
    simpa [mod_eq_of_lt (w2 d List.mem_cons_self),
      mod_eq_of_lt (w1 D List.mem_cons_self)] using H
  simp only [eqd, add_right_inj, mul_left_cancel_iff_of_pos (zero_lt_of_lt hb)] at h
  have := ih len (fun a ha ↦ w1 a <| List.mem_cons_of_mem D ha)
    (fun a ha ↦ w2 a <| List.mem_cons_of_mem d ha) h
  rw [eqd, this]

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
⊢ (p.digits 0).sum ≤ 0

Tactic:
| zero =>

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

Goal state before:
pp: case succ.zero
n : ℕ
a✝ : (digits 0 n).sum ≤ n
⊢ (digits 0 (n + 1)).sum ≤ n + 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ 0 = ofDigits p (List.drop 0 digits)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ 0 = ofDigits p (List.take 0 digits)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
⊢ digits 2 0 = List.map (fun b ↦ bif b then 1 else 0) (bits 0)

Tactic:
| zero =>

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

Goal state before:
pp: case cons
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]

Tactic:
dsimp [Nat.ModEq] at *

Goal state after:
case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ l1.length = l2.length

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
⊢ a ^ n ∣ b → ¬a ^ (n + 1) ∣ b → emultiplicity a b = ↑n

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

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

Goal state before:
pp: case zero
b n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore 0 n []).length ≤ e

Tactic:
| zero =>

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

Goal state before:
pp: case succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0
hlt : n < b ^ 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0

Tactic:
| zero =>

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

Goal state before:
pp: case succ.succ.zero
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < 0 + 1
hlt : n < b ^ (0 + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
| zero =>

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

Goal state before:
pp: case zero
b i : ℕ
⊢ ((b + 2).digits 0)[i]?.getD 0 = 0 / (b + 2) ^ i % (b + 2)

Tactic:
| zero =>

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

Goal state before:
pp: n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = n.factorization p

Tactic:
simp [factorization, pp]

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

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

Tactic:
simp [factorization]

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

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

Tactic:
simp [factorization]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ emultiplicity p (a + b) = ↑(multiplicity p b)

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

Goal state after:
case hk
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ multiplicity p b ∣ a + b

case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ a + b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ (if h : 1 ∈ periodicPts fun x_1 ↦ x * x_1 then Nat.find h else 0) = 0

Tactic:
dif_neg

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ 0 = 0

case hnc
G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ 1 ∉ periodicPts fun x_1 ↦ x * x_1
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: case zero
n : ℕ
⊢ (n ^ 0).factorization = 0 • n.factorization

Tactic:
| zero =>

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

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
ψ : G →* H
x : G
⊢ orderOf (ψ x) ∣ orderOf x

Tactic:
apply orderOf_dvd_of_pow_eq_one
  rw [← map_pow, pow_orderOf_eq_one]
  apply map_one

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ (a * b).factorization q = a.factorization q + b.factorization q

Tactic:
factorization_mul_apply_of_coprime hab

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
⊢ a.factorization q + b.factorization q = a.factorization q + b.factorization q
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
⊢ False

Tactic:
have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
    obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
    rw [hb, ← mul_assoc] at ha
    exact Dvd.intro_left (orderOf x * b) ha.symm

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
⊢ False
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p a : α
hp : Prime p
⊢ emultiplicity p (a ^ 0) = ↑0 * emultiplicity p a

Tactic:
| zero =>

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ emultiplicity p (p ^ n) = ↑n

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

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

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.Choose.Factorization

Goal state before:
pp: case zero
p : ℕ
hp : Prime p
⊢ (p * 0)!.factorization p = 0!.factorization p + 0

Tactic:
| zero =>

Goal state after:
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
⊢ n ≤ ((p ^ n).choose k).factorization p + k.factorization p

Tactic:
nth_rewrite 1 [← factorization_pow_self (n := n) hp]
    exact factorization_le_factorization_choose_add hkn hk0

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

Goal state before:
pp: case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
p : ℕ
hp : (n.factorization - d.factorization) p < n.factorization p - d.factorization p
⊢ False

Tactic:
tsub_apply,

Goal state after:
case inr
d n : ℕ
hd : d ≠ 0
hdn : d ≤ n
hd_lt_n : d < n
h1 : n / d ≠ 0
h : (n / d).factorization = n.factorization - d.factorization
h2 : ¬n ≤ n / d * d
p : ℕ
hp : n.factorization p - d.factorization p < n.factorization p - d.factorization p
⊢ False
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝³ : Ring R
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors R
p : ℕ
hp : p ≠ 2
inst✝ : CharP R p
⊢ ¬-1 = 1

Tactic:
exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))

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

Goal state before:
pp: case zero
p n : ℕ
h : 0 < p
⊢ 0!.factorization p = 0

Tactic:
| zero =>

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

Goal state before:
pp: case hd.inl
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
hea : 0 ∣ a
heb : 0 ∣ b
⊢ 0 ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
exact absurd (zero_dvd_iff.mp hea) ha_pos

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ (closure s).toSubmonoid ≤ Submonoid.closure s

Tactic:
closure_toSubmonoid

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ Submonoid.closure (s ∪ s⁻¹) ≤ Submonoid.closure s
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: case zero
p : ℕ
hp : Prime p
⊢ emultiplicity p (p * 0)! = emultiplicity p 0! + ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
p : ℕ
hp : Prime p
⊢ emultiplicity p (p ^ 0)! = ↑(∑ i ∈ range 0, p ^ i)

Tactic:
| zero =>

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.lcm b).factorization = a.factorization ⊔ b.factorization

Tactic:
rw [← add_right_inj (a.gcd b).factorization, ←
    factorization_mul (mt gcd_eq_zero_iff.1 fun h => ha h.1) (lcm_ne_zero ha hb), gcd_mul_lcm,
    factorization_gcd ha hb, factorization_mul ha hb]
  ext1
  exact (min_add_max _ _).symm

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
⊢ emultiplicity p ((n + k).choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}))

Tactic:
refine WithTop.add_right_cancel ?_ h₁

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h₁ :
  emultiplicity p ((n + k).choose k) + emultiplicity p (k ! * n !) =
    ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i})) + emultiplicity p (k ! * n !)
⊢ emultiplicity p (k ! * n !) ≠ ⊤
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ emultiplicity p (n.choose k) = ↑(#({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}))

Tactic:
convert! @emultiplicity_choose' p (n - k) k b hp _

Goal state after:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k

p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k

Tactic:
have h1 := (injective_zpow_iff_not_isOfFinOrder.mpr hx) hl

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
hx : ¬IsOfFinOrder x
k : ℤ
h : zpowers x = zpowers (x ^ k)
hx_mem : x ∈ zpowers (x ^ k)
hy_mem : x ^ k ∈ zpowers x
l : ℤ
hl : x ^ (k * l) = x ^ 1
h1 : k * l = 1
⊢ x = x ^ k ∨ x⁻¹ = x ^ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case zero
p : ℕ
⊢ #({e ∈ Finset.range 0 | p ∣ e + 1}) = 0 / p

Tactic:
| zero =>

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

Goal state before:
pp: case zero
n : ℕ
⊢ #({k ∈ Finset.range (succ 0) | k ≠ 0 ∧ n ∣ k}) = 0 / n

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case zero
G : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝¹ : LeftCancelMonoid M
inst✝ : Finite M
S : Set M
hS1 : S.Nonempty
hS2 : S * S = S
a : M
ha : a ∈ S
⊢ a ^ (0 + 1) ∈ S

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
d df dg : ℕ
a b : R
f g : R[X]
h_mul_left✝ : f.natDegree ≤ df
h_mul_right✝ : g.natDegree ≤ dg
h_mul_left : f.coeff df = a
h_mul_right : g.coeff dg = b
ddf : df + dg ≤ d
⊢ (f * g).coeff d = if d = df + dg then a * b else 0

Tactic:
split_ifs with h
  · subst h_mul_left h_mul_right h
    exact coeff_mul_add_eq_of_natDegree_le ‹_› ‹_›
  · apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ddf ?_)
    · exact natDegree_mul_le_of_le ‹_› ‹_›
    · exact ne_comm.mp h

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : ℕ
c : R
p : R[X]
h_natDeg_le : p.natDegree ≤ m
coeff_eq : p.coeff o = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.natDegree = deg

Tactic:
by
  subst coeff_eq deg_eq_deg coeff_eq_deg
  exact natDegree_eq_of_le_of_coeff_ne_zero ‹_› ‹_›

Goal state after:
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
f : R[X]
hd : ∀ d < 0, f.coeff d = 0
⊢ X ^ 0 ∣ f

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.refine_1
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
n : ℕ
hn : ↑(f.natDegree * p) < ↑n
⊢ ((expand R p) f).coeff n = 0

Tactic:
rw [coeff_expand hp]
    split_ifs with hpn
    · rw [coeff_eq_zero_of_natDegree_lt]
      contrapose! hn
      norm_cast
      rw [← Nat.div_mul_cancel hpn]
      exact Nat.mul_le_mul_right p hn
    · rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ↑(f.natDegree * p) ≤ ((expand R p) f).degree

Tactic:
refine le_degree_of_ne_zero ?_

Goal state after:
case neg.refine_2
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : (expand R p) f ≠ 0
⊢ ((expand R p) f).coeff (f.natDegree * p) ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)

Tactic:
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff (n + 1) * ↑(n + 1) = p.coeff (n + 1) * (↑n + 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
⊢ (⇑derivative)^[0] (s • p) = s • (⇑derivative)^[0] p

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ((⇑derivative)^[0] p).natDegree ≤ p.natDegree - 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
⊢ ∀ (a : R), count a (x ::ₘ t) = rootMultiplicity a p

Tactic:
intro a

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : p ≠ 0
this : Decidable (∃ x, p.IsRoot x)
h : ∃ x, p.IsRoot x
x : R
hx : p.IsRoot x
hpd : 0 < p.degree
hd0 : p /ₘ (X - C x) ≠ 0
wf : (p /ₘ (X - C x)).degree < p.degree
t : Multiset R
htd : ↑t.card ≤ (p /ₘ (X - C x)).degree
htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))
hdeg : (X - C x).degree ≤ p.degree
hdiv0 : p /ₘ (X - C x) ≠ 0
a : R
⊢ count a (x ::ₘ t) = rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ map (iterateFrobenius R p 0) ((expand R (p ^ 0)) f) = f ^ p ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial.zero
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
b : R
⊢ (monomial (0 + n - 1)) (a * (b * ↑0)) + (monomial (0 + n - 1)) (a * (b * ↑n)) =
    (monomial (0 - 1 + n)) (a * (b * ↑0)) + (monomial (0 + (n - 1))) (a * (b * ↑n))

Tactic:
| zero =>

Goal state after: