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

Goal state before:
pp: case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ (n ^ (n✝ + 1)).primeFactors = n.primeFactors

Tactic:
primeFactors_pow_succ

Goal state after:
case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ n.primeFactors = n.primeFactors
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ ↑↑a.val = a

Tactic:
rw [Int.cast_natCast, natCast_zmod_val]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ (-1).cast = ↑(n + 1) - 1

Tactic:
rw [← natCast_val, val_neg_one, Nat.cast_succ, add_sub_cancel_right]

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

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

Tactic:
intro a b h

Goal state after:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ a = b
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #(Ico 1 (n + 1)) = n

Tactic:
rw [card_Ico, add_tsub_cancel_right]

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:
Nat.lt_div_iff_mul_lt' h_dvd,

Goal state after:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ m * 1 < n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n x : ℕ
h : n.gcd x = 1
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
Nat.gcd_rec

Goal state after:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

pp: case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd

Tactic:
· rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
    rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
    exact ⟨rfl, hn⟩

Goal state after:
case mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
u : (ZMod n)ˣ
⊢ (↑u).val.Coprime n

Tactic:
by
  rcases n with - | n
  · rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp
  apply Nat.coprime_of_mul_modEq_one ((u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1)).val
  have := Units.ext_iff.1 (mul_inv_cancel u)
  rw [Units.val_one] at this
  rw [← natCast_eq_natCast_iff, Nat.cast_one, ← this]; clear this
  rw [← natCast_zmod_val ((u * u⁻¹ : Units (ZMod (n + 1))) : ZMod (n + 1))]
  rw [Units.val_mul, val_mul, natCast_mod]

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

Goal state before:
pp: case succ.succ.inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : 0 < x + 1
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
· exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'

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

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = if a = 0 then 0 else n - a.val

Tactic:
rw [if_neg h]

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : ¬a = 0
⊢ (n - a.val) % n = n - a.val
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: n : ℕ
⊢ Coprime 1 n

Tactic:
exact coprime_one_left n

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

Goal state before:
pp: case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (b + 2).digitsAux ⋯ (x + (b + 2) * (n✝ + 1)) = x :: (b + 2).digitsAux ⋯ (n✝ + 1)

Tactic:
rw [digitsAux_def]

Goal state after:
case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)

case succ.w
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n✝ + 1)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n✝ : ℕ
hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0
⊢ (x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n✝ + 1)

Tactic:
congr
    · simp [Nat.add_mod, mod_eq_of_lt hxb]
    · simp [add_mul_div_left, div_eq_of_lt hxb]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : NonAssocSemiring R
f g : ZMod n →+* R
⊢ f = g

Tactic:
by
  ext a
  obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a
  let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
  let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
  change φ k = ψ k
  rw [φ.ext_int ψ]

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ padicValNat 0 n < n

Tactic:
| =>

Goal state after:
p n : ℕ
hn : n ≠ 0
⊢ padicValNat 0 n < n
Module: Mathlib.Data.Nat.MaxPowDiv

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

Tactic:
| =>

Goal state after:
p n : ℕ
hn : n ≠ 0
⊢ padicValNat 1 n < n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p✝ n : ℕ
hn : n ≠ 0
p : ℕ
⊢ padicValNat (p + 2) n < n

Tactic:
| =>

Goal state after:
p✝ n : ℕ
hn : n ≠ 0
p : ℕ
⊢ padicValNat (p + 2) n < n
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicValNat p p = 1

Tactic:
by
  simpa using padicValNat_base_pow hp 1

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

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0

Tactic:
by
  rcases b with (_ | _ | b)
  · cases m
    · cases hm rfl
    · simp
  · simp
  revert hm
  induction m using Nat.strongRecOn with | ind n IH => ?_
  intro hn
  by_cases! hnb : n < b + 2
  · simpa only [digits_of_lt (b + 2) n hn hnb]
  · rw [digits_getLast n (le_add_left 2 b)]
    refine IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) ?_
    rw [← pos_iff_ne_zero]
    exact Nat.div_pos hnb (zero_lt_succ (succ b))

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

Goal state before:
pp: b m : ℕ
⊢ m < (b + 2) ^ ((b + 2).digits m).length

Tactic:
convert! @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'

Goal state after:
b m : ℕ
⊢ m = ofDigits (b + 2) ((b + 2).digits m)
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:
exact False.elim (Nat.lt_irrefl 0 h_e_pos)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_6
inst✝ : DivisionMonoid G
x : G
x✝ : ∃ n, n ≠ 0 ∧ x ^ n = 1
n : ℤ
hn : n ≠ 0
hn' : x ^ n = 1
h : n = -↑n.natAbs
⊢ x ^ n.natAbs = 1

