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

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.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)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ 0 + (1 + emultiplicity p (n + 1)) = emultiplicity p (n + 1) + 1

Tactic:
zero_add,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.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)), emultiplicity p m = 0
h : ∑ x ∈ Ico 1 (p * n + 1), emultiplicity p x ≠ ⊤
⊢ 1 + emultiplicity p (n + 1) = emultiplicity p (n + 1) + 1
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 : 0 + emultiplicity p k = ↑n
⊢ p ^ n ∣ k

Tactic:
zero_add,

Goal state after:
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 : emultiplicity p k = ↑n
⊢ p ^ n ∣ k
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℤ
⊢ a ^ (n % ↑(card G)) = a ^ n

Tactic:
by
  rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x * single g 1 %ᵒᶠ g).coeff g' = 0

Tactic:
rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_mul_single_of_forall_add_ne]

Goal state after:
case inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ ∀ (d : G), d + g ≠ g'
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case zero
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
⊢ a ^ (0 + 1) ∈ S

Tactic:
zero_add,

Goal state after:
case zero
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
⊢ a ^ 1 ∈ S
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 (0 + n) = g.coeff 0
⊢ X ^ (n + 1) ∣ f

Tactic:
zero_add,

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 : (X ^ n * g).coeff n = g.coeff 0
⊢ X ^ (n + 1) ∣ f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
⊢ map (iterateFrobenius R p n) ((expand R (p ^ n)) f) = f ^ p ^ n

Tactic:
induction n with
  | zero => simp
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A

Tactic:
by
  simp [isAlgebraic_def, transcendental_def, Transcendental]

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

Goal state before:
pp: case inr.refine_1.e_a.refine_1
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree

pp: case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
· ext; simp

Goal state after:
case inr.refine_1.e_a.refine_2
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n✝ : ℕ
this :
  ∀ (n : ℕ), p.natDegree ≤ n → (p /ₘ (X - C a)).coeff n = ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n✝
n : ℕ
hn : n < p.natDegree
x✝ : n✝ ≤ n
ih : (p /ₘ (X - C a)).coeff (n + 1) = ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst✝ : DecidablePred fun n ↦ ¬(X - C a) ^ (n + 1) ∣ p
⊢ rootMultiplicity a p = Nat.find ⋯

Tactic:
by
  dsimp [rootMultiplicity]
  rw [dif_neg p0]
  congr

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
hp : ¬p.natDegree = 0
⊢ (derivative p).natDegree = p.natDegree - 1

Tactic:
· simp [natDegree, degree_derivative hp]

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

Goal state before:
pp: α : Type u_2
a : α
⊢ (pure a).ker = {a}

Tactic:
← principal_singleton,

Goal state after:
α : Type u_2
a : α
⊢ (𝓟 {a}).ker = {a}
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
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff

Tactic:
have mul_eq := p.pow_mul_divByMonic_rootMultiplicity_eq t

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
mul_eq : (X - C t) ^ rootMultiplicity t p * (p /ₘ (X - C t) ^ rootMultiplicity t p) = p
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff
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)
⊢ ↑(n.descFactorial k) * (↑(n - k) * X ^ (n - k - 1)) = ↑((n - k) * n.descFactorial k) * X ^ (n - (k + 1))

Tactic:
Nat.sub_sub,

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 mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) → t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)

Tactic:
rintro ⟨I, hIf, hpI, hst⟩

Goal state after:
case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
I : Set ι
hIf : I.Finite
hpI : ∀ i ∈ I, p i
hst : ⋂ i ∈ I, s i ⊆ t
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
inst✝ : Finite ι
l : ι → Filter α
hd : Pairwise (Disjoint on l)
⊢ ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)

