mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ leadingCoeff D (p * 0) = leadingCoeff D p * leadingCoeff D 0

Tactic:
leadingCoeff_zero,

Goal state after:
case inr.inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
p : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
⊢ leadingCoeff D (p * 0) = leadingCoeff D p * 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
leadingCoeff_mul'

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff = p.leadingCoeff * q.leadingCoeff

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
⊢ f = g

Tactic:
set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
⊢ f = g
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Tactic:
refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (C (p.coeff b)).natDegree + (q ^ b).natDegree < p.natDegree * q.natDegree
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
M : Type u_1
inst✝ : CommMonoid M
n : α →₀ ℕ
f : (α →₀ ℕ) → (α →₀ ℕ) → M
⊢ ∀ (i : (α →₀ ℕ) × (α →₀ ℕ)), i ∈ antidiagonal n ↔ (Equiv.prodComm (α →₀ ℕ) (α →₀ ℕ)) i ∈ antidiagonal n

Tactic:
by simp [add_comm]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x

pp: case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y

Tactic:
· rw [← comapDomain_add_of_injective Sum.inl_injective, h, comapDomain_inl_sumElim]

Goal state after:
case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case neg
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
· convert! dvd_zero p
    rw [notMem_support_iff] at hi
    simp [hi]

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

Goal state before:
pp: case add
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q
f₁ f₂ : R[X]
h₁ : (aeval a) f₁ • m ∈ q
h₂ : (aeval a) f₂ • m ∈ q
⊢ (aeval a) (f₁ + f₂) • m ∈ q

Tactic:
simp_rw [map_add, add_smul]
    exact Submodule.add_mem q h₁ h₂

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n) * eval₂ f g p = eval₂ f g p ^ n * eval₂ f g p

Tactic:
eval₂_pow

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g p ^ n * eval₂ f g p = eval₂ f g p ^ n * eval₂ f g p
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
⊢ φ = (monomial d₀) (coeff d₀ φ)

Tactic:
ext d

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
d : σ →₀ ℕ
⊢ coeff d φ = coeff d ((monomial d₀) (coeff d₀ φ))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
⊢ eval₂ f g₁ p = eval₂ f g₂ p

Tactic:
apply Finset.sum_congr rfl

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
⊢ ∀ x ∈ p.coeff.support,
    (fun s a ↦ f a * s.prod fun n e ↦ g₁ n ^ e) x (p.coeff x) =
      (fun s a ↦ f a * s.prod fun n e ↦ g₂ n ^ e) x (p.coeff x)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
⊢ p = q

Tactic:
ext d

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
d : σ →₀ ℕ
⊢ coeff d p = coeff d q
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ (p.coeff.sum fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) = ((map f) p).coeff.sum fun s a ↦ a * s.prod fun n e ↦ g n ^ e

Tactic:
simp [map, MvPolynomial, Finsupp.sum_mapRange_index, mapRingHom]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff i P = coeff i Q

Tactic:
← coeff_X_mul i n P,

Goal state after:
R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
P Q : MvPolynomial σ R
hPQ : X n * P = X n * Q
i : σ →₀ ℕ
⊢ coeff (Finsupp.single n 1 + i) (X n * P) = coeff i Q
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (C r).coeffs ⊆ {r}

Tactic:
classical
  rw [coeffs_C]
  split <;> simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (C r).coeffs ⊆ {r}

Tactic:
by
  classical
  rw [coeffs_C]
  split <;> simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
⊢ ((killCompl hf) p).support = p.support.preimage (Finsupp.mapDomain f) ⋯

Tactic:
by
  ext x
  simp [coeff_killCompl]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ ((monomial s) a).degrees ≤ toMultiset s

Tactic:
refine (supDegree_single s a).trans_le ?_
    split_ifs
    exacts [bot_le, le_rfl]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
j : σ
hj : j ∈ x.support
⊢ (Finsupp.single (f j) (x j)) i = 0

Tactic:
simp only [mem_degrees] at hi

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ), (∃ d, coeff d φ ≠ 0 ∧ a ∈ d.support) → f a ≠ i
⊢ (Finsupp.single (f j) (x j)) i = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees

Tactic:
exact Multiset.subset_of_le degrees_mul_le

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)

Tactic:
by
  simp_rw [degreeOf_eq_sup]; exact supDegree_add_le

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ (∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k ↦ g₁ i ^ k) =
    ∑ x ∈ p₁.support, f₁ (coeff x p₁) * x.prod fun i k ↦ g₂ i ^ k

Tactic:
apply Finset.sum_congr rfl

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
⊢ ∀ x ∈ p₁.support, (f₁ (coeff x p₁) * x.prod fun i k ↦ g₁ i ^ k) = f₁ (coeff x p₁) * x.prod fun i k ↦ g₂ i ^ k
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff m p = coeff 0 p

Tactic:
← hm

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : 0 = m
⊢ coeff 0 p = coeff 0 p
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
⊢ p.trailingDegree = ↑n ↔ p.natTrailingDegree = n

Tactic:
by
  rw [natTrailingDegree, ENat.toNat_eq_iff hn]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0

Goal state after:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

pp: case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1

Tactic:
case zero =>
    by_contra
    exact h (card_support_eq_zero.mp h₁)

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : f = 0
⊢ #f.support ≤ 1

Tactic:
simp [hpz]

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

Goal state before:
pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
nd : ¬(p + q).natDegree = q.natDegree
⊢ False

Tactic:
exact nd (natDegree_add_eq_right_of_degree_lt pq)

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ (X - C x).natDegree + P.natDegree = P.natDegree + 1

Tactic:
natDegree_X_sub_C,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
⊢ 1 + P.natDegree = P.natDegree + 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (Polynomial.aevalTower (rename Option.some) (X none)).comp
      (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) =
    AlgHom.id R (MvPolynomial (Option S₁) R)

Tactic:
ext i : 2

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X i)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1

Tactic:
coeff_comp_degree_mul_degree h,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(finSuccEquiv R n) = eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i

Tactic:
ext i : 2

Goal state after:
case hC
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ((↑(finSuccEquiv R n)).comp C) i =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i).comp C) i

case hX
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X i)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X i)).coeff n✝
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
⊢ (↑p).coeff i = if i = n then 1 else 0

Tactic:
split_ifs <;> simp_all [p.2.1, p.2.2 _ (hi.lt_of_ne (.symm _))]

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

Goal state before:
pp: case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum = 0

Tactic:
· simp only [Multiset.mem_map]
      rintro _ ⟨_, _, rfl⟩
      apply monic_X_sub_C

Goal state after:
case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum = 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case a
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)

Tactic:
rw [mul_comm]

Goal state after:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ y ^ (n - 1 - (n - 1 - x✝)) * x ^ (n - 1 - x✝) = y ^ x✝ * x ^ (n - 1 - x✝)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ C (p.coeff k) * X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
C_mul'

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ C (p.coeff k) * X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
C_mul'

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ p.coeff k • X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
| p

Tactic:
rw [← eraseLead_add_C_mul_X_pow p]

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
| p.eraseLead + C p.leadingCoeff * X ^ p.natDegree
Module: Mathlib.Algebra.Ring.Action.Submonoid

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Monoid M
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction M α
a✝ b✝ : α
ha : a✝ ∈ MulAction.fixedPoints M α
hb : b✝ ∈ MulAction.fixedPoints M α
x✝ : M
⊢ x✝ • (a✝ + b✝) = a✝ + b✝

Tactic:
by rw [smul_add, ha, hb]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ C (f.coeff n) * X ^ n ∈ map C I

Tactic:
rw [mul_comm]

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ X ^ n * C (f.coeff n) ∈ map C I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ Polynomial.leadingCoeff 0 = p.coeff n

Tactic:
leadingCoeff_zero,

Goal state after:
case mp.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ 0 = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = C (x * y)

Tactic:
hy,

Goal state after:
R : Type u
inst✝ : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : C x ∈ I
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = C 1
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
rw [mul_comm]

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R[X]
hI : comap C I = I.leadingCoeff
n✝ : ℕ
ih : ∀ m < n✝, ∀ f ∈ I, f.natDegree = m → f ∈ map C (comap C I)
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n✝
h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I)
hlt : f.eraseLead.natDegree < f.natDegree
he : f.eraseLead ∈ I
⊢ f.eraseLead.natDegree < n✝

Tactic:
by simpa [hn] using hlt

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥B
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
⊢ finrank R ↥(A ⊔ B) = finrank R ↥B * finrank ↥B ↥(Algebra.adjoin ↥B ↑A)

Tactic:
by
  rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a : ℤ
⊢ |a| ≡ a [ZMOD 2]

Tactic:
by
  grind [Int.ModEq]

Goal state after:
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h✝ : ∀ (p : ℕ), Nat.Prime p → ↑p ≠ 0
p : ℕ := ringChar R
h : p = 0
this : CharP R 0
⊢ CharZero R

Tactic:
exact CharP.charP_to_charZero R

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: ⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1

Tactic:
by simp [Nat.not_prime_one]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
hg : Surjective ⇑g
⊢ Surjective (⇑(f.liftOfSurjective hf g H) ∘ ⇑f)

Tactic:
convert! hg

Goal state after:
R : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : CommRing C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f : A →ₐ[R] B
hf : Surjective ⇑f
g : A →ₐ[R] C
H : ker f.toRingHom ≤ ker g.toRingHom
hg : Surjective ⇑g
⊢ ⇑(f.liftOfSurjective hf g H) ∘ ⇑f = ⇑g
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ comap ((Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)).comp (Ideal.Quotient.mk I)) ⊥ = I ⊔ J

Tactic:
← comap_comap,

Goal state after:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ comap (Ideal.Quotient.mk I) (comap (Ideal.Quotient.mk (map (Ideal.Quotient.mk I) J)) ⊥) = I ⊔ J