mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (_root_.frobenius S p) (r • s) = (_root_.frobenius R p) r • (↑↑(_root_.frobenius S p)).toFun s

Tactic:
simp_rw [Algebra.smul_def, map_mul, ← (algebraMap R S).map_frobenius]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst✝² : ExpChar R p
inst✝¹ : ExpChar S p
x y : R
inst✝ : Algebra R S
r : R
s : S
⊢ (algebraMap R S) ((_root_.frobenius R p) r) * (_root_.frobenius S p) s =
    (algebraMap R S) ((_root_.frobenius R p) r) * (↑↑(_root_.frobenius S p)).toFun s
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(2 * n)

Tactic:
two_mul

Goal state after:
h2 : _root_.Prime 2
b : Bool
n : ℕ
ih : n ≠ 0 → emultiplicity 2 n ! < ↑n
h : bit b n ≠ 0
hn : ¬n = 0
⊢ emultiplicity 2 n ! + ↑n < ↑(n + n)
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: case mpr
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : AddCommMonoid G
inst✝ : IsCancelAdd G
x : k[G]
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x

Tactic:
intro h
    rw [← divOf_add_modOf x g, h, add_zero]
    exact dvd_mul_right _ _

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

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

Tactic:
natDegree_expand,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).coeff (f.natDegree * p) = f.coeff f.natDegree
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)
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
unfold modByMonic divByMonic divModByMonicAux
        dsimp
        rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
by
  nontriviality R
  by_cases hfg : f /ₘ g = 0
  · rw [hfg, natDegree_zero]
    rw [divByMonic_eq_zero_iff hg] at hfg
    rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]
  have hgf := hfg
  rw [divByMonic_eq_zero_iff hg] at hgf
  push Not at hgf
  have := degree_add_divByMonic hg hgf
  have hf : f ≠ 0 := by
    intro hf
    apply hfg
    rw [hf, zero_divByMonic]
  rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
    ← Nat.cast_add, Nat.cast_inj] at this
  rw [← this, add_tsub_cancel_left]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
by
  simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ (m + 1) • (m + k).succ.descFactorial k • p.coeff (m + k.succ) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)

Tactic:
smul_smul

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
⊢ ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case insert
α : Type u
f : Filter α
β : Type v
s : β → Set α
is : Set β
a✝¹ : β
s✝ : Set β
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
hs : ⋂ i ∈ s✝, s i ∈ f ↔ ∀ i ∈ s✝, s i ∈ f
⊢ ⋂ i ∈ insert a✝¹ s✝, s i ∈ f ↔ ∀ i ∈ insert a✝¹ s✝, s i ∈ f

Tactic:
simp [hs]

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

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

Tactic:
· refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)
    rfl

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

Goal state before:
pp: case right
α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ ⨅ i, 𝓟 (x i) = ⨅ s ∈ range x, 𝓟 s

Tactic:
iInf_range

Goal state after:
case right
α : Type u_1
ι' : Sort u_5
inst✝ : Countable ι'
x : ι' → Set α
⊢ ⨅ i, 𝓟 (x i) = ⨅ i, 𝓟 (x i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
exact
      (div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
          ⟨by
            rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div, ← add_assoc,
              add_comm (q * _), modByMonic_add_div],
            (degree_add_le _ _).trans_lt
              (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2

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

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

Tactic:
eq_neg_iff_add_eq_zero,

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
⊢ -p %ₘ q + p %ₘ q = 0
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

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:
· rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]

Goal state after:
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
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
p : α → β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, ¬p x.1 x.2
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (x_1 : β) in lb, ¬p x x_1

Tactic:
exact h.curry

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: case neg
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
all_top : ∀ y ∈ s, ∀ (x : β), x ≤ f y
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
obtain ⟨a₀, ha₀s⟩ := hs
    exact ⟨a₀, ha₀s, fun a ha => all_top a ha (f a₀)⟩

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
f : R[X]
⊢ derivative (↑n * f) = ↑n * derivative f

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (factors a)).prod ~ᵤ a

Tactic:
factors,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map normalize (if h : a = 0 then 0 else Classical.choose ⋯)).prod ~ᵤ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Nontrivial α
⊢ (normalizedFactors 1).prod ~ᵤ Multiset.prod 0

Tactic:
· apply prod_normalizedFactors one_ne_zero

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

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

Tactic:
| succ n ihn =>

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (ofMultiset s).roots = s

Tactic:
by
  simp

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

Goal state before:
pp: case inr.cons.hx
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h✝ : Nontrivial α
a✝ : α
s✝ : Multiset α
IH : 0 ∉ s✝ → normalizedFactors s✝.prod = (Multiset.map normalizedFactors s✝).sum
hs : 0 ∉ a✝ ::ₘ s✝
⊢ a✝ ≠ 0

Tactic:
exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)

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

Goal state before:
pp: case neg.calc_2
α : 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
x : α
hadd : x ∈ Classical.choose ⋯ ∨ x ∈ Classical.choose ⋯
⊢ Prime x

Tactic:
rcases hadd with h | h

Goal state after:
case neg.calc_2.inl
α : 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
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x

case neg.calc_2.inr
α : 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
x : α
h : x ∈ Classical.choose ⋯
⊢ Prime x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ (map (algebraMap T S) p ^ n).roots = n • p.aroots S

Tactic:
roots_pow

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ n • (map (algebraMap T S) p).roots = n • p.aroots S
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case hba
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finset.range n).gcd p.coeff ∣ p.content

Tactic:
exact Finset.gcd_mono (supp_subset_range h)

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

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

Tactic:
normalize_eq_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.IsPrimitive ↔ IsUnit p.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
⊢ q ∣ b' → IsUnit q

Tactic:
q_dvd_b'

Goal state after:
case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a p : R
p_prime : Prime p
a' b' c' : R
coprime : IsRelPrime a' b'
a_ne_zero : c' * a' ≠ 0
ih_a : c' * a' ≠ 0 → ∀ (b : R), ∃ a'_1 b' c'_1, IsRelPrime a'_1 b' ∧ c'_1 * a'_1 = c' * a' ∧ c'_1 * b' = b
pa_ne_zero : p * (c' * a') ≠ 0
h : ¬p ∣ c' * b'
q : R
q_dvd_pa' : q ∣ p * a'
q_dvd_b' : q ∣ b'
⊢ IsUnit q
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 q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)

Tactic:
intro n p q hpq

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]
hpq : (p * q).degree < ↑n
⊢ Associated (p * q).content (p.content * q.content)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ (Multiset.map Subtype.val a✝).prod = 0 ↔ ↑a✝ = ⊤

Tactic:
Multiset.prod_eq_zero_iff,

Goal state after:
case coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ 0 ∈ Multiset.map Subtype.val a✝ ↔ ↑a✝ = ⊤
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
⊢ q * p.div q + p.mod q = p

Tactic:
by_cases h : q = 0

Goal state after:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
h : q = 0
⊢ q * p.div q + p.mod q = p

case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p
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
⊢ normalize (q.primPart * p.primPart).content = 1

Tactic:
normalize_eq_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
⊢ IsUnit (q.primPart * p.primPart).content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ↑sa ≤ ↑sb
h_sb : b.factors = ↑sb
⊢ Multiset.count ⟨p, hp⟩ sa ≤ Multiset.count ⟨p, hp⟩ sb

Tactic:
rw [WithTop.coe_le_coe] at h

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hb : b ≠ 0
hp : Irreducible p
ha : ¬a = 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : sa ≤ sb
h_sb : b.factors = ↑sb
⊢ Multiset.count ⟨p, hp⟩ sa ≤ Multiset.count ⟨p, hp⟩ sb
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ (Associates.mk a0).factors
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ (Associates.mk a0).factors.prod

Tactic:
factors_mk a0 nza

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
ha0 : a ≠ 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ FactorSet.prod ↑(factors' a0)
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
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0

Tactic:
rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ (C 1 * X ^ n).rootSet S = {0}

Tactic:
rootSet_C_mul_X_pow hn

Goal state after:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ {0} = {0}

R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ 1 ≠ 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
⊢ p ∣ s ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
simp [hs]

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

Goal state before:
pp: case neg
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:
dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs

Goal state after:
case neg
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.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
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.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q ∣ s ↔ C (lcm p.content q.content) * r ∣ s

Tactic:
dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs

Goal state after:
case neg
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.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    C (lcm p.content q.content) * r ∣ s
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
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.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    C (lcm p.content q.content) * r ∣ s

Tactic:
dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs

Goal state after:
case neg
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.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (C (lcm p.content q.content) * r).content ∣ s.content ∧ (C (lcm p.content q.content) * r).primPart ∣ s.primPart
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)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count (Associates.mk a0).factors
⊢ ∃ b, Associates.mk a0 = b ^ k

Tactic:
rw [factors_mk a0 hz] at hk

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
⊢ ∃ b, Associates.mk a0 = b ^ k
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : Algebra.Transcendental R A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental S B

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at H ⊢
  exact fun halg ↦ H (halg.of_ringHom_of_comp_eq f g hf hg h)

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsTorsionFree K L
inst✝ : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : (aeval b) p = 0
⊢ ∃ a, f a = b

Tactic:
let f' : p.rootSet L → p.rootSet L := (rootSet_maps_to' (fun x ↦ x) f).restrict f _ _

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsTorsionFree K L
inst✝ : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : (aeval b) p = 0
f' : ↑(p.rootSet L) → ↑(p.rootSet L) := Set.MapsTo.restrict (⇑f) (p.rootSet L) (p.rootSet L) ⋯
⊢ ∃ a, f a = b
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
rw [hpq, map_mul, aeval_X_pow] at hp

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : (aeval s) q * s ^ rootMultiplicity 0 p = 0
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ span R ((fun x ↦ (monomial x) 1) '' (s + t)) ≤ restrictSupport R s * restrictSupport R t

Tactic:
Submodule.span_le,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ (fun x ↦ (monomial x) 1) '' (s + t) ⊆ ↑(restrictSupport R s * restrictSupport R t)
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ span R ((fun x ↦ (monomial x) 1) '' s * (fun x ↦ (monomial x) 1) '' t) ≤ restrictSupport R (s + t)

Tactic:
Submodule.span_le,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ (fun x ↦ (monomial x) 1) '' s * (fun x ↦ (monomial x) 1) '' t ⊆ ↑(restrictSupport R (s + t))
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ span R ((fun x ↦ (monomial x) 1) '' 0) ≤ 1

Tactic:
Submodule.span_le,

Goal state after:
case a
σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ (fun x ↦ (monomial x) 1) '' 0 ⊆ ↑1