mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ i,
        C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) i.castSucc) *
          X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i.castSucc +
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) (Fin.last n)

Tactic:
simp only [Fin.strictMono_castSucc.injective.extend_apply]

Goal state after:
case succ.refine_3
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
⊢ f =
    ∑ x_1, C (x x_1) * X ^ k x_1 +
      C (Function.extend Fin.castSucc x (fun x ↦ f.leadingCoeff) (Fin.last n)) *
        X ^ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) (Fin.last n)
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: n m : ℕ
h₀ : m ≠ 0
h : m < n.minFac
⊢ n.Coprime m

Tactic:
rw [← not_not (a := n.Coprime m), Prime.not_coprime_iff_dvd]
  push Not
  exact fun p hp hn hm ↦
    ((le_of_dvd (by lia) hm).trans_lt <| h.trans_le <| minFac_le_of_dvd hp.two_le hn).false

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

Goal state before:
pp: p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a ^ 1 ∧ True

Tactic:
_root_.and_true,

Goal state after:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = a ^ 1
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (map g (t :: ys_hd :: (tail✝ ++ ts)))

Tactic:
apply H

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.H
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
a : List α
⊢ g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)

Tactic:
apply H

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Subalgebra R A
r : R
⊢ (algebraMap R A) r ∈ star S.carrier

Tactic:
simpa only [Set.mem_star, Subalgebra.mem_carrier, ← algebraMap_star_comm] using
          S.algebraMap_mem (star r)

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f^[m] n x

Tactic:
rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
  exact hf.isFixedPt.iterate m

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
g : α → α
hco : Function.Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x

Tactic:
exact hfg.left_of_comp hg

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
n : ℕ
⊢ f^[n + minimalPeriod f x] x = f^[n] x

Tactic:
rw [iterate_add_apply]
  congr
  exact isPeriodicPt_minimalPeriod f x

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
rcases m with e | m

Goal state after:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicOrbit f x

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ x ∈ periodicOrbit f x

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d d' : α
x_mem : x ∈ xs.dropLast
⊢ xs.nextOr x d = xs.nextOr x d'

Tactic:
by
  induction xs with
  | nil => cases x_mem
  | cons y ys IH => ?_
  rcases ys with - | ⟨z, zs⟩
  · simp at x_mem
  by_cases h : x = y
  · rw [h, nextOr_self_cons_cons, nextOr_self_cons_cons]
  · rw [nextOr, nextOr, IH]
    simpa [h] using x_mem

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : x = y
⊢ x ∈ y :: z :: zs

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(QuotientGroup.mk ⁻¹' QuotientGroup.mk '' t)

Tactic:
rw [QuotientGroup.preimage_image_mk]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ ↑(t * ↑s) ≃ ↑(⋃ x, (fun x_1 ↦ x_1 * ↑x) ⁻¹' t)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x y : α
s : List α
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

Tactic:
induction s

Goal state after:
case nil
α : Type u_1
x y : α
⊢ take 2 [x, y].permutations = [[x, y], [y, x]]

case cons
α : Type u_1
x y head✝ : α
tail✝ : List α
tail_ih✝ : take 2 (x :: y :: tail✝).permutations = [x :: y :: tail✝, y :: x :: tail✝]
⊢ take 2 (x :: y :: head✝ :: tail✝).permutations = [x :: y :: head✝ :: tail✝, y :: x :: head✝ :: tail✝]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s

Tactic:
induction s

Goal state after:
case nil
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {p : ℕ}, p ∈ n.primeFactorsList → Prime p

Tactic:
by
  match n with
  | 0 => simp
  | 1 => simp
  | k + 2 =>
      intro p h
      let m := minFac (k + 2)
      have : (k + 2) / m < (k + 2) := factors_lemma
      have h₁ : p = m ∨ p ∈ primeFactorsList ((k + 2) / m) :=
        List.mem_cons.1 (by rwa [primeFactorsList] at h)
      exact Or.casesOn h₁ (fun h₂ => h₂.symm ▸ minFac_prime (by simp)) prime_of_mem_primeFactorsList

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nat.card ↥H * H.index = Nat.card G

Tactic:
rw [← relIndex_bot_left, ← index_bot]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⊥.relIndex H * H.index = ⊥.index
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
⊢ ringChar (ZMod n) = n

Tactic:
ringChar.eq_iff

Goal state after:
n : ℕ
⊢ CharP (ZMod n) n
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
m : ℕ
hlt : 0 < m
hle : m ≤ H.index
he : a ^ m ∈ H
k : ℕ
hn : ∀ (m_1 : ℕ), 0 < m_1 → m_1 ≤ H.index → m_1 ∣ m * k
⊢ (a ^ m) ^ k ∈ H

Tactic:
exact pow_mem he _

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'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card ((G ⧸ H) × G' ⧸ K)

Tactic:
exact Nat.card_congr (QuotientGroup.prodEquiv H K)

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

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

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

Goal state before:
pp: case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(↑n).val + ↑p * (n / ↑p)

Tactic:
rw [val_intCast, Int.emod_add_mul_ediv]

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

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

Tactic:
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
  induction n with
  | zero => simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]
  | succ n ih =>
    simp only [Nat.even_add_one, geom_sum_succ]
    split_ifs at ih ⊢ with h
    · rw [le_add_iff_nonneg_left]
      exact mul_nonneg_of_nonpos_of_nonpos hx0 ih
    · grw [← hx]
      gcongr
      simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

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