Tactic:
by
  have : Pairwise fun i j => ∃ (s : {s // s ∈ l i}) (t : {t // t ∈ l j}), Disjoint s.1 t.1 := by
    simpa only [Pairwise, Function.onFun, Filter.disjoint_iff, exists_prop, Subtype.exists] using hd
  choose! s t hst using this
  refine ⟨fun i => ⋂ j, @s i j ∩ @t j i, fun i => ?_, fun i j hij => ?_⟩
  exacts [iInter_mem.2 fun j => inter_mem (@s i j).2 (@t j i).2,
    (hst hij).mono ((iInter_subset _ j).trans inter_subset_left)
      ((iInter_subset _ i).trans inter_subset_right)]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ n) * eval₂ C q X) = eval₂ C q (derivative (C r * X ^ n * X)) * derivative q

Tactic:
eval₂_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ derivative (eval₂ C q (C r * X ^ n) * q) = eval₂ C q (derivative (C r * X ^ n * X)) * derivative q
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ eval₂ C q (derivative (C r * X ^ n)) * derivative q * q + eval₂ C q (C r * X ^ n) * derivative q =
    (eval₂ C q (derivative (C r * X ^ n)) * eval₂ C q X + eval₂ C q (C r * X ^ n)) * derivative q

Tactic:
eval₂_X,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
r : R
ih : derivative (eval₂ C q (C r * X ^ n)) = eval₂ C q (derivative (C r * X ^ n)) * derivative q
⊢ eval₂ C q (derivative (C r * X ^ n)) * derivative q * q + eval₂ C q (C r * X ^ n) * derivative q =
    (eval₂ C q (derivative (C r * X ^ n)) * q + eval₂ C q (C r * X ^ n)) * derivative q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
R : Type u
a : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hp : ¬p = 0
⊢ count a (Classical.choose ⋯) = rootMultiplicity a p

Tactic:
exact (Classical.choose_spec (exists_multiset_roots hp)).2 a

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
⊢ ∀ q ∈ normalizedFactors a, p ∣ q → p = q

Tactic:
q

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
⊢ q ∈ normalizedFactors a → p ∣ q → p = q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
u : R[X]ˣ
⊢ p.roots = (C ((↑u).coeff 0) * p).roots

Tactic:
roots_C_mul _ <| coeff_coe_units_zero_ne_zero u

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
u : R[X]ˣ
⊢ p.roots = p.roots
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case refine_1
σ : Type u_1
⊢ (Set.range fun a ↦ single a 1) ⊆ {d | degree d = 1}

Tactic:
simp [Set.range_subset_iff]

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

Goal state before:
pp: case refine_2
σ : Type u_1
⊢ {d | degree d = 1} ⊆ Set.range fun a ↦ single a 1

Tactic:
· intro p (hp : p.sum (fun a k ↦ k) = 1)
    obtain ⟨a, rfl⟩ := (Finsupp.sum_eq_one_iff _).mp hp
    use a

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
⊢ normalizedFactors m.prod = m

Tactic:
by
  cases subsingleton_or_nontrivial α
  · obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx
    simp
  · simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
      prime_factors_unique prime_of_normalized_factor h
        (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ 0 < normalizedFactors x

Tactic:
exact
      bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_notMem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬(p * X).coeff (a + 1) = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1

Tactic:
coeff_mul_X

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 ↔ ∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_1
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * (c' * a') = p * a

Tactic:
ha'

Goal state after:
case pos.refine_1
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * a = p * a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
⊢ IsUnit (C r).primPart

Tactic:
by
  by_cases h0 : r = 0
  · simp [h0]
  unfold IsUnit
  refine
    ⟨⟨C ↑(normUnit r)⁻¹, C ↑(normUnit r), by rw [← map_mul, Units.inv_mul, C_1], by
        rw [← map_mul, Units.mul_inv, C_1]⟩,
      ?_⟩
  rw [← normalize_eq_zero, ← C_eq_zero] at h0
  apply mul_left_cancel₀ h0
  conv_rhs => rw [← content_C, ← (C r).eq_C_content_mul_primPart]
  simp only [normalize_apply, map_mul]
  rw [mul_assoc, ← map_mul, Units.mul_inv, C_1, mul_one]

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]
a✝ : Nontrivial R
n : ℕ
p : R[X]
⊢ ∀ (q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)

