mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
⊢ ∀ (n : ℕ) (a : R),
    (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n) → (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))

Tactic:
intro n a _

Goal state after:
case refine_3
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
⊢ (C a * X ^ (n + 1)).natDegree = 0 ∨ M (C a * X ^ (n + 1))
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (C a + p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n) a)
n : ℕ
a : R
a✝ : (C a * X ^ n).natDegree = 0 ∨ M (C a * X ^ n)
a0 : ¬a = 0
⊢ M ((monomial (n + 1)) a)

Tactic:
exact h_monomial a0 n.succ_ne_zero

Goal state after:
Module: Mathlib.Tactic.ComputeDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
deg m o : WithBot ℕ
c : R
p : R[X]
h_deg_le : p.degree ≤ m
coeff_eq : p.coeff (WithBot.unbotD 0 deg) = c
coeff_ne_zero : c ≠ 0
deg_eq_deg : m = deg
coeff_eq_deg : o = deg
⊢ p.degree = deg

Tactic:
subst coeff_eq coeff_eq_deg deg_eq_deg

Goal state after:
R : Type u_1
inst✝ : Semiring R
m : WithBot ℕ
p : R[X]
h_deg_le : p.degree ≤ m
coeff_ne_zero : p.coeff (WithBot.unbotD 0 m) ≠ 0
⊢ p.degree = m
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : FaithfulSMul R S
p : R[X]
hp : Irreducible p
hdeg : p.natDegree ≠ 1
x : S
hx : x ∈ (algebraMap R S).range
⊢ (aeval x) p ≠ 0

Tactic:
obtain ⟨_, rfl⟩ := hx
  rw [aeval_algebraMap_apply_eq_algebraMap_eval]
  exact fun heq ↦ hp.not_isRoot_of_natDegree_ne_one hdeg <|
    FaithfulSMul.algebraMap_injective _ _ <| map_zero (algebraMap R S) ▸ heq

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
⊢ False

Tactic:
by
    have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
    have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
    have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
    have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
    have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
      simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne,
          hr0, not_false_eq_true]
    have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
      rw [← degree_eq_natDegree hp0]; exact hp
    have := congr_arg natDegree hr
    rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
    exact
      ne_of_lt
        (lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
          (add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
        this

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
⊢ rootMultiplicity c (comp 0 (C a * X + C b)) ≤ rootMultiplicity (a * c + b) 0

case inr
R : Type u
inst✝ : CommRing R
p : R[X]
a b c : R
ha : IsUnit a
this : Invertible a := ha.invertible
hp : p ≠ 0
⊢ rootMultiplicity c (p.comp (C a * X + C b)) ≤ rootMultiplicity (a * c + b) p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
x✝¹ x✝ : R[X]
⊢ X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝

Tactic:
simp_rw [dvd_iff_isRoot, IsRoot.def, eval_mul, mul_eq_zero]
    exact id

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

Goal state before:
pp: case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (frobenius R p) ((expand R p) (map (iterateFrobenius R p k) ((expand R (p ^ k)) f))) =
    map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k)) f))

Tactic:
← map_expand,

Goal state after:
case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k)) f) = f ^ p ^ k
⊢ map (frobenius R p) (map (iterateFrobenius R p k) ((expand R p) ((expand R (p ^ k)) f))) =
    map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k)) f))
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
l : ι → Filter α
p : (i : ι) → ι' i → Prop
s : (i : ι) → ι' i → Set α
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
t : Set α
⊢ (∃ i, (i.fst.Finite ∧ ∀ (i_1 : ↑i.fst), p (↑i_1) (i.snd i_1)) ∧ ⋂ i_1, s (↑i_1) (i.snd i_1) ⊆ t) → t ∈ ⨅ i, l i

Tactic:
rintro ⟨⟨I, f⟩, ⟨hI, hf⟩, hsub⟩
    grw [← hsub]
    cases hI.nonempty_fintype
    exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p q : R[X]
x : S
hx : eval₂ f x q = 0
⊢ eval₂ f x (p %ₘ q) = eval₂ f x p

Tactic:
rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

Tactic:
by_cases! h : ¬ q.Monic

Goal state after:
case pos
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : ¬q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q

case neg
R : Type u
inst✝ : CommRing R
p₁ p₂ q : R[X]
h : q.Monic
⊢ p₁ * p₂ %ₘ q = p₁ %ₘ q * (p₂ %ₘ q) %ₘ q
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
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = ((X + C t - (C t).comp (X + C t)) ^ m * g.comp (X + C t)).trailingCoeff