Goal state before:
pp: a : ℤ
⊢ ↑a.natAbs = ↑(a.natAbs.gcd 0)

Tactic:
rw [Nat.gcd_zero_right]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.2 ∈ n.divisors

Tactic:
simp [Dvd.intro_left _ h.1, h.2]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors) ↔
    a✝ ∈ n.divisorsAntidiagonal

Tactic:
← map_div_right_divisors,

Goal state after:
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors) ↔
    a✝ ∈ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 = ∑ x ∈ (n + 1 + 1).properDivisors, x

Tactic:
rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
        (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]

Goal state after:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k → ∃ j, ∃ (_ : j < k), x = p ^ j

pp: case mpr
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ j, ∃ (_ : j < k), x = p ^ j) → (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k

Tactic:
· rintro ⟨⟨j, hjk, rfl⟩, hlt⟩
    exact ⟨j, (Nat.pow_lt_pow_iff_right pp.one_lt).mp hlt, rfl⟩

Goal state after:
case mpr
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ j, ∃ (_ : j < k), x = p ^ j) → (∃ k_1 ≤ k, x = p ^ k_1) ∧ x < p ^ k
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

Tactic:
← map_div_right_divisors,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ map { toFun := fun d ↦ (d, n / d), inj' := ⋯ } n.divisors, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
n : ℕ
IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n
⊢ 4 ^ n < n * n.centralBinom
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
· rw [digitsAux]

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

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

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, m ≠ 0 → (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1
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

Tactic:
simp_all [ofDigits_lt_base_pow_length']

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

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

Tactic:
simp_all [ofDigits_lt_base_pow_length']

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

Goal state before:
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:
simp_all [ofDigits_lt_base_pow_length']

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

Goal state before:
pp: case inl.inr
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)

Goal state after:
case e'_2.h
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

case e'_2.a
p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

case e'_3
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
simp only [toDigitsCore]

Goal state after:
case succ
b f : ℕ
ih : ∀ (n e : ℕ), 0 < e → n < b ^ e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e
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 : ℕ
hx : IsOfFinOrder x
⊢ Group ↥(powers x)

Tactic:
obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec

Goal state after:
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 : ℕ
hx✝ : IsOfFinOrder x
hpos : 0 < ⋯.choose
hx : x ^ ⋯.choose = 1
⊢ Group ↥(powers x)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / p ^ (a * b).factorization p = a / p ^ a.factorization p * (b / p ^ b.factorization p)

Tactic:
simp only [ordProj_mul p ha hb]

Goal state after:
a b p : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ a * b / (p ^ a.factorization p * p ^ b.factorization p) = a / p ^ a.factorization p * (b / p ^ b.factorization p)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ p ^ k * m / p ^ (p ^ k * m).factorization p = m

Tactic:
rw [ordCompl_self_pow_mul m k hp]

Goal state after:
m k p : ℕ
hp : Prime p
hm : ¬p ∣ m
⊢ m / p ^ m.factorization p = m
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℕ
⊢ a ^ (n % orderOf a) = a ^ (n % card G)

Tactic:
← Nat.mod_mod_of_dvd n orderOf_dvd_card,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℕ
⊢ a ^ (n % card G % orderOf a) = a ^ (n % card G)
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ (single g 1 * (x /ᵒᶠ g)).coeff (g + d) + (x %ᵒᶠ g).coeff (g + d) = x.coeff (g + d)

Tactic:
coeff_modOf_self_add,

Goal state after:
case inl
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g d : G
⊢ (single g 1 * (x /ᵒᶠ g)).coeff (g + d) + 0 = x.coeff (g + d)
Module: Mathlib.Data.Nat.Factorization.Basic

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

Tactic:
induction N with

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:
simp [pow_zero]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ ∀ x ∈ f.support, (if p * x = n then f.coeff x else 0) = 0

Tactic:
intro k _

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ f.support
⊢ (if p * k = n then f.coeff k else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (p * n) = f.coeff n

Tactic:
rw [mul_comm, coeff_expand_mul hp]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ p q : R[X]
⊢ ((p + q).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) =
    (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) + q.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)

Tactic:
by
    rw [sum_add_index] <;>
      simp only [add_mul, forall_const, map_add, zero_mul, map_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 %ₘ p = 0

Tactic:
grind [modByMonic, divModByMonicAux]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (algebraMap A B) ((aeval x) p) = 0 ↔ (aeval x) p = 0

Tactic:
← (algebraMap A B).map_zero,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
h : Function.Injective ⇑(algebraMap A B)
⊢ (algebraMap A B) ((aeval x) p) = (algebraMap A B) 0 ↔ (aeval x) p = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i = C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i

Tactic:
Nat.descFactorial_eq_factorial_mul_choose

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i = C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i = C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i

Tactic:
Nat.descFactorial_eq_factorial_mul_choose

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i = C ((k ! * (i + k).choose k) • p.coeff (i + k)) * X ^ i
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ C ↑n * q ^ (n - 1) * derivative q * r + q ^ n * derivative r

Tactic:
exact (((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = ((X.comp (X + C t) - (C t).comp (X + C t)) ^ m * g.comp (X + C t)).trailingCoeff

Tactic:
X_comp,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = ((X + C t - (C t).comp (X + C t)) ^ m * g.comp (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: ι : Sort u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
s : Set α
⊢ (∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i) → s ∈ ⨅ i, f i

Tactic:
rintro ⟨t, ht, rfl⟩

Goal state after:
ι : Sort u_2
inst✝ : Finite ι
α : Type u_3
f : ι → Filter α
t : ι → Set α
ht : ∀ (i : ι), t i ∈ f i
⊢ ⋂ i, t i ∈ ⨅ i, f i
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ f ×ˢ ⨅ i, g i = ⨅ i, f ×ˢ g i

Tactic:
simp only [prod_eq_inf, comap_iInf, inf_iInf]

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ a \ ∂ a = ￢￢a

Tactic:
by
  rw (occs := [1]) [← hnot_hnot_sup_boundary a]
  rw [sup_sdiff_distrib, sdiff_self, sup_bot_eq, hnot_sdiff_comm,
    hnot_boundary, top_sdiff']

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d

Tactic:
exact Filter.prod_mono hf hg

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
c : R
⊢ derivative ((X - C c) ^ 2) = C 2 * (X - C c)

Tactic:
by
  rw [derivative_sq, derivative_X_sub_C, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ n.descFactorial n • 1 = ↑n !

Tactic:
nsmul_one,

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ ↑(n.descFactorial n) = ↑n !