mathlib-initiative/mathlib-tactics huggingface dataset:
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'
J K : Subgroup G'
hJK : J.relIndex K ≠ 0
⊢ J.relIndex (map f (comap f K)) ≠ 0

Tactic:
exact fun h ↦ hJK <| relIndex_eq_zero_of_le_right (map_comap_le _ _) h

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ Injective ⇑(castHom ⋯ R)

Tactic:
injective_iff_map_eq_zero

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬↑k = ↑0
⊢ 1 ≤ ↑k

Tactic:
Fin.val_zero,

Goal state after:
case neg.succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬↑k = 0
⊢ 1 ≤ ↑k
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg.succ.hnc
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
k : ZMod (n✝ + 1)
hk : ¬k = 0
⊢ ¬k = 0

Tactic:
exact hk

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n.succ → 1 ≤ a✝

Tactic:
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

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

Goal state before:
pp: p n : ℕ
_h : 0 ≤ ↑n
⊢ ↑(↑n).toNat = ↑↑n

Tactic:
by simp only [Int.cast_natCast, Int.toNat_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n → 1 ≤ a✝

Tactic:
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a : ℕ × ℕ
⊢ a ∈ n.divisorsAntidiagonal ↔ a.1 * a.2 = n ∧ n ≠ 0

Tactic:
mem_divisorsAntidiagonal

Goal state after:
n : ℕ
a : ℕ × ℕ
⊢ a.1 * a.2 = n ∧ n ≠ 0 ↔ a.1 * a.2 = n ∧ n ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
a : ZMod 0
⊢ a * a⁻¹ = ↑(a.val.gcd 0)

Tactic:
dsimp [ZMod] at a ⊢

Goal state after:
case zero
a : ℤ
⊢ a * a⁻¹ = ↑((val a).gcd 0)
Module: Mathlib.NumberTheory.Divisors

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

Tactic:
mem_divisorsAntidiagonal

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

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

Tactic:
mem_divisorsAntidiagonal

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

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n

Tactic:
Nat.coprime_iff_gcd_eq_one,

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.gcd n = 1
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
exact hn.geom_sum_pos

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
⊢ ∑ x ∈ properDivisors 0, x = 1 ↔ Prime 0

pp: case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)

Tactic:
· simp [Nat.not_prime_zero]

Goal state after:
case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
| image Prod.fst n.divisorsAntidiagonal

Tactic:
← map_div_left_divisors,

Goal state after:
n : ℕ
| image Prod.fst (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors)
Module: Mathlib.Data.Nat.Digits.Defs

Goal state before:
pp: case zero
b : ℕ
h : 2 ≤ b
w : 0 < 0
⊢ b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)

Tactic:
cases w

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

Goal state before:
pp: m k n : ℕ
| (∃ y, m * y + k = n) ↔ ↑n = ↑k ∧ k ≤ n

Tactic:
enter [1, 1, y]; rw [add_comm, eq_comm]

Goal state after:
m k n y : ℕ
| n = k + m * y
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
p : ZMod N × ℕ
⊢ (fun n ↦ (↑n, n / N)) ((fun p ↦ p.1.val + N * p.2) p) = p

Tactic:
ext1
    · simp only [add_comm p.1.val, cast_add, cast_mul, natCast_self, zero_mul, natCast_val,
        cast_id', id_eq, zero_add]
    · simp only [add_comm p.1.val, mul_add_div (NeZero.pos _),
        (Nat.div_eq_zero_iff).2 <| .inr p.1.val_lt, add_zero]

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

Goal state before:
pp: case e'_2
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = ofDigits b (b.digits n)

Tactic:
rw [ofDigits_digits]

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

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

pp: case succ.zero
m : ℕ
hm : m ≠ 0
⊢ ((0 + 1).digits m).getLast ⋯ ≠ 0

pp: case succ.succ
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
· cases m
    · cases hm rfl
    · simp

Goal state after:
case succ.zero
m : ℕ
hm : m ≠ 0
⊢ ((0 + 1).digits m).getLast ⋯ ≠ 0

case succ.succ
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Tactic:
rw [ofDigits_digits]

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

Goal state before:
pp: case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = ofDigits p (List.drop tl.length tl)
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
List.drop_length,

Goal state after:
case inl.cons.inr
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
h' : ¬tl = []
w₁' : ∀ l ∈ tl, l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl) = ofDigits p []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
  convert! Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)
  rw [orderOf, mul_left_iterate_apply_one]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ ¬p ^ (multiplicity p b + 1) ∣ b

pp: case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ (multiplicity p b + 1) ∣ a

Tactic:
· apply this.not_pow_dvd_of_multiplicity_lt
      simp

Goal state after:
case hsucc
α : Type u_1
inst✝ : Ring α
p a b : α
h : ↑(multiplicity p b) < emultiplicity p a
this : FiniteMultiplicity p b
⊢ p ^ (multiplicity p b + 1) ∣ a
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: case refine_1.refine_2
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 ≠ []
⊢ ∀ x ∈ L.tail, x < b

Tactic:
exact fun x hx ↦ hL₂ _ <| mem_of_mem_tail hx

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)

Tactic:
induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_isUnit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : RightCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ m + k ≡ m [MOD orderOf x] → x ^ (m + k) = x ^ m

Tactic:
· intro h
    have hk : x ^ k = 1 := by
      apply pow_eq_one_iff_modEq.2
      exact Nat.ModEq.add_left_cancel' m (by simpa using h)
    calc
      x ^ (m + k) = x ^ m * x ^ k := by rw [pow_add]
      _ = x ^ m := by simp [hk]

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

Goal state before:
pp: case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k

Tactic:
exact H.1

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

