mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
f : Filter α
⊢ f.ker = ∅ ↔ f.kerᶜ ∈ f

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
f : Filter α
⊢ f.ker = ∅ → f.kerᶜ ∈ f

case mpr
α : Type u_2
f : Filter α
⊢ f.kerᶜ ∈ f → f.ker = ∅
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ

Tactic:
constructor

Goal state after:
case mp
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ

case mpr
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
u v : α → M
⊢ mapDomain f (u + v) = mapDomain f u + mapDomain f v

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
f : α → β
inst✝¹ : AddCommMonoid M
inst✝ : TendstoCofinite f
u v : α → M
x✝ : β
⊢ mapDomain f (u + v) x✝ = (mapDomain f u + mapDomain f v) x✝
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst✝² : AddCommMonoid M
inst✝¹ : TendstoCofinite f
inst✝ : DistribSMul R M
r : R
v : α → M
⊢ mapDomain f (r • v) = r • mapDomain f v

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst✝² : AddCommMonoid M
inst✝¹ : TendstoCofinite f
inst✝ : DistribSMul R M
r : R
v : α → M
x✝ : β
⊢ mapDomain f (r • v) x✝ = (r • mapDomain f v) x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case e_f
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ Associates.mk ∘ normalize = Associates.mk

Tactic:
ext

Goal state after:
case e_f
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
x✝ : α
⊢ (Associates.mk ∘ normalize) x✝ = Associates.mk x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

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

Tactic:
exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

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

Goal state before:
pp: σ : 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 : σ →₀ ℕ
⊢ (weight w) f = 0 ↔ f = 0

Tactic:
constructor

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 : σ →₀ ℕ
⊢ (weight w) f = 0 → f = 0

case mpr
σ : 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 : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
h : Multiset.prod 0 ~ᵤ a
⊢ (∀ b ∈ 0, Prime b) → ∃ p, a ~ᵤ p ∧ 0 = {p}

Tactic:
exact (ha.not_isUnit (associated_one_iff_isUnit.1 (Associated.symm h))).elim

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * (s.erase q).prod * q

Tactic:
mul_right_comm _ _ q,

Goal state after:
case refine_1
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
f : Multiset α
ha : Irreducible a
pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : DecidableEq α
p : α
s : Multiset α
a✝ : s.prod ~ᵤ a → (∀ b ∈ s, Prime b) → ∃ p, a ~ᵤ p ∧ s = {p}
u : αˣ
hu : (p ::ₘ s).prod * ↑u = a
hs : ∀ b ∈ p ::ₘ s, Prime b
hs0 : ¬s = 0
q : α
hq : q ∈ s
⊢ a = p * ↑u * q * (s.erase q).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalize = Associates.out ∘ Associates.mk

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
x✝ : α
⊢ normalize x✝ = (Associates.out ∘ Associates.mk) x✝
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case succ
σ : Type u_5
g f : σ →₀ ℕ
hgf : g ≤ g + f
IH : degree g ≤ degree (g + f) → ∃ g_1 ≤ g + f, degree g_1 = degree g
hn : degree g + 1 ≤ degree (g + f)
i : σ
hi : i ∈ f.support
⊢ ∃ g_1 ≤ g + f, degree g_1 = degree g + 1

Tactic:
exact ⟨g + .single i 1, add_le_add_right (by simp; grind) _, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x ∣ y → normalizedFactors x ≤ normalizedFactors y

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ p ∈ normalizedFactors x → Prime p ∧ p ∣ x

case mpr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
p x : α
hx : x ≠ 0
⊢ Prime p ∧ p ∣ x → p ∈ normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x ↔ ¬IsUnit x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x → ¬IsUnit x

case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < normalizedFactors x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y → normalizedFactors x < normalizedFactors y

case mpr
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x < normalizedFactors y → DvdNotUnit x y
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
a x : α
⊢ x ∈ normalizedFactors a ↔ ↑f x ∈ normalizedFactors (f a)

Tactic:
rcases eq_or_ne a 0 with rfl | ha
    · simp
    · simp [mem_normalizedFactors_iff' ha,
        mem_normalizedFactors_iff' (EmbeddingLike.map_ne_zero_iff.mpr ha), map_dvd_iff_dvd_symm,
        MulEquiv.irreducible_iff, he]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x p = eval x q

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x q = eval x q
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
constructor

Goal state after:
case succ.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ ¬p.coeff a = 0 → ∃ a_2, ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1