Tactic:
rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'

Goal state after:
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:
by
  obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec
  exact Submonoid.groupPowers hpos hx

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

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

Tactic:
Nat.add_sub_cancel_right

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

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

Tactic:
rcases lt_trichotomy (multiplicity p a) (multiplicity p b) with (hab | _ | hab)
  · rw [add_comm, ha.multiplicity_add_of_gt hab, min_eq_left]
    exact le_of_lt hab
  · contradiction
  · rw [hb.multiplicity_add_of_gt hab, min_eq_right]
    exact le_of_lt hab

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
by
  by_cases h0 : orderOf x = 0
  · rw [h0, coprime_zero_right] at h
    exact ⟨1, by rw [h, pow_one, pow_one]⟩
  by_cases h1 : orderOf x = 1
  · exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
  obtain ⟨m, -, h⟩ := exists_mul_mod_eq_one_of_coprime h (by lia)
  exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

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

Tactic:
rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]

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

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (⇑p.factorization + ⇑(n + 1).factorization) p) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)

Tactic:
Pi.add_apply,

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (p.factorization p + (n + 1).factorization p)) =
    ∑ x ∈ Ico 1 (p * n + 1), x.factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Factorization.Basic

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

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

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

Tactic:
· exact pos_iff_ne_zero.mp (ordCompl_pos p (pow_ne_zero k hp.ne_zero))

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

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

Goal state before:
pp: p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ∑ i ∈ Ico 1 b, (n + k) / p ^ i =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (⇑k !.factorization + ⇑n !.factorization) p

Tactic:
Pi.add_apply,

Goal state after:
p n k b : ℕ
hp : Prime p
hnb : log p (n + k) < b
h2 : (n + k).choose k * k ! * n ! = (n + k)!
⊢ ∑ i ∈ Ico 1 b, (n + k) / p ^ i =
    #({i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}) + (k !.factorization p + n !.factorization p)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsPeriodicPt (fun x_1 ↦ x * x_1) p 1 ∧ ¬IsFixedPt (fun x_1 ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1

Tactic:
isPeriodicPt_mul_iff_pow_eq_one,

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
⊢ x ^ p = 1 ∧ ¬IsFixedPt (fun x_1 ↦ x * x_1) 1 ↔ x ^ p = 1 ∧ x ≠ 1
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 = ((p ^ n).choose k).factorization p + k.factorization p - k.factorization p

Tactic:
Nat.add_sub_cancel_right

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ((p ^ n).choose k).factorization p = ((p ^ n).choose k).factorization p
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ (⇑n.succ.factorization + ⇑n !.factorization) p = 0

Tactic:
Pi.add_apply,

Goal state after:
case succ
p n✝ n : ℕ
hn : n < p → n !.factorization p = 0
h : n + 1 < p
⊢ n.succ.factorization p + n !.factorization p = 0
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ ↑i = 1

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ ↑i = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ ↑(orderOf x) ∣ ↑i ↔ x ^ (-↑i) = 1

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
x : G
i : ℕ
⊢ orderOf x ∣ i ↔ x ^ (-↑i) = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n ↦ x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
by
  refine ⟨?_, fun h n m hnm => ?_⟩
  · simp_rw [isOfFinOrder_iff_pow_eq_one]
    rintro h ⟨n, hn, hx⟩
    exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)
  rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm

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

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

Tactic:
Nat.add_sub_cancel_right

Goal state after:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k)
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
a : G
ha : a ∈ S
⊢ ?m.40 ^ card G ∈ S ^ card G

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
a : G
ha : a ∈ S
⊢ G

Tactic:
exact Set.pow_mem_pow ha

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
⊢ M (p.divX * X + C 0)

Tactic:
C_0,

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + C a)
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p.divX * X + C (p.coeff 0) = 0
wf : (p.divX * X + C (p.coeff 0)).divX.degree < (p.divX * X + C (p.coeff 0)).degree
hcp0 : p.coeff 0 = 0
⊢ M (p.divX * X + 0)
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr
a b m n : ℕ
g : ℕ := m.gcd n
m' : ℕ := m / m.gcd n
n' : ℕ := n / m.gcd n
h : (a ^ m') ^ g = (b ^ n') ^ g
coprime : m'.Coprime n'
hn : n ≠ 0
⊢ g ≠ 0

Tactic:
exact gcd_ne_zero_right hn

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : a = 0
⊢ (C 0 * X ^ (n + 1)).natDegree = 0

Tactic:
C_0,

Goal state after:
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : a = 0
⊢ (0 * X ^ (n + 1)).natDegree = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ M (C a * X ^ (n + 1))

Tactic:
C_mul_X_pow_eq_monomial

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ M ((monomial (n + 1)) a)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
x✝ : X ^ n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = X ^ n * g
⊢ f.coeff d = 0

Tactic:
simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_gt hd, IsEmpty.forall_iff]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : (X ^ n * g).coeff n = g.coeff 0
⊢ X ^ (n + 1) ∣ f

Tactic:
← hgf,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : f.coeff n = g.coeff 0
⊢ X ^ (n + 1) ∣ f
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity (X - C 0) (p.comp (X + C t))

Tactic:
C_0,

Goal state after:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity (X - 0) (p.comp (X + C t))
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = ((expand S p) (map f q)).coeff n✝

Tactic:
coeff_expand (Nat.pos_of_ne_zero hp)

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (a * ↑n) * X ^ (n - 1) = (monomial (n - 1)) (a * ↑n)

pp: case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
C_mul_X_pow_eq_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial (n - 1)) (a * ↑n) = (monomial (n - 1)) (a * ↑n)

case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : p ∣ y
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Tactic:
obtain ⟨x, rfl⟩ : p ∣ x := (Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n y : ℕ
h : p ∣ y
x : ℕ
eq : (p * x, y).1 + (p * x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)
⊢ f.coeff (p * x, y).1 * ((expand R p) g).coeff (p * x, y).2 = 0
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
n : ℕ
⊢ C 0 * X ^ (n - 1) = 0

Tactic:
C_0,

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
n : ℕ
⊢ 0 * X ^ (n - 1) = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) 0 = (Finsupp.single 0 (C r)) 0

Tactic:
| =>

Goal state after:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) 0 = (Finsupp.single 0 (C r)) 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
i✝ i : ℕ
⊢ (derivativeFinsupp (C r)) (i + 1) = (Finsupp.single 0 (C r)) (i + 1)

Tactic:
| =>

Goal state after:
R : Type u
inst✝ : Semiring R
r : R
i✝ i : ℕ
⊢ (derivativeFinsupp (C r)) (i + 1) = (Finsupp.single 0 (C r)) (i + 1)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 0 = (Finsupp.single 0 X + Finsupp.single 1 1) 0

Tactic:
| =>

Goal state after:
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 0 = (Finsupp.single 0 X + Finsupp.single 1 1) 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 1 = (Finsupp.single 0 X + Finsupp.single 1 1) 1

Tactic:
| =>

Goal state after:
R : Type u
inst✝ : Semiring R
i : ℕ
⊢ (derivativeFinsupp X) 1 = (Finsupp.single 0 X + Finsupp.single 1 1) 1
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
i n : ℕ
⊢ (derivativeFinsupp X) (n + 2) = (Finsupp.single 0 X + Finsupp.single 1 1) (n + 2)

Tactic:
| =>

Goal state after:
R : Type u
inst✝ : Semiring R
i n : ℕ
⊢ (derivativeFinsupp X) (n + 2) = (Finsupp.single 0 X + Finsupp.single 1 1) (n + 2)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
| C 0 + (X - C a) * (p /ₘ (X - C a))

Tactic:
C_0,

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : eval a p = 0
| 0 + (X - C a) * (p /ₘ (X - C a))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = p %ₘ (X - C 0)

Tactic:
C_0,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = p %ₘ (X - 0)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case h.left
α : Type u_1
s : ℕ → Set α
⊢ Antitone fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m

pp: case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
· exact fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl

Goal state after:
case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)
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 = (g.comp (X + C t)).reverse.leadingCoeff

Tactic:
reverse_leadingCoeff,

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 = (g.comp (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
h : I.pi s ∈ pi f
i : ι
hi : i ∈ I
⊢ s i ∈ f i

Tactic:
classical
  rcases mem_pi.1 h with ⟨I', -, t, htf, hts⟩
  refine mem_of_superset (htf i) fun x hx => ?_
  have : ∀ i, (t i).Nonempty := fun i => nonempty_of_mem (htf i)
  choose g hg using this
  have : update g i x ∈ I'.pi t := fun j _ => by
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*]
  simpa using hts this i hi

Goal state after: