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

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose⁻¹ * g ∈ H

Tactic:
convert! one_mem H

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose⁻¹ * g = 1
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier =
    Fintype.card ↑(MulAction.orbit (ConjAct G) g) * Fintype.card ↥(MulAction.stabilizer (ConjAct G) g) /
      Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
Nat.mul_div_cancel

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card ↑(MulAction.orbit (ConjAct G) g)

case H
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n m : ℕ
h : m ∣ n
a : ZMod m
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = a

Tactic:
obtain ⟨a, rfl⟩ := intCast_surjective a

Goal state after:
n m : ℕ
h : m ∣ n
a : ℤ
⊢ ∃ a_1, (castHom h (ZMod m)) a_1 = ↑a
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
⊢ (-1).cast = ↑0 - 1

Tactic:
dsimp [ZMod, ZMod.cast]; simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hx : x < 0
hx' : 0 < x + 1
hn : 1 < n
⊢ 0 < ∑ i ∈ range n, x ^ i ∧ ∑ i ∈ range n, x ^ i < 1

Tactic:
refine Nat.le_induction ?_ ?_ n (show 2 ≤ n from hn)
  · rw [geom_sum_two]
    exact ⟨hx', (add_lt_iff_neg_right _).2 hx⟩
  clear hn
  intro n _ ihn
  rw [geom_sum_succ, add_lt_iff_neg_right, ← neg_lt_iff_pos_add', neg_mul_eq_neg_mul]
  exact
    ⟨mul_lt_one_of_nonneg_of_lt_one_left (neg_nonneg.2 hx.le) (neg_lt_iff_pos_add'.2 hx') ihn.2.le,
      mul_neg_of_neg_of_pos hx ihn.1⟩

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n m : ℕ
h : m ∈ n.divisors
⊢ 0 < m

Tactic:
cases m

Goal state after:
case zero
n : ℕ
h : 0 ∈ n.divisors
⊢ 0 < 0

case succ
n n✝ : ℕ
h : n✝ + 1 ∈ n.divisors
⊢ 0 < n✝ + 1
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ n.divisors.sup id = n

Tactic:
by
  refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · apply zero_le
  · exact Finset.le_sup (f := id) <| mem_divisors_self n hn

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ 0 = x + 1 ∧ Even n ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1

Tactic:
and_comm,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Even n ∧ 0 = x + 1 ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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] <;>
        simp

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

Goal state before:
pp: case succ.mp.succ
n✝ : ℕ
a : ZMod (n✝ + 1)
m : ℕ
he : 2 * a.val = (n✝ + 1) * (m + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

Tactic:
cases m

Goal state after:
case succ.mp.succ.zero
n✝ : ℕ
a : ZMod (n✝ + 1)
he : 2 * a.val = (n✝ + 1) * (0 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝ + 1

case succ.mp.succ.succ
n✝¹ : ℕ
a : ZMod (n✝¹ + 1)
n✝ : ℕ
he : 2 * a.val = (n✝¹ + 1) * (n✝ + 1 + 1)
⊢ a = 0 ∨ 2 * a.val = n✝¹ + 1
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: n k : ℕ
p : 0 < n
⊢ n.choose k < 2 ^ n

Tactic:
by
  refine lt_of_le_of_lt ?_ (Nat.two_pow_pred_lt_two_pow p)
  rw [← Nat.sub_add_cancel p]
  exact choose_succ_le_two_pow (n - 1) k

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

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

Tactic:
by_cases hb : b = 0

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

case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val
Module: Mathlib.Data.Nat.Digits.Defs

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

Tactic:
digitsAux

Goal state after:
case succ
b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < n✝ + 1
⊢ (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b) = (n✝ + 1) % b :: b.digitsAux h ((n✝ + 1) / b)
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p n : ℕ
⊢ n.divMaxPow p * p ^ padicValNat p n = n

Tactic:
unfold divMaxPow padicValNat
  fun_cases maxPowDvdDiv with
  | case1 h => exact go_spec h |>.1
  | case2 h => simp

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

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

Tactic:
exact le_of_dvd (Nat.pos_of_ne_zero hn) pow_padicValNat_dvd

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

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

Tactic:
cases m

Goal state after:
case zero.zero
hm : 0 ≠ 0
⊢ (digits 0 0).getLast ⋯ ≠ 0

case zero.succ
n✝ : ℕ
hm : n✝ + 1 ≠ 0
⊢ (digits 0 (n✝ + 1)).getLast ⋯ ≠ 0
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ emultiplicity a b < ↑m

Tactic:
hf.emultiplicity_eq_multiplicity

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
m : ℕ
hm : multiplicity a b < m
⊢ ↑(multiplicity a b) < ↑m
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char),
    (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1

Tactic:
intro n c tl; simp only [Nat.toDigitsCore, List.length]

Goal state after:
case succ
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
intro n c tl; simp only [Nat.toDigitsCore, List.length]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : min (emultiplicity p a) (emultiplicity p b) = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

Tactic:
simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢

Goal state after:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ ¬FiniteMultiplicity p (a + b)
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ (b.digitsAppend l (ofDigits b L)).length = l

pp: case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b

Tactic:
· rw [length_digitsAppend hb _ (mapsTo_ofDigits hb _ hL)]

Goal state after:
case refine_2
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b
Module: Mathlib.Data.Nat.Factorization.Defs

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

Tactic:
← primeFactorsList_count_eq

Goal state after:
n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ a.factorization ≤ b.factorization

Tactic:
Finsupp.le_def

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (∀ (p : ℕ), p ^ a.factorization p ∣ p ^ b.factorization p) ↔ ∀ (i : ℕ), a.factorization i ≤ b.factorization i
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
m : ℕ
hm : m ∈ Ico (p * n + 1) (p * (n + 1))
⊢ ¬p ∣ m

Tactic:
exact not_dvd_of_lt_of_lt_mul_succ (mem_Ico.mp hm).left (mem_Ico.mp hm).right

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

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : ¬Prime p
⊢ n.factorization p ≤ b

Tactic:
simp [factorization_eq_zero_of_not_prime n pp]

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

Goal state before:
pp: n p : ℕ
hn : ¬n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
if pp : p.Prime then ?_ else
    simp [pp]
  ext q
  rcases eq_or_ne q p with (rfl | hqp)
  · simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]
    simp
  · rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]
    simp [pp.factorization, hqp.symm]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hx
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y

Tactic:
exact h.orderOf_mul_dvd_lcm.trans (Nat.lcm_dvd hxy dvd_rfl)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
⊢ zpowers x = zpowers y ↔ x = y ∨ x⁻¹ = y

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩

Goal state after:
G : Type u_1
inst✝ : Group G
x y : G
hx : ¬IsOfFinOrder x
h : zpowers x = zpowers y
⊢ x = y ∨ x⁻¹ = y
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: R : Type u_6
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ card R • 1 = 0

Tactic:
card_nsmul_eq_zero

Goal state after:
R : Type u_6
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < p✝.degree
hC : ∀ {a : R}, a ≠ 0 → P (C a * X)
hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < p.degree → P p
h0' : 0 < (C (p.coeff 0) * X).degree
h0 : ¬0 < p.degree
h : p.coeff 0 = 0
⊢ False

Tactic:
by simp [h] at h0'

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

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

Tactic:
by
  simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
⊢ map f ((expand R p) q) = (expand S p) (map f q)

Tactic:
by_cases hp : p = 0
  · simp [hp]
  ext
  rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
  split_ifs <;> simp_all

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
⊢ derivative (map f p) = map f (derivative p)

