mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.index ≠ 0
hK : K.index ≠ 0
⊢ (H ⊓ K).index ≠ 0

Tactic:
← relIndex_top_right

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.relIndex ⊤ ≠ 0
hK : K.relIndex ⊤ ≠ 0
⊢ (H ⊓ K).relIndex ⊤ ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).index ≤ H.index * K.index

Tactic:
← relIndex_top_right,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relIndex ⊤ ≤ H.relIndex ⊤ * K.relIndex ⊤
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).index ≠ 0
⊢ (⨅ i, f i).index ≠ 0

Tactic:
← relIndex_top_right

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Finite ι
f : ι → Subgroup G
hf : ∀ (i : ι), (f i).relIndex ⊤ ≠ 0
⊢ (⨅ i, f i).relIndex ⊤ ≠ 0
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ (⨅ i, f i).index ≤ ∏ i, (f i).index

Tactic:
← relIndex_top_right,

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ (⨅ i, f i).relIndex ⊤ ≤ ∏ x, (f x).relIndex ⊤
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
x y : M
hx : x ∈ Set.range ⇑f
hy : y ∈ Set.range ⇑f
⊢ #{g | f g = x} = #{g | f g = y}

Tactic:
rcases hx with ⟨x, rfl⟩

Goal state after:
G : Type u_1
M : Type u_2
F : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Fintype G
inst✝³ : Monoid M
inst✝² : DecidableEq M
inst✝¹ : FunLike F G M
inst✝ : MonoidHomClass F G M
f : F
y : M
hy : y ∈ Set.range ⇑f
x : G
⊢ #{g | f g = f x} = #{g | f g = y}
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = ↑z.val + ↑p * k

Tactic:
constructor
  · rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_intCast, Int.emod_add_mul_ediv]
  · rintro ⟨k, rfl⟩
    rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
      ZMod.natCast_self, zero_mul, add_zero, cast_id]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s ⊆ ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
subset_empty

Goal state after:
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
exact prod_divisorsAntidiagonal fun i j => f j i

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

Goal state before:
pp: n : ℕ
IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * n.centralBinom) ≤ 2 * (2 * n + 1) * n.centralBinom

Tactic:
rw [← mul_assoc]; linarith

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

Goal state before:
pp: m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast.cast = a

Tactic:
by
  have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
  rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

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

Goal state before:
pp: b n : ℕ
⊢ (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))

Tactic:
by
  simp [digits, digitsAux_def]

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

Goal state before:
pp: case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * ofDigits b (List.map (fun x ↦ n * x) tl)

Tactic:
← ih

Goal state after:
case cons
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun x ↦ n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: case inr
p : ℕ
hp : p ≠ 0
n k : ℕ
hp1 : 1 < p
⊢ (p ^ k * n).divMaxPow p = n.divMaxPow p

Tactic:
rcases eq_or_ne n 0 with rfl | hn <;> simp [divMaxPow, *]

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

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

Tactic:
split_ifs

Goal state after:
case pos
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : n / b = 0
⊢ [(n % b).digitChar].length ≤ e + 1 + 1

case neg
b f n e : ℕ
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
h✝ : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ 1 ^ n = 1

Tactic:
one_pow

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ 1 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ 1 ^ 0 = 1

Tactic:
one_pow

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ 1 = 1
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 * b ^ (l - 1)

Tactic:
rw [← Nat.pow_succ', Nat.sub_one, Nat.succ_pred hl]

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

Goal state before:
pp: n : ℕ
⊢ Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1

Tactic:
simp [Multiset.coe_eq_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
hx : x ^ n = 1
hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1
a : ℕ
ha : n = orderOf x * a
h : ¬a = 1
a_min_fac_dvd_p_sub_one : a.minFac ∣ n
⊢ a.minFac ∣ a

Tactic:
exact Nat.minFac_dvd a

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

Goal state before:
pp: case neg
n p : ℕ
hp : Prime p
h : n / p ^ n.factorization p = n
n_zero : ¬n = 0
⊢ n = 0 ∨ ¬p ∣ n

Tactic:
· right
      rw [← h]
      exact not_dvd_ordCompl hp n_zero

Goal state after:
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 p + n !.factorization p = 0

Tactic:
hn (lt_of_succ_lt h),

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

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ emultiplicity p (n + 1)! = emultiplicity p n ! + emultiplicity p (n + 1)

Tactic:
by
        rw [factorial_succ, hp.emultiplicity_mul, add_comm]

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

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

Tactic:
have := Nat.sub_add_cancel hkn
  convert! @emultiplicity_choose' p (n - k) k b hp _
  · rw [this]
  exact this.symm ▸ hnb

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ card ↥(zpowers a) ≤ k

Tactic:
Fintype.card_zpowers

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
k : ℕ
k_pos : k ≠ 0
ha : a ^ k = 1
⊢ orderOf a ≤ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
⊢ (∃ m, n ∣ k ^ m) ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
by
  refine ⟨fun ⟨m, h⟩ ↦ ?_, fun h ↦ ⟨n, dvd_pow_self_iff hn hk |>.mpr h⟩⟩
  rcases eq_or_ne m 0 with (rfl | hm)
  · simp_all
  rw [← Nat.primeFactors_pow k hm]
  exact Nat.primeFactors_mono h <| pow_ne_zero m hk

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
rw [← hS2, pow_succ]
      exact Set.mul_mem_mul ih ha

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

Goal state before:
pp: case pos.h₁
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
⊢ (if p * (n / p) = n then 0 else 0) = 0

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : p * (n / p) = n
⊢ 0 = 0

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : n / p ∉ f.support
h✝ : ¬p * (n / p) = n
⊢ 0 = 0
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) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : p ∣ n✝
⊢ f (q.coeff (n✝ / p)) = (map f q).coeff (n✝ / p)

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✝ : ℕ
h✝ : ¬p ∣ n✝
⊢ f 0 = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h₀.zero
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a✝¹ : 0 ∈ p.support
a✝ : 0 ≠ n + 1
⊢ (p.coeff 0 * ↑0 * if n = 0 - 1 then 1 else 0) = 0

Tactic:
rw [Nat.cast_zero, mul_zero, zero_mul]

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

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

Tactic:
derivative_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (monomial (n - 1)) (a * ↑n) = (monomial (n - 1)) (a * ↑n)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
rw [natDegree_lt_natDegree_iff hp']
    exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C ↑h.unit⁻¹ * C (a - b) = 1

Tactic:
← C_mul

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
h : IsUnit (a - b)
⊢ C (↑h.unit⁻¹ * (a - b)) = 1
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.zero
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
h : ¬p ∣ 0
⊢ 0 = f.coeff 0

pp: case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ 0 = f.coeff (n + 1)

Tactic:
· exact absurd (dvd_zero p) h

Goal state after:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
← degree_add_divByMonic hq h,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ q.degree + (p /ₘ q).degree
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 : R[X]
x : R
⊢ eval₂ (RingHom.id R) x ((s • 1) • p) = s • eval x p

Tactic:
eval₂_smul,

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : SMulZeroClass S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ (RingHom.id R) (s • 1) * eval₂ (RingHom.id R) x p = s • eval x p
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]
⊢ eval₂ C q ((s • 1) • p) = s • eval₂ C q p

Tactic:
eval₂_smul,

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]
⊢ C (s • 1) * eval₂ C q p = s • eval₂ C q p
Module: Mathlib.Algebra.Polynomial.Eval.SMul

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ eval₂ (C.comp f) X (r • p) = f r • eval₂ (C.comp f) X p

Tactic:
eval₂_smul,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (C.comp f) r * eval₂ (C.comp f) X p = f r • eval₂ (C.comp f) X p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : map f (y %ₘ x) = 0
⊢ map f (y %ₘ x) = map f 0

Tactic:
rw [H, Polynomial.map_zero]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Injective ⇑f
x y : R[X]
hx : x.Monic
H : y %ₘ x = 0
⊢ map f (y %ₘ x) = 0

Tactic:
rw [H, Polynomial.map_zero]

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

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
⊢ ∃ t, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i)

Tactic:
use fun n => ⋂ m ≤ n, s m

Goal state after:
case h
α : Type u_1
s : ℕ → Set α
⊢ (Antitone fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m) ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 ((fun n ↦ ⋂ m, ⋂ (_ : m ≤ n), s m) i)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ (⇑derivative)^[k + 1] (X ^ n) = ↑(n.descFactorial (k + 1)) * X ^ (n - (k + 1))

Tactic:
rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]

Goal state after:
case succ
R : Type u
inst✝ : CommSemiring R
n k : ℕ
ih : (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - (k + 1))) = ↑(n - k) * ↑(n.descFactorial k) * X ^ (n - (k + 1))
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
⊢ (if hi : i ∈ I then V ⟨i, hi⟩ else univ) ∈ s i

Tactic:
split_ifs

Goal state after:
case pos
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∈ I
⊢ V ⟨i, h✝⟩ ∈ s i

case neg
α : Type u
ι : Type u_2
s : ι → Filter α
I : Set ι
If : I.Finite
V : ↑I → Set α
hV : ∀ (i : ↑I), V i ∈ s ↑i
i : ι
h✝ : i ∉ I
⊢ univ ∈ s i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : p.natDegree = (p * u).natDegree
⊢ p = p * u

Tactic:
rw [natDegree_mul hq.1 hq.2, left_eq_add] at h₁

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * u).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = (p * C (u.coeff 0)).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u

Tactic:
leadingCoeff_mul,

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p u : R[X]
h₂ : p.leadingCoeff = p.leadingCoeff * (C (u.coeff 0)).leadingCoeff
hq : p ≠ 0 ∧ u ≠ 0
h₁ : u.natDegree = 0
⊢ p = p * u
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.refine_1.refine_2
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ c ∈ {r | IsUnit r ∨ Prime r}

Tactic:
· left; exact ha₁

Goal state after:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
⊢ ∃ g_1 ≤ g + f, degree g_1 = degree g + 1

Tactic:
obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop

Goal state after:
case succ
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
i : σ
hi : i ∈ f.support
⊢ ∃ g_1 ≤ g + f, degree g_1 = degree g + 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : 0 ∉ hd :: tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots

Tactic:
rw [List.mem_cons, not_or] at H

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ.refine_2
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
⊢ f ∈ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s

Tactic:
obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop

Goal state after:
case succ.refine_2
α : Type u_5
s : Set α
n : ℕ
ih : n • (fun x ↦ single x 1) '' s = {x | degree x = n ∧ ↑x.support ⊆ s}
f : α →₀ ℕ
x✝ : f ∈ {x | degree x = n + 1 ∧ ↑x.support ⊆ s}
f_deg : degree f = n + 1
f_supp : ↑f.support ⊆ s
i : α
hi : i ∈ f.support
⊢ f ∈ {x | degree x = n ∧ ↑x.support ⊆ s} + (fun x ↦ single x 1) '' s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
⊢ x ∈ normalizedFactors a → x ∉ normalizedFactors b

Tactic:
hxa

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
hc : IsRelPrime a b
x : α
hxa : x ∈ normalizedFactors a
⊢ x ∉ normalizedFactors b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : 0 < n
⊢ 1 ^ n = 1

Tactic:
one_pow

Goal state after:
R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : 0 < n
⊢ 1 = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
this : ¬IsUnit q
⊢ IsUnit r

Tactic:
simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff

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

Goal state before:
pp: case refine_1
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ 0 ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = 0 ∧ c' * b' = b

pp: case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b

pp: case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
· intros
    contradiction

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (x : R), IsUnit x → x ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = x ∧ c' * b' = b

case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣ C p.leadingCoeff * X ^ p.natDegree * q - C (p * q).leadingCoeff * X ^ (p * q).natDegree

Tactic:
leadingCoeff_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    C p.leadingCoeff * X ^ p.natDegree * q - C (p.leadingCoeff * q.leadingCoeff) * X ^ (p * q).natDegree
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod ∣ p

Tactic:
rw [← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)]
  rw [prod_multiset_root_eq_finset_root, Polynomial.map_prod]
  refine Finset.prod_dvd_of_coprime (fun a _ b _ h => ?_) fun a _ => ?_
  · simp_rw [Polynomial.map_pow, Polynomial.map_sub, map_C, map_X]
    exact (pairwise_coprime_X_sub_C (IsFractionRing.injective R <| FractionRing R) h).pow
  · exact Polynomial.map_dvd _ (pow_rootMultiplicity_dvd p a)

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
h : p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

pp: case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

Tactic:
· exact (derivative_rootMultiplicity_of_root h).symm.le

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ if hp : Irreducible p then BfactorSetMem ⟨p, hp⟩ ⊤ else False

Tactic:
split_ifs

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem ⟨p, hp⟩ ⊤