mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
⊢ RingHom.ker (mapRingHom f) = map C (RingHom.ker f)

Tactic:
by
  ext
  simp only [RingHom.mem_ker, coe_mapRingHom]
  rw [mem_map_C_iff, Polynomial.ext_iff]
  simp [RingHom.mem_ker]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ (p * X ^ (n - m)).degree ≤ ↑n

Tactic:
refine le_trans (degree_mul_le _ _) ?_

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ p.degree + (X ^ (n - m)).degree ≤ ↑n
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R A

Tactic:
rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)

Tactic:
by
  apply toSubsemiring_injective
  simp_rw [Algebra.adjoin, unop_toSubsemiring, Subsemiring.unop_closure, Set.preimage_union]
  congr with x
  simp

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → FiniteType R S

Tactic:
rintro ⟨ι, hfintype, f, hsur⟩
    let : Fintype ι := hfintype
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mk
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g ⇑f
x✝ : R ⧸ ker f
x : R
⊢ f.kerLift ((⇑(Ideal.Quotient.mk (ker f)) ∘ g) (f.kerLift (Quot.mk (⇑(Submodule.quotientRel (ker f))) x))) =
    f.kerLift (Quot.mk (⇑(Submodule.quotientRel (ker f))) x)

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, kerLift_mk,
        Function.comp_apply, hf (f x)]

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

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑a * a.gcdA b + ↑b * a.gcdB b ≡ 1 [ZMOD ↑b]

Tactic:
← Nat.gcd_eq_gcd_ab,

Goal state after:
a b : ℕ
hab : a.Coprime b
hgcd : a.gcd b = 1
⊢ ↑(a.gcd b) ≡ 1 [ZMOD ↑b]
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
hIJ : I ≤ J
x : R
⊢ x ∈ J ⊔ I ↔ x ∈ J

Tactic:
sup_eq_left.mpr hIJ

Goal state after:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
hIJ : I ≤ J
x : R
⊢ x ∈ J ↔ x ∈ J
Module: Mathlib.Data.Fintype.List

Goal state before:
pp: α : Type u_1
l : Finset α
h_nodup : l.val.Nodup
⊢ l.val.lists.Nodup

Tactic:
← Finset.coe_toList l,

Goal state after:
α : Type u_1
l : Finset α
h_nodup : (↑l.toList).Nodup
⊢ l.val.lists.Nodup
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : α → α
x : α
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
by_cases hx : x ∈ periodicPts f
  · have hx' := minimalPeriod_pos_of_mem_periodicPts hx
    have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
    rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
    refine ⟨?_, fun H => ⟨?_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
    · rintro ⟨hr, H⟩ n hn
      rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
      · rwa [hM', hM, iterate_minimalPeriod]
      · exact H _ hM'
    · rw [iterate_zero_apply]
      nth_rw 3 [← @iterate_minimalPeriod α f x]
      nth_rw 2 [← hM]
      exact H _ (Nat.lt_succ_self _)
  · rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_notMem_periodicPts hx]
    simp

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Tactic:
by
  apply h.minimalPeriod_of_comp_dvd_mul.antisymm
  suffices ∀ {f g : α → α},
      Commute f g →
        Coprime (minimalPeriod f x) (minimalPeriod g x) →
          minimalPeriod f x ∣ minimalPeriod (f ∘ g) x from
    hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
  intro f g h hco
  refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd
  · exact (isPeriodicPt_minimalPeriod _ _).const_mul _
  · exact (isPeriodicPt_minimalPeriod _ _).mul_const _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
y : α
hl : l.Nodup
h✝ : (y :: l).getLast ⋯ ∈ l
h : (y :: l).getLast ⋯ ∈ y :: l
hy : (y :: l).getLast ⋯ ≠ y
H : (y :: l).getLast ⋯ ∈ (y :: l).dropLast
k : ℕ
hk : k + 1 < (y :: l).dropLast.length
hk' : (y :: l).dropLast[k + 1] = (y :: l).getLast ⋯
this : k + 1 = l.length
⊢ False

Tactic:
simp [this] at hk

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ n % (tl.length + 1) = n

Tactic:
Nat.mod_eq_of_lt hn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
hd : α
tl : List α
h : (hd :: tl).Nodup
hn✝ : n < (hd :: tl).length
hn : n < tl.length + 1
hx : (hd :: tl)[n] ∈ hd :: tl
⊢ n = n
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
l : List α
hl : l.Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ l.length

Tactic:
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)

Goal state after:
case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length

case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) l)

Tactic:
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)

Goal state after:
case h.nil
α : Type u_1
x y : α
hxy : x ≠ y
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) []
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) []
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [])

case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))
Module: Mathlib.Data.List.Prime

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
⊢ p ∈ L

