mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
⊢ {p ∈ n.primeFactors | p ∣ m} = m.primeFactors

Tactic:
simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm,
    divisors_filter_dvd_of_dvd hn hmn]

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

Goal state before:
pp: b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)

Tactic:
mul_one,

Goal state after:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (a + a * (b - 1)) / (b - 1) = a + a / (b - 1)
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: z : ℤ
⊢ image Prod.fst z.divisorsAntidiag = z.divisors

Tactic:
by
  ext
  simp [Eq.comm, dvd_def]

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

Goal state before:
pp: n k : ℕ
⊢ n.choose k ≤ 2 ^ n

Tactic:
obtain (rfl | hn) := eq_zero_or_pos n

Goal state after:
case inl
k : ℕ
⊢ choose 0 k ≤ 2 ^ 0

case inr
n k : ℕ
hn : n > 0
⊢ n.choose k ≤ 2 ^ n
Module: Mathlib.Data.Nat.Choose.Central

Goal state before:
pp: case h
n : ℕ
⊢ (n + 1 + n + 1).choose (n + 1) = 2 * (n + 1 + n).choose n

Tactic:
choose_succ_succ' (n + 1 + n) n,

Goal state after:
case h
n : ℕ
⊢ (n + 1 + n).choose n + (n + 1 + n).choose (n + 1) = 2 * (n + 1 + n).choose n
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + x.natAbs ≤ (↑n * m + x).natAbs + x.natAbs

Tactic:
refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)

Goal state after:
case inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m + x - x).natAbs
Module: Mathlib.Data.Nat.MaxPowDiv

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

Tactic:
apply (p + 2 |>.pow_lt_pow_iff_right <| by lia).mp
    apply Nat.lt_of_le_of_lt ?_ <| Nat.lt_pow_self <| by lia
    exact le_of_dvd (Nat.pos_of_ne_zero hn) pow_padicValNat_dvd

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

Goal state before:
pp: case inr.inr.p
p n k l : ℕ
hn : n ≠ 0
h : p ^ (p.maxPowDvdDiv n).fst * l = p ^ (p.maxPowDvdDiv n).fst * n.divMaxPow p
hl : ¬p ∣ l
hp : 1 < p
hk : k = (p.maxPowDvdDiv n).fst
⊢ 0 < p ^ (p.maxPowDvdDiv n).fst

Tactic:
exact Nat.pow_pos <| Nat.zero_lt_of_lt hp

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
⊢ emultiplicity a b < ↑k ↔ ¬a ^ k ∣ b

Tactic:
rw [pow_dvd_iff_le_emultiplicity, not_le]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Defs

Goal state before:
pp: p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p n = ↑(padicValNat p n)

Tactic:
emultiplicity_eq_coe,

Goal state after:
p : ℕ
hp : p ≠ 1
n : ℕ
hn : n ≠ 0
⊢ p ^ padicValNat p n ∣ n ∧ ¬p ^ (padicValNat p n + 1) ∣ n
Module: Mathlib.Data.Nat.Digits.Lemmas

Goal state before:
pp: b : ℕ
hb : 1 < b
l : ℕ
⊢ fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (consFixedLengthDigits hb l) ⋯

Tactic:
ext L
  simp_rw [Finset.disjiUnion_eq_biUnion, Finset.mem_biUnion, Finset.mem_range,
    consFixedLengthDigits, Finset.mem_image]
  refine ⟨fun hL ↦ ?_, ?_⟩
  · have hL₁ : L.length = l + 1 := ((mem_fixedLengthDigits_iff hb).mp hL).1
    have hL₂ : ∀ x ∈ L, x < b := ((mem_fixedLengthDigits_iff hb).mp hL).2
    have hL₃ : L ≠ [] := by simp [ne_nil_iff_length_pos, hL₁]
    refine ⟨L.head hL₃, hL₂ _ (L.head_mem hL₃), L.tail, ?_, cons_head_tail hL₃⟩
    refine (mem_fixedLengthDigits_iff hb).mpr ⟨?_, ?_⟩
    · rw [length_tail, hL₁, Nat.add_sub_cancel_right]
    · exact fun x hx ↦ hL₂ _ <| mem_of_mem_tail hx
  · rintro ⟨d, hd₁, T, hT, rfl⟩
    exact cons_mem_fixedLengthDigits_succ hb l d hd₁ hT

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