Goal state before:
pp: case refine_2
h2 : _root_.Prime 2
⊢ ∀ (b : Bool) (n : ℕ), (n ≠ 0 → emultiplicity 2 n ! < ↑n) → bit b n ≠ 0 → emultiplicity 2 (bit b n)! < ↑(bit b n)

Tactic:
intro b n ih h

Goal state after:
case refine_2
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
⊢ emultiplicity 2 (bit b n)! < ↑(bit b n)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ 0 ≤ p.divX.degree

Tactic:
rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * X.leadingCoeff ≠ 0
⊢ ¬p = C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff = 1

Tactic:
by
      apply monic_mul_C_of_leadingCoeff_mul_eq_one
      simp [← pow_add, hp]

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
rw [hf]

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hc : IsRelPrime (p.coeff 0) (p.coeff 1)
f g : R[X]
h : p = f * g
H : f.degree ≤ g.degree
hg : g.degree = 1
hf : f = C (f.coeff 0)
⊢ IsUnit (C (f.coeff 0))
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).natDegree ≤ ↑q.natDegree + ↑(p /ₘ q).natDegree

Tactic:
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)

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

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

Tactic:
RingHom.id_apply,

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
⊢ s • 1 * eval₂ (RingHom.id R) x p = s • eval x p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff

Tactic:
rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, (X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p

Tactic:
refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n, (X - C a) ^ (m + 1) ∣ p
⊢ (X - C a) ^ n ∣ p
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ (fun a ↦ if h : a ∈ s then p ⟨a, h⟩ else univ) a ∈ f a

Tactic:
by simpa [ha] using hp ⟨a, ha⟩

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s) → s ∈ f ×ˢ g

Tactic:
rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
    exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : q.leadingCoeff ∣ p.leadingCoeff
r : R[X]
hr : q = p * r
u : Rˣ
hu : p.leadingCoeff * ↑u = q.leadingCoeff
⊢ (p * ↑((Units.map ↑C) u)).leadingCoeff = q.leadingCoeff

Tactic:
by simpa using hu

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

Goal state before:
pp: case refine_1
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).2 ≤ cofinite

Tactic:
exact boundary_le_cofinite f

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

Goal state before:
pp: case refine_2
α : Type u_2
f : Filter α
⊢ (f.ker, Coheyting.boundary f).1ᶜ ∈ (f.ker, Coheyting.boundary f).2

Tactic:
exact mem_inf_of_right (mem_principal_self f.kerᶜ)

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
w : σ → M
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype σ
f : σ →₀ R
⊢ (weight w) f = ∑ i, f i • w i

Tactic:
rw [weight_apply, f.sum_fintype (fun i c ↦ c • w i) fun _ ↦ zero_smul _ _]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod

Tactic:
rw [eqc, Multiset.prod_add]

Goal state after:
case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ p.prod * c = p.prod * (factors c).prod
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = normalize r * p.support.gcd p.coeff

Tactic:
← Finset.gcd_mul_left

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support.gcd (C r * p).coeff = p.support.gcd fun x ↦ r * p.coeff x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg.calc_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
con : Classical.choose ⋯ = 0
⊢ c ~ᵤ 1

Tactic:
convert! (Classical.choose_spec (pf c cne0)).2.symm
        rw [con, Multiset.prod_zero]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ (C a * X ^ n).aroots S = n • {0}

Tactic:
aroots_C_mul_X_pow ha

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
ha : a ≠ 0
n : ℕ
⊢ n • {0} = n • {0}
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ∈ p.support.erase p.natDegree
⊢ p.coeff i = p.eraseLead.coeff i

Tactic:
Finset.mem_erase

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e w.prod * ↑e ↑u = a

Tactic:
MonoidHom.coe_coe,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e w.prod * e ↑u = a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ IsUnit p.content

Tactic:
IsPrimitive

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.IsPrimitive

Tactic:
isPrimitive_iff_content_eq_one,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : ¬p.content = 0
⊢ p.primPart.content = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : (p * q).degree < ↑(n + 1)
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
degree_eq_natDegree (mul_ne_zero p0 q0),

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
hpq : ↑(p * q).natDegree < ↑(n + 1)
p0 : ¬p = 0
q0 : ¬q = 0
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ (C ↑(normUnit p.leadingCoeff) * p).roots = p.roots

Tactic:
roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ p.roots = p.roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
classical
  exact Multiset.le_iff_count.2 fun b => by
    rw [count_roots]
    apply count_map_roots h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ (p * q).IsPrimitive

Tactic:
isPrimitive_iff_content_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ (p * q).content = 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : (Associates.mk a).factors ⊓ (Associates.mk b).factors = 0
⊢ ((Associates.mk a).factors ⊓ (Associates.mk b).factors).prod = 1

Tactic:
rw [hf]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : (Associates.mk a).factors ⊓ (Associates.mk b).factors = 0
⊢ FactorSet.prod 0 = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
⊢ ∃ r, r.IsPrimitive ∧ ∀ (s : R[X]), p ∣ s ∧ q ∣ s ↔ r ∣ s

Tactic:
refine ⟨r, rprim, fun s => ⟨?_, fun rs => ⟨pr.trans rs, qr.trans rs⟩⟩⟩

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
s : R[X]
⊢ p ∣ s ∧ q ∣ s → r ∣ s
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : (C (r.coeff 0)).IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : s.natDegree ≤ 0
⊢ False

Tactic:
isPrimitive_iff_content_eq_one,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : (C (r.coeff 0)).content = 1
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : s.natDegree ≤ 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ Irreducible p

Tactic:
← irreducible_mk

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ Irreducible (Associates.mk p)