Tactic:
by
  obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL
  rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]

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

Goal state before:
pp: case mp
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1

Tactic:
rcases n with (_ | _ | n)
    · exact Or.inl rfl
    · exact Or.inr rfl
    · rw [primeFactorsList] at h
      injection h

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'
⊢ f.ker.index = Nat.card ↥f.range

Tactic:
by
  rw [← MonoidHom.comap_bot, index_comap, relIndex_bot_left]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.1 = a.cast

Tactic:
cases n
  · rfl
  · simp [ZMod.cast]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.2 = a.cast

Tactic:
cases n
  · rfl
  · simp [ZMod.cast]

Goal state after:
Module: Mathlib.GroupTheory.Index

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

Tactic:
rw [isFiniteRelIndex_iff_relIndex_ne_zero]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
h : K ≤ L
inst✝ : H.IsFiniteRelIndex L
⊢ H.relIndex K ≠ 0
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
Nat.mod_add_div

Goal state after:
case mp
p n : ℕ
inst✝ : NeZero p
⊢ n = n
Module: Mathlib.Data.ZMod.Basic

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

Tactic:
ZMod.val_add,

Goal state after:
n : ℕ
a b : ZMod n
h : a.val + b.val < n
this : NeZero n
⊢ (a.val + b.val) % n = a.val + b.val
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ ↑u * (↑u)⁻¹ = 1

Tactic:
rw [inv_coe_unit, u.mul_inv]

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

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

Tactic:
rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert]

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

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y

Tactic:
exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h

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

Goal state before:
pp: n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a * 2 = 0 ↔ a = 0

Tactic:
← @Nat.cast_two (ZMod n),

Goal state after:
n : ℕ
hn : Nat.Coprime 2 n
a : ZMod n
⊢ a * ↑2 = 0 ↔ a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
cases hb

Goal state after:
case pos.refl
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val 0 ≤ a.val
⊢ (a - 0).val = a.val - val 0
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1

Tactic:
Nat.mod_add_div

Goal state after:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ n✝ + 1 = n✝ + 1
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case inl.cons
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []},
    tl.getLast h_nonempty ≠ 0 →
      (∀ l ∈ tl, l < p) → (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ i ∈ range (hd :: tl).length, ofDigits p (hd :: tl) / p ^ i.succ = ofDigits p (hd :: tl) - (hd :: tl).sum

Tactic:
simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a : α
ha : FiniteMultiplicity a 1
⊢ multiplicity a 1 = 0

Tactic:
simp [ha.multiplicity_eq_iff, ha.not_dvd_of_one_right]

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

Goal state before:
pp: case ind.succ
b n : ℕ
IH : ∀ m ≤ n, ∀ (i : ℕ), ((b + 2).digits m)[i]?.getD 0 = m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ ((b + 2).digits n.succ)[i + 1]?.getD 0 = n.succ / (b + 2) ^ (i + 1) % (b + 2)

Tactic:
simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]

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

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

Tactic:
rw [count_eq_zero_of_not_mem (mt prime_of_mem_primeFactorsList pp)]

Goal state after:
n p : ℕ
hn0 : n > 0
pp : ¬Prime p
⊢ 0 = n.factorization p
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
⊢ n.factorization p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0

Tactic:
simp_rw [← notMem_support_iff, support_factorization, mem_primeFactors, not_and_or, not_ne_iff]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n

Tactic:
Nat.mod_add_div

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ n = x ^ n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
⊢ p ^ n.factorization p ∣ n

Tactic:
if hp : p.Prime then ?_ else simp [hp]
  rw [← primeFactorsList_count_eq]
  apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)
  rw [hp.primeFactorsList_pow, List.subperm_ext_iff]
  intro q hq
  simp [List.eq_of_mem_replicate hq]

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

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

Tactic:
rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]

Goal state after:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d ∣ n / p ^ n.factorization p

Tactic:
← factorization_le_iff_dvd hd0 (ordCompl_pos p hn0).ne',

Goal state after:
p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
⊢ d.factorization ≤ (n / p ^ n.factorization p).factorization
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: p d n : ℕ
hdn : d ∣ n
hpd : ¬p ∣ d
hn0 : ¬n = 0
hd0 : ¬d = 0
q : ℕ
hqp : q = p
⊢ d.factorization q ≤ (Finsupp.erase p n.factorization) q

Tactic:
simp [factorization_eq_zero_iff, hqp, hpd]

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p + p * (n / p))

Tactic:
Nat.mod_add_div

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ n
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
h : y ∈ zpowers x
⊢ orderOf y ∣ orderOf x

Tactic:
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h
  rw [orderOf_dvd_iff_pow_eq_one]
  exact zpow_pow_orderOf

Goal state after:
Module: Mathlib.Algebra.CharP.Lemmas

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p + p * (n / p))

Tactic:
Nat.mod_add_div

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ n
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:
simp [hp.emultiplicity_one]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x y, 1 = k * x + ↑(orderOf g) * y

Tactic:
← Int.sub_eq_iff_eq_add',

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x y, 1 - k * x = ↑(orderOf g) * y
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: ⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n

Tactic:
have h2 := prime_two.prime

Goal state after:
h2 : _root_.Prime 2
⊢ ∀ {n : ℕ}, n ≠ 0 → emultiplicity 2 n ! < ↑n
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case mpr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), Prime p → padicValNat p a = padicValNat p b) → a = b

Tactic:
· intro h
    refine eq_of_factorization_eq ha hb fun p => ?_
    by_cases pp : p.Prime
    · simp [factorization_def, pp, h p pp]
    · simp [factorization_eq_zero_of_not_prime, pp]

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

Goal state before:
pp: case neg.true
h2 : _root_.Prime 2
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
hn : ¬n = 0
this : emultiplicity 2 (2 * n)! < ↑(2 * n)
h : bit true n ≠ 0
⊢ emultiplicity 2 (bit true n)! < ↑(bit true n)

Tactic:
suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
        simpa [emultiplicity_mul, h2, prime_two, bit, factorial]
      rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
      refine this.trans ?_
      exact mod_cast lt_succ_self _

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

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

Tactic:
Finset.filter_insert

Goal state after:
case succ
n N : ℕ
ih : #({k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}) = N / n
⊢ #(if N + 1 ≠ 0 ∧ n ∣ N + 1 then insert (N + 1) ({k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k})
      else {k ∈ Finset.range (N + 1) | k ≠ 0 ∧ n ∣ k}) =
    (N + 1) / n
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
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
⊢ 1 ∈ S ^ card G

Tactic:
obtain ⟨a, ha⟩ := hS

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
a : G
ha : a ∈ S
⊢ 1 ∈ S ^ card G
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w✝ : R
⊢ (aeval ((algebraMap R S) w✝)) p ≠ 0

Tactic:
rw [aeval_algebraMap_apply_eq_algebraMap_eval]

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
w✝ : R
⊢ (algebraMap R S) (eval w✝ p) ≠ 0
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
derivative_apply

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)).coeff n = p.coeff (n + 1) * (↑n + 1)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝

Tactic:
by
    simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]
    exact id

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.Monic
⊢ q ∣ p %ₘ q - p

Tactic:
simp [modByMonic_eq_sub_mul_div]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree ≤ (q * (p /ₘ q)).degree

Tactic:
by
        rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]
        exact Nat.le_add_right _ _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (derivative p)

Tactic:
derivative_apply

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ((map f p).sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)) = map f (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1))
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (derivative p).degree ≤ ↑(p.natDegree - 1)

Tactic:
derivative_apply

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ (p.sum fun n a ↦ C (a * ↑n) * X ^ (n - 1)).degree ≤ ↑(p.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
p : R[X]
⊢ a - b ∣ eval a p - eval b p

Tactic:
suffices X - C b ∣ p - C (p.eval b) by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C]
      using (_root_.map_dvd (evalRingHom a)) this
  simp [dvd_iff_isRoot]

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

Goal state before:
pp: α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
⊢ ∀ (i : ↑I), V i ∈ s ↑i

Tactic:
rintro i

Goal state after:
α : Type u
ι : Type u_2
s : ι → Filter α
U : Set α
I : Set ι
Ifin : I.Finite
σ : ↑{i | i ∈ I} → Set (Set α)
σfin : ∀ (i : ↑{i | i ∈ I}), (σ i).Finite
σsub : ∀ (i : ↑{i | i ∈ I}), σ i ⊆ (s ↑i).sets
tsub : ⋃ i, σ i ⊆ ⋃ i, (s i).sets
tfin : (⋃ i, σ i).Finite
tinter : ⋂ i, ⋂₀ σ i ⊆ U
V : ↑{i | i ∈ I} → Set α := fun i ↦ U ∪ ⋂₀ σ i
hV : V = fun i ↦ U ∪ ⋂₀ σ i
i : ↑I
⊢ V i ∈ s ↑i
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
hVf : ∀ (i : ι), ∃ t ∈ f i, eval i ⁻¹' t ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i

Tactic:
choose t htf htV using hVf

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
I : Set ι
If : I.Finite
V : ι → Set ((i : ι) → α i)
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
htV : ∀ (i : ι), eval i ⁻¹' t i ⊆ V i
⊢ ∃ I_1, I_1.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ ⋂ a ∈ I_1, eval a ⁻¹' t a ⊆ ⋂ i ∈ I, V i