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

Goal state before:
pp: case neg.inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

Tactic:
have hd₁ : n < ((X - C x) * P).eraseLead.natDegree := by
      linarith [natDegree_eraseLead_add_one h₂]

Goal state after:
case neg.inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).natDegree - 1 - 1 < n

Tactic:
simpa [h₁, hdP] using! hn

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
rw [hpi]; simpa

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : MonicDegreeEq R n
⊢ (↑p).coeff n ≠ 0

Tactic:
by simp [p.2.1]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
induction n generalizing f with
  | zero => exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
  | succ n hn =>
    intro h
    obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
    have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
    refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
    · intro i j hij
      have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_ofPred_eq]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
      obtain ⟨i, rfl⟩ := hi
      rw [Fin.strictMono_castSucc.injective.extend_apply]
      by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
      · obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
      · rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finsetSum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim
    · intro i
      by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
      · obtain ⟨i, rfl⟩ := hi
        rw [Fin.strictMono_castSucc.injective.extend_apply]
        exact hx i
      · rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero
    · rw [Fin.sum_univ_castSucc]
      simp only [Fin.strictMono_castSucc.injective.extend_apply]
      rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
      all_goals exact H

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
i : ℕ
⊢ ↑((restriction 1).coeff i) = ↑(coeff 1 i)

Tactic:
rw [coeff_restriction', coeff_one, coeff_one]; split_ifs <;> rfl

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

Tactic:
have : m ∈ closure S := hS.symm ▸ mem_top _
    refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval fun s ↦ of' R M ↑s)

Tactic:
intro f
  induction f using induction_on with
  | of m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩
  | add f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | smul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

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

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
⊢ d ∈ F.coeff.support →
    (natDegree ∘ fun i ↦ (fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) i (F.coeff i)) d ≤ m * n

Tactic:
hd

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ (natDegree ∘ fun i ↦ (fun s a ↦ (algebraMap R R[X]) a * s.prod fun n e ↦ f n ^ e) i (F.coeff i)) d ≤ m * n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ p ∈ I

Tactic:
rw [as_sum p]
  suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
    exact Submodule.sum_mem I this
  intro m _
  rw [← mul_one (coeff m p), ← C_mul_monomial]
  suffices C (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
  simpa [Ideal.mem_comap] using hcoe m

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
⊢ a ≡ b - n * c [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  rw [← modEq_add_modulus_mul_iff, sub_add_cancel]

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ ¬Prime n ↔ ∃ a b, a < n ∧ b < n ∧ a * b = n

Tactic:
by
  rw [prime_iff_not_exists_mul_eq, and_iff_right h, Classical.not_not]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ f^[m] x = x

Tactic:
convert! (hm.apply_iterate ((n / r + 1) * r - n)).eq

Goal state after:
case e'_2
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)

case e'_3
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ x = f^[(n / r + 1) * r - n] (f^[n] x)
Module: Mathlib.Data.List.Cycle

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

Tactic:
· exact if_neg h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
⊢ d ∈ xs' → xs.nextOr x d ∈ xs'

Tactic:
hd

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
xs' : List α
hxs' : ∀ x ∈ xs, x ∈ xs'
hd : d ∈ xs'
⊢ xs.nextOr x d ∈ xs'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
y z : α
xs : List α
x : α
h : x ∈ y :: z :: xs
hx : ¬x = y
⊢ x ∈ z :: xs

Tactic:
by simpa [hx] using h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
ha : a ∈ l
ha₀ : a ≠ l.head ⋯
this : idxOf a l = (idxOf a l.tail).succ
i : ℕ
hi : i < [l.prev a ha, a].length
hi₁ : ¬i = 1
⊢ l[i + (idxOf a l - 1)]? = some [l.prev a ha, a][i]

Tactic:
grind [prev_eq_getElem?_idxOf_pred_of_ne_head]

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

Goal state before:
pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ hd ∉ tl) ∧ hd' ∉ tl ∧ tl.Nodup
⊢ ¬hd = hd'

Tactic:
exact hl.left.left

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

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

Tactic:
by
  induction s with
  | nil => exact fun _ ↦ Cycle.Chain.nil r
  | cons a l => ?_
  intro hs
  have Ha : a ∈ (a :: l : Cycle α) := by simp
  have Hl : ∀ {b} (_hb : b ∈ l), b ∈ (a :: l : Cycle α) := @fun b hb => by simp [hb]
  rw [Cycle.chain_coe_cons]
  apply Pairwise.isChain
  rw [pairwise_cons]
  exact
    ⟨fun b hb => by grind,
      pairwise_append.2
        ⟨pairwise_of_forall_mem_list fun b hb c hc => hs b (Hl hb) c (Hl hc),
          pairwise_singleton r a, fun b hb c hc => by grind⟩⟩

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

Goal state before:
pp: case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ b.primeFactorsList.prod

Tactic:
← hu1.prod_eq,

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ a ^ (n + 1) ∣ u.prod
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList

Tactic:
exact mem_primeFactorsList_mul_left hpb ha

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.FiniteIndex
⊢ H.IsFiniteRelIndex K

Tactic:
rw [← isFiniteRelIndex_top_iff] at h

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsFiniteRelIndex ⊤
⊢ H.IsFiniteRelIndex K
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
refine ⟨n / p, ?_⟩

Goal state after:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = (↑n).val + p * (n / p)
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
refine ⟨n / p, ?_⟩

Goal state after:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(↑n).val + ↑p * (n / ↑p)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ (a.val + b.val) % n = a.val + b.val

Tactic:
Nat.mod_eq_of_lt h

Goal state after:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ a.val + b.val = a.val + b.val
Module: Mathlib.Algebra.Polynomial.Cardinal

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ #R[X] ≤ max #R ℵ₀

Tactic:
cases subsingleton_or_nontrivial R
  · exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)
  · exact cardinalMk_eq_max.le

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ 1 < n / m