Tactic:
rw [derivative_apply, 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.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Multiset A
x : A
hx : x ∈ s
p : R[X]
hp : (mapAlg R A) p = (Multiset.map (fun x ↦ X - C x) s).prod
⊢ (aeval x) p = 0

Tactic:
rw [← aeval_map_algebraMap A, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]
  rw [Multiset.map_map, Multiset.mem_map]
  exact ⟨x, hx, by simp⟩

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

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

Tactic:
rw [le_principal_iff]

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⋂ m, ⋂ (_ : m ≤ i), s m ∈ ⨅ i, 𝓟 (s i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : (X - C x).degree = 0
⊢ p.degree = 1

Tactic:
rw [h₁] at h₂

Goal state after:
R : Type u
inst✝¹ : CommRing R
p : R[X]
inst✝ : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = (X - C x) * g
this : IsUnit (X - C x) ∨ IsUnit g
h : IsUnit (X - C x)
h₁ : (X - C x).degree = 1
h₂ : 1 = 0
⊢ p.degree = 1
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl.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
⊢ s.prod = x * (y * k)

Tactic:
← mul_one s.prod,

Goal state after:
case cons.inl.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
⊢ s.prod * 1 = x * (y * k)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ (factors a).card = (factors b).card

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b = 0
⊢ (factors a).card = (factors b).card

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : ¬b = 0
⊢ (factors a).card = (factors b).card
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
M : Type u_4
inst✝ : CommMonoidWithZero M
S : Finset M₀
p : M
pp : Prime p
g : M₀ → M
hS : ∀ a ∈ S, ¬p ∣ g a
⊢ ¬p ∣ S.prod g

Tactic:
by
  exact mt (Prime.dvd_finsetProd_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots.card ≤ p.natDegree

Tactic:
by_cases hp0 : p = 0
  · simp [hp0]
  exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ f s • w s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
rw [← Finsupp.mem_support_iff] at hs
    rw [Finset.sum_eq_add_sum_sdiff_singleton_of_mem hs]
    exact le_add_of_nonneg_right <| Finset.sum_nonneg <|
      fun i _ ↦ nsmul_nonneg (hw i) (f i)

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a⁻¹ * C ↑a * X - C ↑a⁻¹ * C b).roots = {↑a⁻¹ * b}

Tactic:
← C_mul,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C (↑a⁻¹ * ↑a) * X - C ↑a⁻¹ * C b).roots = {↑a⁻¹ * b}
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C (↑a⁻¹ * ↑a) * X - C ↑a⁻¹ * C b).roots = {↑a⁻¹ * b}

Tactic:
← C_mul,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C (↑a⁻¹ * ↑a) * X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
⊢ p ∣ a ∨ p ∣ b

Tactic:
obtain ⟨fa, hfa⟩ := eif a ha0

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
⊢ p ∣ a ∨ p ∣ b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ (0 ^ (n + 1)).roots = (n + 1) • roots 0

pp: case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
· rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]

Goal state after:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots
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:
by simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff

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

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ (C ((algebraMap T S) a)).roots = 0

Tactic:
roots_C

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : T
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
classical
  rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
by
  by_cases h : p = 0
  · simp [h]
  rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] at h
  rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content,
    eraseLead_support]
  refine congr rfl (Finset.gcd_congr rfl fun i hi => ?_)
  rw [Finset.mem_erase] at hi
  rw [eraseLead_coeff, if_neg hi.1]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
⊢ a ∣ b * c → a ∣ c

Tactic:
simpa [mul_comm b c] using dvd_of_dvd_mul_left_of_no_prime_factors ha @no_factors

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ C ↑(normUnit r)⁻¹ * C ↑(normUnit r) = 1

Tactic:
rw [← map_mul, Units.inv_mul, C_1]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this : Nontrivial M
⊢ Fintype { x // x ∣ y }

Tactic:
haveI : StrongNormalizationMonoid M := UniqueFactorizationMonoid.strongNormalizationMonoid

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝ : Nontrivial M
this : StrongNormalizationMonoid M
⊢ Fintype { x // x ∣ y }
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : C (f.coeff 0) ≠ 0
a : R
r : R[X]
hr : derivative f * g = f * r
haf : derivative f = 0
⊢ ¬(C (f.coeff 0)).IsRoot a

Tactic:
exact not_isRoot_C _ _ <| C_ne_zero.mp hf0

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ C ↑(normUnit p.leadingCoeff)⁻¹ * C ↑(normUnit p.leadingCoeff) = 1

Tactic:
rw [← map_mul, Units.inv_mul, C_1]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C (p.coeff 0) * C (p.coeff 0)⁻¹

Tactic:
← C_mul,

Goal state after:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = C (p.coeff 0 * (p.coeff 0)⁻¹)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ #(p.aroots B).toFinset ≤ p.natDegree

Tactic:
Multiset.toFinset_card_le

Goal state after:
A : Type u_1
inst✝³ : CommRing A
p : A[X]
B : Type u_3
inst✝² : CommRing B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
⊢ (p.aroots B).card ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ¬map (algebraMap R S) (∏ i ∈ s, f i) = 0

Tactic:
Polynomial.map_eq_zero

Goal state after:
case a
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ¬∏ i ∈ s, f i = 0