Tactic:
C_comp,

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = ((X + C t - C t) ^ m * g.comp (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ pi f ⊓ 𝓟 (I.pi s) = ⊥ ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥

Tactic:
rw [← univ_pi_piecewise_univ I, pi_inf_principal_univ_pi_eq_bot]

Goal state after:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), (f i).NeBot
I : Set ι
⊢ (∃ i, f i ⊓ 𝓟 (I.piecewise s (fun x ↦ univ) i) = ⊥) ↔ ∃ i ∈ I, f i ⊓ 𝓟 (s i) = ⊥
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
lift s to Finset ι using hs
  exact mod_cast iInf_principal_finset s f

Goal state after:
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ (￢￢a) = ∂ (￢a)

Tactic:
simp_rw [boundary, hnot_hnot_hnot, inf_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W

Tactic:
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : ¬derivative P = 0
hP'' : P.natDegree ≠ 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_

Goal state after:
R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : ¬derivative P = 0
hP'' : P.natDegree ≠ 0
⊢ (derivative P).natDegree < k
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons
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, y ∈ {r | IsUnit r ∨ Prime r}) → 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
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
simp only [Multiset.prod_cons] at hprod

Goal state after:
case cons
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, y ∈ {r | IsUnit r ∨ Prime r}) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hm : (IsUnit c ∨ Prime c) ∧ ∀ a ∈ s, IsUnit a ∨ Prime a
hprod : c * s.prod = x * y
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ (∑ x ∈ powersetCard (#S - k) S ×ˢ S with
      match x with
      | (T, i) => i ∈ T,
      match x with
      | (T, i) => ∏ a ∈ T.erase i, (X - C a)) =
    ∑ x ∈ powersetCard (#S - (k + 1)) S ×ˢ S with
      match x with
      | (T, i) => i ∉ T,
      match x with
      | (T, i) => ∏ a ∈ T, (X - C a)

Tactic:
apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
S : Finset R
hk : k ≤ #S
⊢ (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)

Tactic:
induction k
  case zero => simp
  case succ k ind =>
    specialize ind (Nat.le_of_succ_le hk)
    nth_rewrite 1 [add_comm]
    rw [Function.iterate_add_apply, Function.iterate_one, ind, ← nsmul_eq_mul, derivative_smul,
      nsmul_eq_mul, derivative_sum, Nat.factorial_succ, mul_comm (k + 1), Nat.cast_mul, mul_assoc]
    congr 1
    calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case h
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
⊢ b ∣ k

Tactic:
have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)

Goal state after:
case h
M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : (a : M₀) → DecidablePred (Associated a)
a : M₀
s : Multiset M₀
induct : ∀ (n : M₀), (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → (∀ (a : M₀), countP (Associated a) s ≤ 1) → s.prod ∣ n
h : ∀ a_1 ∈ a ::ₘ s, Prime a_1
uniq : ∀ (a_1 : M₀), countP (Associated a_1) (a ::ₘ s) ≤ 1
k : M₀
div : ∀ a_1 ∈ a ::ₘ s, a_1 ∣ a * k
b : M₀
b_in_s : b ∈ s
b_div_n : b ∣ a * k
⊢ b ∣ k
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ Multiset.Rel Associated (p ::ₘ f) g

Tactic:
let ⟨b, hbg, hb⟩ :=
      (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
        hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)

Goal state after:
case cons
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ f) g
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p : Multiset M
a : M
s : Multiset M
ih : (Multiset.map Associates.mk s).prod = Associates.mk s.prod
⊢ (Multiset.map Associates.mk (a ::ₘ s)).prod = Associates.mk (a ::ₘ s).prod

Tactic:
by simp [ih, Associates.mk_mul_mk]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ (Multiset.map (Associates.mk ∘ f) p.val).prod = Associates.mk (∏ i ∈ p, f i)

Tactic:
← Multiset.map_map,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
p : Finset ι
f : ι → M
⊢ (Multiset.map Associates.mk (Multiset.map f p.val)).prod = Associates.mk (∏ i ∈ p, f i)
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : s ∉ f.support
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
· simp only [notMem_support_iff] at h
    rw [h]
    apply zero_le

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

Goal state before:
pp: case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0

Tactic:
by_contra hs

Goal state after:
case mp
σ : Type u_1
M : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ normalizedFactors a

Tactic:
rw [hp]

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
p : α
a_assoc : a ~ᵤ p
hp : normalizedFactors a = {p}
⊢ p ∈ {p}
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ y

Tactic:
←
      (prod_normalizedFactors hy).dvd_iff_dvd_right

Goal state after:
case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x ≤ normalizedFactors y → (normalizedFactors x).prod ∣ (normalizedFactors y).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (Associates.out ∘ Associates.mk) (factors a) = Multiset.map (Associates.out ∘ Associates.mk) (factors b)

Tactic:
← Multiset.map_map,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (Associates.out ∘ Associates.mk) (factors b)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map (Associates.out ∘ Associates.mk) (factors b)

Tactic:
← Multiset.map_map,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
h' : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (factors a)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (factors b))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ p ∈ normalizedFactors x

Tactic:
exact Multiset.mem_map.mpr ⟨y, hy₁, by
    rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]⟩

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
h✝ : Subsingleton α
⊢ m = 0

Tactic:
by
      refine Multiset.eq_zero_of_forall_notMem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

Tactic:
by
        by_cases hx : x = 0
        · simp [hx]
        by_cases hy : y = 0
        · simp [hy]
        simp [hx, hy]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : C p.content = 0
⊢ p.primPart.natDegree = p.natDegree

Tactic:
C_eq_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : p.content = 0
⊢ p.primPart.natDegree = p.natDegree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ p.count 0 = 0

Tactic:
simp only [count, dif_pos hp, bcount, Multiset.count_zero]

Goal state after:
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 * C q.leadingCoeff⁻¹)).degree < p.degree

Tactic:
exact degree_divByMonic_lt _ (q * C q.leadingCoeff⁻¹) hp
    (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)

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

Goal state after:
α✝ : 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)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ 0 ∣ map f y ↔ 0 ∣ y

Tactic:
zero_dvd_iff,

Goal state after:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f y = 0 ↔ 0 ∣ y
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f y = 0 ↔ 0 ∣ y

Tactic:
zero_dvd_iff,

Goal state after:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f y = 0 ↔ y = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : C (lcm p.content q.content) = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
C_eq_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : lcm p.content q.content = 0
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s