Tactic:
rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.1 ∈ n.divisors

Tactic:
rw [mem_divisorsAntidiagonal] at h

Goal state after:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.1 ∈ n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.2 ∈ n.divisors

Tactic:
rw [mem_divisorsAntidiagonal] at h

Goal state after:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.2 ∈ n.divisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.primeFactors = {p ∈ n.divisors | Prime p}

Tactic:
by
  grind

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

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

Tactic:
exact Nat.add_le_add (choose_succ_le_two_pow n k) (choose_succ_le_two_pow n (k + 1))

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

Goal state before:
pp: n a : ℕ
h : a < n
⊢ a % n = a

Tactic:
Nat.mod_eq_of_lt h

Goal state after:
n a : ℕ
h : a < n
⊢ a = a
Module: Mathlib.Data.Nat.Choose.Central

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

Tactic:
exact False.elim ((not_lt.2 n_big) hn)

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

Goal state before:
pp: b x : ℕ
hx : x.succ ≠ 0
hxb : x.succ < b
⊢ b.digits x.succ = [x.succ]

Tactic:
rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩

Goal state after:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (b + succ 1).digits x.succ = [x.succ]
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.val ^ (m + 1) % n = a.val ^ (m + 1)

Tactic:
Nat.mod_eq_of_lt h

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 + 1) = a.val ^ (m + 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case cons.cons
b hd₁ hd₂ : ℕ
tl₂ : List ℕ
ih₂ :
  ∀ (tl₁ : List ℕ),
    (∀ {l2 : List ℕ},
        tl₁.length = l2.length →
          ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)) →
      (hd₁ :: tl₁).length = tl₂.length →
        ofDigits b (hd₁ :: tl₁) + ofDigits b tl₂ = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) tl₂)
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ},
    tl₁.length = l2.length → ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = (hd₂ :: tl₂).length
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b (hd₂ :: tl₂) =
    ofDigits b (List.zipWith (fun x1 x2 ↦ x1 + x2) (hd₁ :: tl₁) (hd₂ :: tl₂))

Tactic:
| cons hd₂ tl₂ ih₂ =>

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

