mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ (p * (n + 1))!.factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1

Tactic:
← prod_Ico_id_eq_factorial,

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ (∏ x ∈ Ico 1 (p * (n + 1) + 1), x).factorization p = (p * n)!.factorization p + (n + 1).factorization p + 1
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (p * (n + 1)).factorization p) =
    (p * n)!.factorization p + ((n + 1).factorization p + 1)

Tactic:
← prod_Ico_id_eq_factorial,

Goal state after:
n p : ℕ
hp : Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), m.factorization p = 0
⊢ ∑ i ∈ Ico 1 (p * n + 1), i.factorization p +
      (∑ k ∈ Ico (p * n + 1) (p * (n + 1)), k.factorization p + (p * (n + 1)).factorization p) =
    (∏ x ∈ Ico 1 (p * n + 1), x).factorization p + ((n + 1).factorization p + 1)
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + emultiplicity p (n + 1) =
    ↑(∑ i ∈ Ico 1 b, n / p ^ i) + ↑(#({i ∈ Ico 1 b | p ^ i ∣ n + 1}))

Tactic:
←
          emultiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb

Goal state after:
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i ∈ Ico 1 b, n / p ^ i) + emultiplicity p (n + 1) = ↑(∑ i ∈ Ico 1 b, n / p ^ i) + emultiplicity p n.succ
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ emultiplicity p (p * n)! ≠ ⊤ → emultiplicity p (p * (n + 1))! = emultiplicity p (p * n)! + emultiplicity p (n + 1) + 1

Tactic:
← prod_Ico_id_eq_factorial,

Goal state after:
n p : ℕ
hp : Prime p
hp' : _root_.Prime p
h0 : 2 ≤ p
h1 : 1 ≤ p * n + 1
h2 : p * n + 1 ≤ p * (n + 1)
h3 : p * n + 1 ≤ p * (n + 1) + 1
h4 : ∀ m ∈ Ico (p * n + 1) (p * (n + 1)), emultiplicity p m = 0
⊢ emultiplicity p (∏ x ∈ Ico 1 (p * n + 1), x) ≠ ⊤ →
    emultiplicity p (∏ x ∈ Ico 1 (p * (n + 1) + 1), x) =
      emultiplicity p (∏ x ∈ Ico 1 (p * n + 1), x) + emultiplicity p (n + 1) + 1
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
⊢ e ∣ b → e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
heb

Goal state after:
case hd
a b : ℕ
ha_pos : a ≠ 0
hb_pos : b ≠ 0
e : ℕ
hea : e ∣ a
heb : e ∣ b
⊢ e ∣ (a.factorization ⊓ b.factorization).prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Multiplicity

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ multiplicity p (p ^ n)! = ∑ i ∈ range n, p ^ i

Tactic:
by
  rw [← ENat.natCast_inj, ← (Nat.finiteMultiplicity_iff.2
      ⟨hp.ne_one, (p ^ n).factorial_pos⟩).emultiplicity_eq_multiplicity]
  induction n with
  | zero => simp [hp.emultiplicity_one]
  | succ n h =>
    rw [pow_succ', hp.emultiplicity_factorial_mul, h, Finset.sum_range_succ, ENat.natCast_add]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
nontriviality R
  exact (degree_modByMonic_lt _ hq).le

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

Tactic:
subset_iff,

Goal state after:
case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, x ∈ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) → x ∈ antidiagonal (n * p)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x ↦ (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

Tactic:
simp_rw [subset_iff, mem_image, mem_antidiagonal]; rintro _ ⟨x, rfl, rfl⟩; simp_rw [add_mul]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Tactic:
coeff_expand hp.bot_lt,

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ (f.coeff (x, y).1 * if p ∣ (x, y).2 then g.coeff ((x, y).2 / p) else 0) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ ((expand R p) (contract p f)).coeff n = f.coeff n

Tactic:
coeff_expand hp.bot_lt,

Goal state after:
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then (contract p f).coeff (n / p) else 0) = f.coeff n
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t.succ] p = 0

Tactic:
Function.iterate_succ_apply

Goal state after:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
⊢ (⇑derivative)^[t] (derivative p) = 0
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) (map (iterateFrobenius R p k) ((expand R (p * p ^ k)) f)) =
    map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k)) f))

Tactic:
iterateFrobenius_one

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree

Tactic:
← degree_add_divByMonic hq (not_lt.1 hpq),

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this✝ : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < q.degree + (p /ₘ q).degree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree + (q - f /ₘ g).degree = (r - f %ₘ g).degree

Tactic:
rw [h₂, degree_mul']; simpa [Monic.def.1 hg]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (∀ (x : ↥S), IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), IsAlgebraic R x

Tactic:
refine forall_congr' fun x => exists_congr fun p => and_congr Iff.rfl ?_

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = p.coeff (n + 1) + a * q.coeff (n + 1)

Tactic:
rw [← p.modByMonic_add_div (X - C a)]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
n : ℕ
a✝ : Nontrivial R
this : (X - C a).Monic
q : R[X] := p /ₘ (X - C a)
⊢ q.coeff n = (p %ₘ (X - C a) + (X - C a) * (p /ₘ (X - C a))).coeff (n + 1) + a * q.coeff (n + 1)
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s✝ : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
s : Set (Set α)
⊢ ∀ {x y : Set α},
    x ∈ sInter '' {t | t.Finite ∧ t ⊆ s} →
      y ∈ sInter '' {t | t.Finite ∧ t ⊆ s} → ∃ z ∈ sInter '' {t | t.Finite ∧ t ⊆ s}, z ⊆ x ∩ y

Tactic:
by
    rintro _ _ ⟨a, ⟨fina, suba⟩, rfl⟩ ⟨b, ⟨finb, subb⟩, rfl⟩
    exact ⟨⋂₀ (a ∪ b), mem_image_of_mem _ ⟨fina.union finb, union_subset suba subb⟩,
        (sInter_union _ _).subset⟩

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:
by
  rw [modByMonic_eq_sub_mul_div, eval₂_sub, eval₂_mul, hx, zero_mul, sub_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
p : α × β → Prop
s : Set β
⊢ {a | ∀ b ∈ s, (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f

Tactic:
simp only [mem_ofPred_eq]

Goal state after:
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
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)

Tactic:
by
  rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩
  exact ha.mono fun a ha => hb.mono fun b hb => h ha hb

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
x : α × γ
hx : t (x.1, x.1) ∧ s x.2
⊢ p ((x.1, x.1), x.2)

Tactic:
simp only [hst hx.1 hx.2]

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
x : α × γ
hx : t x.1 ∧ s (x.2, x.2)
⊢ p (x.1, x.2, x.2)

Tactic:
simp only [hst hx.1 hx.2]

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

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

Tactic:
rcases ha₁.exists_right_inv with ⟨k, hk⟩

Goal state after:
case cons.inl
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, IsUnit y ∨ Prime y) → 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
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
k : M₀
hk : c * k = 1
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}
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
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (Associates.out ∘ Associates.mk) (normalizedFactors (x * y)) =
    Multiset.map (Associates.out ∘ Associates.mk) (normalizedFactors x + normalizedFactors y)

Tactic:
←
    Multiset.map_map Associates.out,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y))) =
    Multiset.map (Associates.out ∘ Associates.mk) (normalizedFactors x + normalizedFactors y)
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
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map (Associates.out ∘ Associates.mk) (normalizedFactors x + normalizedFactors y) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))

Tactic:
← Multiset.map_map Associates.out

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalize = Associates.out ∘ Associates.mk
⊢ Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) =
    Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a

pp: case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a

Tactic:
· rw [hcases]
    exact dvd_zero p

Goal state after:
case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr.cons
α : 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✝
⊢ normalizedFactors (a✝ ::ₘ s✝).prod = (Multiset.map normalizedFactors (a✝ ::ₘ s✝)).sum

Tactic:
rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
x : R
hx : x ∈ nthRootsFinset n 1
f : F
⊢ f x ∈ nthRootsFinset n (f 1)

Tactic:
exact map_mem_nthRootsFinset hx _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : Associates α
hx : ¬x✝ = 0
x : Associates α
⊢ Associates.mk (Classical.choose ⋯ x) = id x

Tactic:
Classical.choose_spec mk_surjective.hasRightInverse x

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x✝ : Associates α
hx : ¬x✝ = 0
x : Associates α
⊢ x = id 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
r : T
⊢ (map (algebraMap T S) (X - C r)).roots = {(algebraMap T S) r}

Tactic:
Polynomial.map_sub,

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
r : T
⊢ (map (algebraMap T S) X - map (algebraMap T S) (C r)).roots = {(algebraMap T S) r}
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:
Polynomial.map_sub,

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 - map (algebraMap R (FractionRing R)) (C i)) ^ rootMultiplicity i p)
    a b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ prod ⊤ = 0

Tactic:
Associates.prod_top

Goal state after:
case top.coe
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ prod ⊤ = 0

Tactic:
Associates.prod_top

Goal state after:
case coe.top
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ map f (X - C a) ^ rootMultiplicity (f a) (map f p) ∣ map f p

Tactic:
Polynomial.map_sub,

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ (map f X - map f (C a)) ^ rootMultiplicity (f a) (map f p) ∣ map f p
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ r.cancelLeads s
⊢ r ∣ s

Tactic:
← rprim.dvd_primPart_iff_dvd s0

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ r.cancelLeads s
⊢ r ∣ s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
h : q = p
⊢ q.count a.factors = p.count a.factors * q.count p.factors

pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ q.count a.factors = p.count a.factors * q.count p.factors

Tactic:
· rw [h, count_self hp, mul_one]

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h✝ : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
h : ¬q = p
⊢ q.count a.factors = p.count a.factors * q.count p.factors
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
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0
⊢ (Polynomial.aeval r) ((Polynomial.aeval f) p) = 0

Tactic:
← aeval_comp,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval r) (p.comp f) = 0
⊢ (Polynomial.aeval r) ((Polynomial.aeval f) p) = 0
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
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0

Tactic:
← aeval_comp,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval f) p = 0
⊢ (Polynomial.aeval r) (p.comp f) = 0
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₂
⊢ (∃ y, ∀ (x : M), f x = g (y • x)) ↔ ∃ α, ∀ (x : M), f x = α • g x

Tactic:
LinearMapClass.map_smul_of_tower g

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ Function.Surjective ⇑(aeval ⟨s, ⋯⟩)

Tactic:
rw [← AlgHom.range_eq_top, _root_.eq_top_iff]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ ⊤ ≤ (aeval ⟨s, ⋯⟩).range