Tactic:
q

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
p q : R[X]
⊢ (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : 0 + p % q = p
⊢ p.degree < q.degree

Tactic:
zero_add,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : p % q = p
⊢ p.degree < q.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p %ₘ (q * C q.leadingCoeff⁻¹)) = map f p %ₘ (map f q * C (f q.leadingCoeff)⁻¹)

Tactic:
← map_inv₀ f,

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p %ₘ (q * C q.leadingCoeff⁻¹)) = map f p %ₘ (map f q * C (f q.leadingCoeff⁻¹))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ ↑(factors' a)

Tactic:
apply mem_factorSet_some.2 h_mem

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

Goal state before:
pp: k : Type y
inst✝ : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ (p % q).natDegree < q.natDegree

Tactic:
have hq' : q.leadingCoeff ≠ 0 := by
    rw [leadingCoeff_ne_zero]
    contrapose hq
    simp [hq]
  rw [mod_def]
  refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_
  · refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    rw [mul_inv_eq_one₀ hq']
  · contrapose hq
    rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)]
    simp [hq]
  · exact natDegree_mul_C_le q q.leadingCoeff⁻¹

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

Goal state before:
pp: R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α f = 0

Tactic:
obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g

Goal state after:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α f = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b : α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
      rw [mul_comm, sup_mul_inf, mk_mul_mk, out_mk]
      exact normalize_associated (a * b)

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p ≠ 0

Tactic:
simp [← zero_le_degree_iff, h]

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

Goal state before:
pp: case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x * C (f x.leadingCoeff)⁻¹ ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y

Tactic:
← map_inv₀ f,

Goal state after:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x * C (f x.leadingCoeff⁻¹) ∣ map f y ↔ x * C x.leadingCoeff⁻¹ ∣ y
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ p.count m.factors

Tactic:
count,

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ (if hp : Irreducible p then bcount ⟨p, hp⟩ else 0) m.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ p.count m.factors ≠ 0 → p ≤ m

Tactic:
← pos_iff_ne_zero

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
m p : Associates α
h0 : m ≠ 0
hp : Irreducible p
⊢ 0 < p.count m.factors → p ≤ m
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p.count p.factors = 1

Tactic:
by
  simp [factors_self hp, Associates.count_some hp]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Field R
p₁ p₂ : R[X]
h : 0 ∣ p₁ - p₂
⊢ p₁ % 0 = p₂ % 0

pp: case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ p₁ % q = p₂ % q

Tactic:
· simpa [sub_eq_zero] using h

Goal state after:
case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ p₁ % q = p₂ % q
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : Countable R
⊢ {x | IsAlgebraic R x}.Countable

Tactic:
rw [← le_aleph0_iff_set_countable, ← lift_le_aleph0]

Goal state after:
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra R A
inst✝¹ : Module.IsTorsionFree R A
inst✝ : Countable R
⊢ lift.{?u.26, v} #↑{x | IsAlgebraic R x} ≤ ℵ₀
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : DivisionRing A
inst✝¹ : Field R
inst✝ : Algebra R A
n : ℚ
⊢ IsAlgebraic R ↑n

Tactic:
rw [← map_ratCast (algebraMap R A)]
  exact isAlgebraic_algebraMap (Rat.cast n)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = 0 + (aeval x) (C (p.coeff 0))

Tactic:
zero_add,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
h : (aeval x) p.divX = 0
⊢ (algebraMap K L) (p.coeff 0) = (aeval x) (C (p.coeff 0))
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + C a ≠ 0
aeval_eq : (aeval x) (p + C a) = 0
⊢ 0 + (C a).coeff 0 ≠ 0

Tactic:
zero_add,

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + C a ≠ 0
aeval_eq : (aeval x) (p + C a) = 0
⊢ (C a).coeff 0 ≠ 0
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : DirectLimit G f
⊢ Nonempty ι

Tactic:
by infer_instance

Goal state after: