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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ r • (expand R p) (X ^ q) = r • X ^ (q * p)

Tactic:
map_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
r : R
⊢ r • (expand R p) X ^ q = r • X ^ (q * p)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * (expand R p) ((expand R q) (X ^ (n + 1))) = C r * (expand R (p * q)) (X ^ (n + 1))

Tactic:
map_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * (expand R p) ((expand R q) X) ^ (n + 1) = C r * (expand R (p * q)) X ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * (expand R p) (X ^ q) ^ (n + 1) = C r * (X ^ (p * q)) ^ (n + 1)

Tactic:
map_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : (expand R p) ((expand R q) (C r * X ^ n)) = (expand R (p * q)) (C r * X ^ n)
⊢ C r * ((expand R p) X ^ q) ^ (n + 1) = C r * (X ^ (p * q)) ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ C r * (expand R 1) (X ^ (n + 1)) = C r * X ^ (n + 1)

Tactic:
map_pow,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
r : R
x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n
⊢ C r * (expand R 1) X ^ (n + 1) = C r * X ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
by
  by_cases hp : p = 0
  · rw [hp, zero_mul, trailingDegree_zero, top_add]
  by_cases hq : q = 0
  · rw [hq, mul_zero, trailingDegree_zero, add_top]
  · rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq,
    trailingDegree_eq_natTrailingDegree (mul_ne_zero hp hq), natTrailingDegree_mul hp hq]
    apply WithTop.coe_add

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p

Tactic:
rw [eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ p * C q.leadingCoeff = p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑(p.natDegree - q.natDegree) + ↑q.natDegree

Tactic:
← Nat.cast_add,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
⊢ ↑p.natDegree = ↑(p.natDegree - q.natDegree + q.natDegree)
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).Monic

Tactic:
simp only [Monic]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = 1
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:
have _wf := div_wf_lemma h hq
        have ih := modByMonic_eq_sub_mul_div
          (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) q
        unfold modByMonic divByMonic divModByMonicAux
        rw [dif_pos hq, dif_pos h]
        rw [modByMonic, dif_pos hq] at ih
        refine ih.trans ?_
        rw [divByMonic, dif_pos hq, dif_pos hq, dif_pos h, mul_add, sub_add_eq_sub_sub]

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

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommSemiring R
inst✝² : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
inst✝¹ : CharZero R
inst✝ : ExpChar R 1
⊢ (expand R 1) (contract 1 f) = f

Tactic:
rw [expand_one, contract_one]

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

Goal state before:
pp: case monomial
R : Type u
inst✝ : Semiring R
g : R[X]
m : ℕ
a : R
⊢ derivative ((monomial m) a * g) = derivative ((monomial m) a) * g + (monomial m) a * derivative g

Tactic:
induction g using Polynomial.induction_on' with

Goal state after:
case monomial.monomial
R : Type u
inst✝ : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ derivative ((monomial m) a * (monomial n) b) =
    derivative ((monomial m) a) * (monomial n) b + (monomial m) a * derivative ((monomial n) b)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case monomial.monomial.succ
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
b : R
m : ℕ
⊢ (monomial (m + 1 + n - 1)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + n - 1)) (a * (b * ↑n)) =
    (monomial (m + 1 - 1 + n)) (a * (b * ↑(m + 1))) + (monomial (m + 1 + (n - 1))) (a * (b * ↑n))

Tactic:
| succ m =>

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) ((X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f) * (expand R (p ^ n)) g)

Tactic:
map_pow,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((expand R (p ^ n)) (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * (expand R (p ^ n)) g)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((X ^ p ^ n - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * (expand R (p ^ n)) g)

Tactic:
map_pow,

Goal state after:
R : Type u
inst✝¹ : CommRing R
p n : ℕ
inst✝ : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg : f = (X - C (r ^ p ^ n)) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬((expand R (p ^ n)) g).IsRoot r
| rootMultiplicity r ((X ^ p ^ n - C r ^ p ^ n) ^ rootMultiplicity (r ^ p ^ n) f * (expand R (p ^ n)) g)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : ↑g.natDegree + ↑(f /ₘ g).natDegree = ↑f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
← Nat.cast_add,

Goal state after:
case neg
R : Type u
inst✝ : Ring R
f g : R[X]
hg : g.Monic
a✝ : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : ↑(g.natDegree + (f /ₘ g).natDegree) = ↑f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ p

Tactic:
rw [← modByMonic_add_div p q, h, zero_add]

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : p %ₘ q = 0
⊢ q ∣ q * (p /ₘ q)
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q) +
      ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) =
    ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)

Tactic:
add_comm,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      (∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)) =
    ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
        ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q) +
      1 • ((⇑derivative)^[n + 1] p * (⇑derivative)^[0] q)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
⊢ ∀ (x : Subtype (Membership.mem s)), (fun a ↦ if h : a ∈ s then p ⟨a, h⟩ else univ) ↑(id x) = p x

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
p : Subtype (Membership.mem s) → Set β
hp : ∀ (i : Subtype (Membership.mem s)), p i ∈ f ↑i
h : ⋂ i, p i ∈ ⨅ x, f ↑x
a : α
ha : a ∈ s
⊢ (fun a ↦ if h : a ∈ s then p ⟨a, h⟩ else univ) ↑(id ⟨a, ha⟩) = p ⟨a, ha⟩
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x

Tactic:
exact .iInter fun i ↦ hle i.1 i.2

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

Goal state before:
pp: α : Type u_2
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ {x | p x}.Infinite

Tactic:
simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]

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

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

Tactic:
linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
⊢ p ∣ a ∨ p ∣ b

Tactic:
have h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb) := by
          apply uif
          · exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)
          · exact fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)
          calc
            Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
              rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
            _ ~ᵤ fa.prod * fb.prod := hfa.2.symm.mul_mul hfb.2.symm
            _ = _ := by rw [Multiset.prod_add]

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
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
ha0 : a ≠ 0
hb0 : b ≠ 0
fx : Multiset α
hfx : (∀ b ∈ fx, Irreducible b) ∧ fx.prod ~ᵤ x
fa : Multiset α
hfa : (∀ b ∈ fa, Irreducible b) ∧ fa.prod ~ᵤ a
fb : Multiset α
hfb : (∀ b ∈ fb, Irreducible b) ∧ fb.prod ~ᵤ b
h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb)
⊢ p ∣ a ∨ p ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
      (∀ a ∈ q, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s).prod = q.prod → map (Quot.mk ⇑(Associated.setoid α)) s = q

Tactic:
apply Multiset.induction_on_multiset_quot q

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s_1, Irreducible a) →
      (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s_1).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
          map (Quot.mk ⇑(Associated.setoid α)) s_1 = map (Quot.mk ⇑(Associated.setoid α)) s
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
eq_comm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
⊢ ¬IsUnit q

Tactic:
intro H

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = C r * q
H : IsUnit q
⊢ False
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
by_cases h : p ∣ b

Goal state after:
case pos
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b : R
h : ¬p ∣ b
⊢ ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
g : G
hg : IsUnit g
x : R
⊢ g • x ∈ f.rootSet R → x ∈ f.rootSet R

Tactic:
obtain ⟨g, rfl⟩ := hg

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
x : R
g : Gˣ
⊢ ↑g • x ∈ f.rootSet R → x ∈ f.rootSet R
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
⊢ ∀ x ∈ Finset.range (max p.natDegree q.natDegree).succ, a ∣ p.coeff x - q.coeff x

Tactic:
intro x _

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
h : C a ∣ p - q
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
⊢ a ∣ p.coeff x - q.coeff x
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    p * q - (C (p * q).leadingCoeff * X ^ (p * q).natDegree + (p * q - C p.leadingCoeff * X ^ p.natDegree * q))

Tactic:
add_comm,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
⊢ C p.leadingCoeff ∣
    p * q - (p * q - C p.leadingCoeff * X ^ p.natDegree * q + C (p * q).leadingCoeff * X ^ (p * q).natDegree)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n ! ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : ((⇑derivative)^[rootMultiplicity t p] p).IsRoot t
⊢ False

Tactic:
simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n ! ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f - 1 = rootMultiplicity a f + rootMultiplicity a r
this : IsDomain R
⊢ False

Tactic:
add_comm,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f - 1 = rootMultiplicity a r + rootMultiplicity a f
this : IsDomain R
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ q * (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))) + p %ₘ (q * C q.leadingCoeff⁻¹) =
    p %ₘ (q * C q.leadingCoeff⁻¹) + q * C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))

Tactic:
add_comm,

Goal state after:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
h : ¬q = 0
⊢ p %ₘ (q * C q.leadingCoeff⁻¹) + q * (C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))) =
    p %ₘ (q * C q.leadingCoeff⁻¹) + q * C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ (mapRingHom f) ((X - C a) ^ rootMultiplicity a p)

Tactic:
map_pow,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ (mapRingHom f) (X - C a) ^ rootMultiplicity a p
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
A : Type u_3
B : Type u_4
inst✝² : Semiring A
inst✝¹ : CommRing B
inst✝ : IsDomain B
f : A →+* B
p : A[X]
hp0 : p ≠ 0
hpm0 : map f p = 0
⊢ ↑(map f p).roots.card ≤ p.degree

pp: case neg
A : Type u_3
B : Type u_4
inst✝² : Semiring A
inst✝¹ : CommRing B
inst✝ : IsDomain B
f : A →+* B
p : A[X]
hp0 : p ≠ 0
hpm0 : ¬map f p = 0
⊢ ↑(map f p).roots.card ≤ p.degree

Tactic:
· simp [hp0, hpm0, zero_le_degree_iff]

Goal state after:
case neg
A : Type u_3
B : Type u_4
inst✝² : Semiring A
inst✝¹ : CommRing B
inst✝ : IsDomain B
f : A →+* B
p : A[X]
hp0 : p ≠ 0
hpm0 : ¬map f p = 0
⊢ ↑(map f p).roots.card ≤ p.degree
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:
Polynomial.map_zero,

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 0 (map f x) = map f (EuclideanDomain.gcd 0 x)
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.natDegree = 0
⊢ ↑a.natDegree < ↑a.natDegree + ↑c.natDegree

Tactic:
← Nat.cast_add,

Goal state after:
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.natDegree = 0
⊢ ↑a.natDegree < ↑(a.natDegree + c.natDegree)
Module: Mathlib.Algebra.Polynomial.FieldDivision

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

Tactic:
Polynomial.map_zero,

Goal state after:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
inst✝ : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ 0 ∣ map f y ↔ 0 ∣ y
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 f = conjAlgEquiv S g

Tactic:
eq_comm

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
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
a : A
hf : Function.Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : R[X]
h1 : p ≠ 0
h2 : (aeval a) p = 0
⊢ IsAlgebraic S (g a)

Tactic:
refine ⟨p.map f, (Polynomial.map_ne_zero_iff hf).2 h1, ?_⟩

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✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : R[X]
h1 : p ≠ 0
h2 : (aeval a) p = 0
⊢ (aeval (g a)) (map (↑f) p) = 0