Goal state before:
pp: n : ℕ
f : ℕ →₀ ℕ
hf : f ≤ n.factorization
⊢ (f.prod fun x1 x2 ↦ x1 ^ x2) ∣ n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  rwa [← factorization_le_iff_dvd ?_ hn, factorization_prod_pow_eq_self_of_le_factorization hf]
  refine f.prod_ne_zero_iff.mpr fun _ hp ↦ ?_
  exact pow_ne_zero _ (prime_of_mem_primeFactors <| support_mono hf hp).ne_zero

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

Goal state before:
pp: case succ
b : ℕ
hb : 1 < b
l : ℕ
hr : ∑ L ∈ fixedLengthDigits hb l, L.sum = l * b ^ (l - 1) * b.choose 2
⊢ ∑ L ∈ fixedLengthDigits hb (l + 1), L.sum = (l + 1) * b ^ (l + 1 - 1) * b.choose 2

Tactic:
| succ l hr =>

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

Goal state before:
pp: case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization + d.factorization = n.factorization

Tactic:
←
    Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,

Goal state after:
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d * d).factorization = n.factorization
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
⊢ (n.choose k).factorization p ≤ log p n

Tactic:
by_cases h : (choose n k).factorization p = 0
  · simp [h]
  have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_not_prime h
  have hkn : k ≤ n := by
    refine le_of_not_gt fun hnk => h ?_
    simp [choose_eq_zero_of_lt hnk]
  rw [factorization_choose hp hkn (Nat.lt_add_one _)]
  exact (card_filter_le ..).trans_eq (Nat.card_Ico _ _)

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ ↑⟨n % orderOf x, ⋯⟩

Tactic:
Fin.val_mk

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
hx : IsOfFinOrder x
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ (n % orderOf x)
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a * X ^ n).divX = if n = 0 then 0 else C a * X ^ (n - 1)

Tactic:
simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

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

Tactic:
by
      obtain ⟨a, ha⟩ := hS1
      rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]
      exact pow_mem a ha (orderOf a - 1)

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n o : ℕ
a : R
p : R[X]
h_pow : p.natDegree ≤ n
h_exp : m * n ≤ o
h_pow_bas : p.coeff n = a
h : ¬o = m * n
⊢ m * n ≠ o

Tactic:
· exact Iff.mp ne_comm h

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r = 0
⊢ False

Tactic:
by subst hr0; simp [hq] at hr

Goal state after:
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
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
have ih := modByMonic_eq_sub_mul_div
          (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) q

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf : (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).degree < p.degree
ih :
  (p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) %ₘ q =
    p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree)) -
      q * ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))) /ₘ q)
⊢ p %ₘ q = p - q * (p /ₘ q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
⊢ (⇑derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑derivative)^[k] (f b)

Tactic:
by
  simp_rw [← Module.End.pow_apply, map_sum]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
⊢ rootMultiplicity a p = if p = 0 then 0 else multiplicity (X - C a) p

Tactic:
simp only [rootMultiplicity, multiplicity, emultiplicity]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
⊢ (if h : p = 0 then 0 else Nat.find ⋯) =
    if p = 0 then 0 else WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ generate s = (FilterBasis.ofSets s).filter

Tactic:
← (hasBasis_generate s).filter_eq

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ ⋯.filter = (FilterBasis.ofSets s).filter
Module: Mathlib.Order.Filter.Ker

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
f✝ g : Filter α
s✝ : Set α
a : α
s : Set α
f : Filter α
⊢ 𝓟 s ≤ f ↔ s ⊆ f.ker

Tactic:
simp [principal_le_iff]

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
κ : Type u_3
p : κ → Prop
s : (i : ι) → κ → Set (α i)
h : ∀ (i : ι), (f i).HasBasis p (s i)
h_dir : ∀ (I : Set ι) (k : ι → κ), I.Finite → (∀ i ∈ I, p (k i)) → ∃ k₀, p k₀ ∧ ∀ i ∈ I, s i k₀ ⊆ s i (k i)
⊢ ∀ (i' : Set ι × κ),
    i'.1.Finite ∧ p i'.2 →
      ∃ i, (i.1.Finite ∧ ∀ i_1 ∈ i.1, p (i.2 i_1)) ∧ (i.1.pi fun i_1 ↦ s i_1 (i.2 i_1)) ⊆ i'.1.pi fun i ↦ s i i'.2

Tactic:
· rintro ⟨I, k⟩ ⟨hI, hk⟩
    exact ⟨⟨I, fun _ ↦ k⟩, ⟨hI, fun _ _ ↦ hk⟩, subset_rfl⟩

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
⊢ 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) * X + C r * X ^ n * 1) * derivative q

Tactic:
mul_one,

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) * X + C r * X ^ n) * derivative q
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ

Tactic:
by
  rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter,
    preimage_compl, preimage_compl, compl_compl, compl_compl]

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod = normalize (normalizedFactors a).prod

pp: α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a

Tactic:
· rw [normalizedFactors, ← coe_normalizeHom, ← map_multiset_prod, coe_normalizeHom,
      normalize_idem]

Goal state after:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : StrongNormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ normalize (normalizedFactors a).prod = normalize a
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
⊢ {d | (weight w) d ≤ n}.Finite

Tactic:
suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
    exact Set.Finite.subset (Finset.finite_toSet _) this

Goal state after:
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
⊢ {d | (weight w) d ≤ n} ⊆ ↑(Finset.image (fun uv ↦ uv.1) fg)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ (if s = r then 1 else 0) = count s {r}

Tactic:
count_singleton

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r s : R
⊢ (if s = r then 1 else 0) = if s = r then 1 else 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ prod 0

Tactic:
prod_zero

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ∈ nthRootsFinset (n + 1) a₁
hη₂ : η₂ ∈ nthRootsFinset (n + 1) a₂
⊢ η₁ * η₂ ∈ nthRootsFinset (n + 1) (a₁ * a₂)

Tactic:
mem_nthRootsFinset n.succ_pos

Goal state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
η₁ η₂ a₁ a₂ : R
n : ℕ
hη₁ : η₁ ^ n.succ = a₁
hη₂ : η₂ ^ n.succ = a₂
⊢ (η₁ * η₂) ^ n.succ = a₁ * a₂
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
p q : T[X]
hpq : p * q ≠ 0
⊢ map (algebraMap T S) (p * q) ≠ 0

Tactic:
Polynomial.map_ne_zero_iff
    (FaithfulSMul.algebraMap_injective T S)

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
p q : T[X]
hpq : p * q ≠ 0
⊢ p * q ≠ 0
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 : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * (q.content * 1)) (p.content * p.primPart.content * (q.content * q.primPart.content))

Tactic:
mul_one,

Goal state after:
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * q.content) (p.content * p.primPart.content * (q.content * q.primPart.content))
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 : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * q.content) (p.content * 1 * (q.content * 1))

Tactic:
mul_one,

Goal state after:
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (p.content * q.content) (p.content * (q.content * 1))
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart.leadingCoeff * p.primPart.leadingCoeff) (q.primPart * p.primPart).eraseLead.content ∣ 1

Tactic:
gcd_comm

Goal state after:
case neg.inr
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart * p.primPart).eraseLead.content (q.primPart.leadingCoeff * p.primPart.leadingCoeff) ∣ 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (q.primPart.eraseLead.content * 1) q.primPart.leadingCoeff *
      gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1

pp: 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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n

Tactic:
mul_one,

Goal state after:
case neg.inr
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd q.primPart.eraseLead.content q.primPart.leadingCoeff *
      gcd (q.primPart * p.primPart).eraseLead.content p.primPart.leadingCoeff ∣
    1

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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ p / q = 0

Tactic:
div_def,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)) = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd (p.primPart.eraseLead.content * 1) p.primPart.leadingCoeff ∣ 1

pp: 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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

pp: 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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n

Tactic:
mul_one,

Goal state after:
case neg.inr
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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ gcd p.primPart.eraseLead.content p.primPart.leadingCoeff ∣ 1

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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

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]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ (q.primPart.eraseLead * p.primPart).degree < ↑n
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p / q).degree ≤ p.degree

Tactic:
div_def,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hq : ¬q = 0
⊢ (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))).degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p / q).degree < p.degree

Tactic:
div_def,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))).degree < p.degree
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: 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) = map f p / map f q

Tactic:
div_def,

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))) = map f p / map f q
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
div_def,

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
⊢ a.prod ≤ b.prod ↔ a ≤ b

Tactic:
by
  refine ⟨fun h ↦ ?_, prod_mono⟩
  have : a.prod.factors ≤ b.prod.factors := factors_mono h
  rwa [prod_factors, prod_factors] at this

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
⊢ IsUnit (1 * 1)

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ IsUnit 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ Associated (C (p * q).content * (p * q).primPart) (C (p * q).content * (p.primPart * q.primPart))

Tactic:
conv_lhs => rw [← (p * q).eq_C_content_mul_primPart,
    p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart, mul_mul_mul_comm, ← C_mul]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ Associated (C (p.content * q.content) * (p.primPart * q.primPart)) (C (p * q).content * (p.primPart * q.primPart))