case succ.mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ (∃ a_1, ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support = p.support

Tactic:
ext

Goal state after:
case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).coeff = fun x ↦ r * p.coeff x

Tactic:
ext

Goal state after:
case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).support = p.support

Tactic:
ext

Goal state after:
case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (C r * p).coeff = fun x ↦ r * p.coeff x

Tactic:
ext

Goal state after:
case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ x ∈ p.support, p.coeff x = 0) → p = 0

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p = 0 → ∀ x ∈ p.support, p.coeff x = 0
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

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ ↑(normUnit p.content) = ↑1
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
a : T
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).aroots S = n • {0}

Tactic:
rw [← C_mul_X_pow_eq_monomial, aroots_C_mul_X_pow ha]

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
⊢ (fun x ↦ eval x p) ⁻¹' {a} = (p - C a).rootSet R

Tactic:
ext

Goal state after:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ C a
x✝ : R
⊢ x✝ ∈ (fun x ↦ eval x p) ⁻¹' {a} ↔ x✝ ∈ (p - C a).rootSet R
Module: Mathlib.RingTheory.Polynomial.Content

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

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ (∀ (i : ℕ), r ∣ p.coeff i) → r ∣ p.content
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case h
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ IsRelPrime a b ∧ 1 * a = a ∧ 1 * b = b

Tactic:
constructor

Goal state after:
case h.left
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ IsRelPrime a b

case h.right
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝¹ a : R
a_unit : IsUnit a
a✝ : a ≠ 0
b : R
⊢ 1 * a = a ∧ 1 * b = b
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
| eval t ((⇑derivative)^[m] p)

Tactic:
rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
| eval t ((⇑derivative)^[m] ((X - C t) ^ m * (p /ₘ (X - C t) ^ m)))
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t
      (∑ k ∈ range m.succ,
        m.choose k • ((⇑derivative)^[m - k] ((X - C t) ^ m) * (⇑derivative)^[k] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)

Tactic:
eval_finsetSum,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ∑ i ∈ range m.succ,
      eval t (m.choose i • ((⇑derivative)^[m - i] ((X - C t) ^ m) * (⇑derivative)^[i] (p /ₘ (X - C t) ^ m))) =
    m ! • eval t (p /ₘ (X - C t) ^ m)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ (∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x) ↔ x ∣ y

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ (∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x) → x ∣ y

case mpr
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ x ∣ y → ∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
by norm_cast

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

Goal state before:
pp: case right.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
constructor

Goal state after:
case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree

case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ q.roots = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
⊢ p.roots.card ≤ 1

Tactic:
obtain hp | ⟨x, hx⟩ := p.roots.empty_or_exists_mem

Goal state after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
hp : p.roots = 0
⊢ p.roots.card ≤ 1

case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hirr : Irreducible p
x : R
hx : x ∈ p.roots
⊢ p.roots.card ≤ 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) ↔
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p) →
    ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
⊢ (∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q) →
    ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
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:
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]

Goal state after:
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
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)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α) (a : Irreducible p), Multiset.count ⟨p, a⟩ sa = Multiset.count ⟨p, a⟩ sb
h_sa : a.factors = ↑sa
h_sb : b.factors = ↑sb
⊢ sa = sb

Tactic:
ext

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a ↔ p ∣ a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → p ∣ a

case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → ⟨Associates.mk p, ⋯⟩ ∈ factors' a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
constructor

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

case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → Associates.mk p ∈ (Associates.mk a).factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ Associates.mk a ⊓ Associates.mk b = 1 → ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d

case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d) → Associates.mk a ⊓ Associates.mk b = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p ∣ q → p.content ∣ q.content ∧ p.primPart ∣ q.primPart

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ p.content ∣ q.content ∧ p.primPart ∣ q.primPart → p ∣ q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
k : ℕ
⊢ (a ^ k).factors = k • a.factors

Tactic:
by
  induction k with
  | zero => rw [zero_nsmul, pow_zero]; exact factors_one
  | succ n h => rw [pow_succ, succ_nsmul, factors_mul, h]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
⊢ ⇑(algebraMap R A) = ⇑(aeval a) ∘ ⇑C

Tactic:
ext

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
a : A
inj : Function.Injective ⇑(aeval a)
x✝ : R
⊢ (algebraMap R A) x✝ = (⇑(aeval a) ∘ ⇑C) x✝