Goal state before:
pp: case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
⊢ d ∈ (b + 2).digits n → d < b + 2

Tactic:
hd

Goal state after:
case ind
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
hd : d ∈ (b + 2).digits n
⊢ d < b + 2
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization
⊢ False

Tactic:
simpa [hp.factorization] using h p

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

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList

Tactic:
hp.primeFactorsList_pow,

Goal state after:
n p : ℕ
hp : Prime p
⊢ replicate (count p n.primeFactorsList) p <+~ n.primeFactorsList
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: 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 ^ l.pred.succ

Tactic:
Nat.succ_pred hl

Goal state after:
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 ^ l
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:
· rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]

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: n p : ℕ
hp : Prime p
hn : n ≠ 0
⊢ ¬p ∣ n / p ^ n.factorization p

Tactic:
rw [Nat.Prime.dvd_iff_one_le_factorization hp (ordCompl_pos p hn).ne']
  rw [Nat.factorization_div (Nat.ordProj_dvd n p)]
  simp [hp.factorization]

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

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

Tactic:
by
  nth_rewrite 2 [← factorization_choose_prime_pow_add_factorization hp hkn hk0]
  rw [Nat.add_sub_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
a : G
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
by
  by_cases ha : IsOfFinOrder a
  · exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp
  · have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : RightCancelMonoid G
a : G
⊢ Nat.card ↥(powers a) = orderOf a

Tactic:
by
  by_cases ha : IsOfFinOrder a
  · exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp
  · have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
z : ℤ
⊢ x ^ (z % ↑(orderOf x) + ↑(orderOf x) * (z / ↑(orderOf x))) = x ^ z

Tactic:
rw [Int.emod_add_mul_ediv]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : (expand R n) g = (expand R n) g'
k : ℕ
⊢ g.coeff k = g'.coeff k

Tactic:
← coeff_expand_mul hn,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
hn : 0 < n
g g' : R[X]
H : (expand R n) g = (expand R n) g'
k : ℕ
⊢ ((expand R n) g).coeff (k * n) = g'.coeff k
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

Tactic:
← smul_eq_C_mul,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (a • p) = a • (⇑derivative)^[k] p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case neg
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
ha : ¬a = x
⊢ count a (x ::ₘ t) = 0 + count a t

Tactic:
rw [count_cons_of_ne ha, zero_add]

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:
by
          intro a
          conv_rhs => rw [← mul_divByMonic_eq_iff_isRoot.mpr hx]
          rw [rootMultiplicity_mul (mul_ne_zero (X_sub_C_ne_zero x) hdiv0),
            rootMultiplicity_X_sub_C, ← htr a]
          split_ifs with ha
          · rw [ha, count_cons_self, add_comm]
          · rw [count_cons_of_ne ha, zero_add]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : p = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree

pp: case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree

Tactic:
· convert! hq
    simp [hp, cancelLeads]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
p q : R[X]
comm : p.leadingCoeff * q.leadingCoeff = q.leadingCoeff * p.leadingCoeff
h : p.natDegree ≤ q.natDegree
hq : 0 < q.natDegree
hp : ¬p = 0
⊢ (p.cancelLeads q).natDegree < q.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
⊢ p %ₘ q = q * (r - p /ₘ q)

Tactic:
rw [modByMonic_eq_sub_mul_div, mul_sub, ← hr]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ C (s • 1) * eval₂ C q p = s • eval₂ C q p

Tactic:
← smul_eq_C_mul,

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ (s • 1) • eval₂ C q p = s • eval₂ C q p
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C (((⇑derivative)^[k] p).coeff i) * X ^ i = C ((i + k).descFactorial 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 : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Goal state after:
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 = k ! • (C ((i + k).choose k • p.coeff (i + k)) * X ^ i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
hp : p ≠ 0
a : R
⊢ ∃ q, p = (X - C a) ^ multiplicity (X - C a) p * q ∧ ¬X - C a ∣ q

Tactic:
apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

Goal state after: