mathlib-initiative/mathlib-tactics huggingface dataset:
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 = (g.comp (X + C t)).coeff 0

Tactic:
this

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 = eval t g
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
⊢ (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommSemiring R
n m : ℕ
p : R[X]
⊢ (⇑derivative)^[n] (p * X ^ m) =
    ∑ k ∈ range n.succ, (n.choose k * m.descFactorial k) • ((⇑derivative)^[n - k] p * X ^ (m - k))
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p

Tactic:
[

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
⊢ ∃ I_1, I_1.Finite ∧ (∀ i ∈ I_1, p i) ∧ ⋂ i ∈ I_1, s i ⊆ ⋂ i, V i

Tactic:
refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩

Goal state after:
case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
I : Set ι
hIf : I.Finite
V : ↑I → Set α
t : (i : ↑I) → p ↑i → Set α
ht₁ : ∀ (i : ↑I) (i_1 : p ↑i), s ↑i ⊆ t i i_1
ht₂ : ∀ (i : ↑I), V i = ⋂ (i_1 : p ↑i), t i i_1
⊢ ⋂ i ∈ I ∩ {i | p i}, s i ⊆ ⋂ i, V i
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p = q

Tactic:
replace h₁ := (natDegree_le_of_dvd hpq hq).antisymm h₁

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
h₁ : p.natDegree = q.natDegree
⊢ p = q
Module: Mathlib.Order.Heyting.Boundary

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

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ (￢￢a) = ∂ (￢a)
Module: Mathlib.Order.Heyting.Boundary

Goal state before:
pp: α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧
    a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)

Tactic:
refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩ <;> try { exact le_sup_of_le_left inf_le_left } <;>
    refine inf_le_of_right_le ?_

Goal state after:
case refine_4
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ b

case refine_6
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
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
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ derivative (∏ a ∈ T, (X - C a)) = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)

Tactic:
[

Goal state after:
case a
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
T : Finset R
hT : T ∈ powersetCard (#S - k) S
⊢ derivative (∏ a ∈ T, (X - C a)) = ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a)
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ y.support ⊆ s

Tactic:
simpa [← hy, mapDomain, sum, Finset.subset_iff, single_apply, s] using
      fun i hi ↦ ⟨i, by simp [hi]⟩

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

Goal state before:
pp: σ : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
w : σ → M
hw : ∀ (s : σ), 0 ≤ w s
s : σ
f : σ →₀ ℕ
hs : f s ≠ 0
⊢ w s ≤ f s • w s

Tactic:
apply le_smul_of_one_le_left (hw s)
    exact Nat.one_le_iff_ne_zero.mpr hs

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
⊢ Associates.mk (Multiset.map normalize (Classical.choose ⋯)).prod = Associates.mk (Classical.choose ⋯).prod

Tactic:
← Associates.prod_mk,

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map Associates.mk (Multiset.map normalize (Classical.choose ⋯))).prod =
    Associates.mk (Classical.choose ⋯).prod

Tactic:
← Associates.prod_mk,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Multiset.map Associates.mk (Multiset.map normalize (Classical.choose ⋯))).prod =
    (Multiset.map Associates.mk (Classical.choose ⋯)).prod
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f ≤ n}.Finite

Tactic:
[

Goal state after:
σ : Type u_1
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f ≤ n}.Finite
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors (x * x ^ n) = normalizedFactors x + n • normalizedFactors x

Tactic:
normalizedFactors_mul h0 (pow_ne_zero _ h0),

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
ih : normalizedFactors (x ^ n) = n • normalizedFactors x
h0 : ¬x = 0
⊢ normalizedFactors x + normalizedFactors (x ^ n) = normalizedFactors x + n • normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Tactic:
by
  rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
    Multiset.nsmul_singleton]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun i ↦ (X - C i).roots) = s.val

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Finset R
⊢ (s.val.bind fun i ↦ (X - C i).roots) = s.val
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ (X - C a).roots) = s

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ (X - C a).roots) = s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ ∃ i, p ^ i ~ᵤ r

Tactic:
by
  use (normalizedFactors r).card
  have := UniqueFactorizationMonoid.prod_normalizedFactors hr
  rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (∀ (a : R), a ∉ nthRoots 2 r) ↔ ¬∃ r_1, r = r_1 ^ 2

Tactic:
mem_nthRoots (by simp : 0 < 2),

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ (∀ (a : R), ¬a ^ 2 = r) ↔ ¬∃ r_1, r = r_1 ^ 2
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
· ext
    apply mul_left_cancel₀ hp0
    rw [← normalize_apply, normalize_content, Units.val_one, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content

Tactic:
[

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

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i ↦ map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p)) a b

Tactic:
[

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
x✝¹ : a ∈ ↑p.roots.toFinset
b : R
x✝ : b ∈ ↑p.roots.toFinset
h : a ≠ b
⊢ Function.onFun IsCoprime (fun i ↦ map (algebraMap R (FractionRing R)) ((X - C i) ^ rootMultiplicity i p)) a b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (replicate (count r s) (X - C r)).prod ∣ p

Tactic:
←
        Multiset.map_replicate fun a => X - C a,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (Multiset.map (fun a ↦ X - C a) (replicate (count r s) r)).prod ∣ p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t

Tactic:
[

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ ↑(normUnit (a✝ * b✝)) = ↑(normUnit a✝) * ↑(normUnit b✝)

Tactic:
[

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : StrongNormalizationMonoid R
a✝ b✝ : R[X]
hp0 : ¬a✝.leadingCoeff = 0
hq0 : ¬b✝.leadingCoeff = 0
⊢ ↑(normUnit (a✝ * b✝)) = ↑(normUnit a✝) * ↑(normUnit b✝)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, a.factors = ↑s) ↔ a ≠ 0

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, a.factors = ↑s) ↔ a ≠ 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (map f p) ↔ IsUnit p

Tactic:
[

Goal state after:
R : Type u
k : Type y
inst✝¹ : Field R
p : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsUnit (map f p) ↔ IsUnit p
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:
exact Multiset.count_le_of_le _ h

Goal state after:
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 ∣ Associates.mk a

Tactic:
apply dvd_of_mem_factors

Goal state after:
α : 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 ∈ (Associates.mk a).factors
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 (p.content * q.content)

Tactic:
[

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ Associates.mk p ∈ (Associates.mk a).factors → Associates.mk p ∣ Associates.mk a

Tactic:
apply dvd_of_mem_factors

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

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

Tactic:
[

Goal state after:
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
⊢ p₁ * p₂ % q = p₁ % q * (p₂ % q) % 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
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x : R[X]
⊢ EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)

Tactic:
[

Goal state after:
R : Type u
k : Type y
inst✝³ : Field R
p q : R[X]
inst✝² : Field k
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x : R[X]
⊢ EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ False

Tactic:
refine (Associates.prime_mk.mpr hp).not_isUnit (isUnit_of_dvd_one ?_)

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
hg : Associates.mk a ⊓ Associates.mk b = 1
p : α
ha : p ∣ a
hb : p ∣ b
hp : Prime p
⊢ Associates.mk p ∣ 1
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
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ↑(map (algebraMap R S) (s.prod f)).roots.toFinset = ⋃ i ∈ ↑s, ↑(map (algebraMap R S) (f i)).roots.toFinset

Tactic:
rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]

Goal state after:
case a
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : s.prod f ≠ 0
⊢ ∏ i ∈ s, map (algebraMap R S) (f i) ≠ 0
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : ¬a * c = 0
cne0 : c ≠ 0
hdeg : ¬c.degree = ↑0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff)
    (↑(a.degree + c.degree), a.leadingCoeff * c.leadingCoeff)

Tactic:
· apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
by
  by_cases hp : p = 0
  · simpa [hp] using zero_notMem_normalizedFactors _
  · rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]

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

Goal state before:
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:
[

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.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ conjAlgEquiv S g = conjAlgEquiv S f ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ conjAlgEquiv S g = conjAlgEquiv S f ↔ ∃ α, ⇑f = α • ⇑g
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✝³ : EquivLike FRS R S
inst✝² : RingEquivClass FRS R S
inst✝¹ : EquivLike FAB A B
inst✝ : RingEquivClass FAB A B
f : FRS
g : FAB
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental S B ↔ Algebra.Transcendental R A

Tactic:
[

Goal state after:
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✝³ : EquivLike FRS R S
inst✝² : RingEquivClass FRS R S
inst✝¹ : EquivLike FAB A B
inst✝ : RingEquivClass FAB A B
f : FRS
g : FAB
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ Algebra.Transcendental S B ↔ Algebra.Transcendental R A
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
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ Transcendental R ((algebraMap S A) a) ↔ Transcendental R a

Tactic:
[

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ Transcendental R ((algebraMap S A) a) ↔ Transcendental R a
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S

Tactic:
[

Goal state after:
R : Type u
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Injective ⇑(algebraMap R S)
⊢ Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
⊢ IsAlgebraic (↥B) x

Tactic:
have : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl

Goal state after:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this✝ : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
this : IsScalarTower (↥A) (↥B) S
⊢ IsAlgebraic (↥B) x