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

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ inl ((algebraMap S R) s) * inl r✝ + inl ((algebraMap S R) s) * ↑a✝ =
    inl r✝ * inl ((algebraMap S R) s) + ↑a✝ * inl ((algebraMap S R) s)

Tactic:
inl_mul_inl,

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ inl ((algebraMap S R) s * r✝) + inl ((algebraMap S R) s) * ↑a✝ =
    inl r✝ * inl ((algebraMap S R) s) + ↑a✝ * inl ((algebraMap S R) s)
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ inl ((algebraMap S R) s * r✝) + inl ((algebraMap S R) s) * ↑a✝ =
    inl r✝ * inl ((algebraMap S R) s) + ↑a✝ * inl ((algebraMap S R) s)

Tactic:
inl_mul_inl,

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ inl ((algebraMap S R) s * r✝) + inl ((algebraMap S R) s) * ↑a✝ =
    inl (r✝ * (algebraMap S R) s) + ↑a✝ * inl ((algebraMap S R) s)
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl (s • 1) * inl r✝ + inl (s • 1) * ↑a✝

Tactic:
inl_mul_inl,

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl (s • 1 * r✝) + inl (s • 1) * ↑a✝
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : 0 ≤ r
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b

Tactic:
rw [StarOrderedRing.nonneg_iff] at hr

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹¹ : Semiring R
inst✝¹⁰ : PartialOrder R
inst✝⁹ : StarRing R
inst✝⁸ : StarOrderedRing R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
hr : r ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
a b : A
hab : a ≤ b
⊢ r • a ≤ r • b
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
⊢ S = ⊤

Tactic:
set bS := Basis.ofVectorSpace K S with bS_eq
  have : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K S) := by
    simpa [bS] using bS.linearIndependent.linearIndepOn_id.image
      (f := Submodule.subtype S) (by simp)
  set b := Basis.extend this with b_eq
  let i2 : Fintype (((↑) : S → V) '' Basis.ofVectorSpaceIndex K S) :=
    (LinearIndependent.set_finite_of_isNoetherian this).fintype
  have : (↑) '' Basis.ofVectorSpaceIndex K S = this.extend (Set.subset_univ _) :=
    Set.eq_of_subset_of_card_le (this.subset_extend _)
      (by
        rw [Set.card_image_of_injective _ Subtype.coe_injective, ← finrank_eq_card_basis bS, ←
            finrank_eq_card_basis b, h])
  rw [← b.span_eq, b_eq, Basis.coe_extend, Subtype.range_coe, ← this, ← Submodule.coe_subtype,
    span_image]
  have := bS.span_eq
  rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this
  rw [this, Submodule.map_top (Submodule.subtype S), range_subtype]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ finrank K V = 1 ↔ Nonempty (Basis ι K V)

Tactic:
constructor
  · intro h
    exact ⟨Module.basisUnique ι h⟩
  · rintro ⟨b⟩
    simpa using finrank_eq_card_basis b

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
hk : ¬k = 1
⊢ Commute (f (X.coeff k)) x

Tactic:
simp [coeff_X_of_ne_one hk]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ (x * single a r).coeff.support ⊆ image (fun x ↦ x * a) x.coeff.support

Tactic:
grw [support_coeff_mul_subset, coeff_single, support_single_subset]
  change image₂ _ _ _ ⊆ _
  rw [image₂_singleton_right]

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

Goal state before:
pp: case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ max q 1 = q

Tactic:
exact Nat.max_eq_left h.one_lt.le

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

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

Tactic:
obtain rfl | h := eq_or_ne p 0

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
⊢ degree 0 = ↑n ↔ natDegree 0 = n

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
obtain rfl | h := eq_or_ne p 0

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
⊢ AddMonoidAlgebra.supDegree id (toFinsupp 0) = natDegree 0

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ (n + 1)).degree ≤ (n + 1) • p.degree

Tactic:
by grw [pow_succ, succ_nsmul, degree_mul_le, degree_pow_le]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: 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
hD : Function.Injective D
hp : p ≠ 0
⊢ Function.invFun D (supDegree D p) ∈ p.coeff.support

Tactic:
obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D hp
  rwa [he, Function.leftInverse_invFun hD]

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

Goal state before:
pp: case h₀.inr.inr
R : Type u
inst✝ : Semiring R
f g : R[X]
df' dg' : ℕ
hdf : f.natDegree ≤ df'
hdf' : df' ≤ df'
hdg : g.natDegree ≤ dg'
hdg' : dg' ≤ dg'
hmem : (df', dg') ∈ antidiagonal (df' + dg')
hne : (df', dg') ≠ (df', dg')
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
exact (hne rfl).elim

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (p - q).degree = p.degree

Tactic:
← degree_neg q

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).degree = q.degree

Tactic:
← degree_neg q

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - C a ≠ 0

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg C a]
  exact X_pow_add_C_ne_zero hn _

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ < embDomain f g₂ ↔ g₁ < g₂

Tactic:
by
  simp [lt_iff_le_not_ge, embDomain_le_embDomain_iff_le]

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = eval₂ (algebraMap R A) (φ X) p

Tactic:
by
  rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]

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

Goal state before:
pp: case monomial
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
n : ℕ
t : R
hmq : (aeval a) (C t * X ^ n) • m ∈ q
⊢ (aeval a) (C t * X ^ (n + 1)) • m ∈ q

Tactic:
| monomial n t hmq =>

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial 0) a * X s ^ n

Tactic:
C_apply

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ (monomial 0) a * X s ^ n = (monomial 0) a * X s ^ n
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ ∏ x ∈ s.support, X x ^ s x = (monomial s) 1

Tactic:
by
  simp only [monomial_eq, map_one, one_mul, Finsupp.prod]

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

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

Tactic:
coeff_monomial,

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ d_1 ∈ φ.support, d_1 = d
⊢ coeff d φ = if d = d then coeff d φ else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

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

Tactic:
coeff_monomial,

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
d : σ →₀ ℕ
hd : d ≠ d₀
⊢ 0 = if d₀ = d then coeff d₀ φ else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ coeff d ((monomial (Finsupp.indicator s fun i x_1 ↦ x i)) 1) =
    if d = Finsupp.indicator s fun i x_1 ↦ x i then 1 else 0

Tactic:
coeff_monomial,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ (if (Finsupp.indicator s fun i x_1 ↦ x i) = d then 1 else 0) =
    if d = Finsupp.indicator s fun i x_1 ↦ x i then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Tactic:
rw [Ne, eq_zero_iff]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ (map f) ((rename g) (C a)) = (rename g) ((map f) (C a))

Tactic:
simp only [map_C, rename_C]

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

Goal state before:
pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = (rename Subtype.val) q) →
      (∃ s q_1, q = (rename Subtype.val) q_1) → ∃ s q_1, p + q = (rename Subtype.val) q_1

Tactic:
rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩

Goal state after:
case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ ∃ s_1 q_1, (rename Subtype.val) p + (rename Subtype.val) q = (rename Subtype.val) q_1
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 : σ → R
p : MvPolynomial σ R
⊢ f ((eval g) p) = eval₂ f (⇑f ∘ g) p

Tactic:
rw [← p.map_id, eval_map, eval₂_comp_right]

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

Goal state before:
pp: case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) ((monomial (Finsupp.mapDomain f u)) r) = coeff d ((monomial u) r)

Tactic:
coeff_monomial,

Goal state after:
case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = coeff d ((monomial u) r)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ degreeOf n f = f.support.sup fun m ↦ m n

Tactic:
classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - (coeff d ((monomial d) c) - coeff d ((monomial d') c)) = 0

Tactic:
coeff_monomial,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - ((if d = d then c else 0) - coeff d ((monomial d') c)) = 0
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - ((if d = d then c else 0) - coeff d ((monomial d') c)) = 0

Tactic:
coeff_monomial,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ coeff d p - ((if d = d then c else 0) - if d' = d then c else 0) = 0
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hp : x ∈ p.support
hxd : x = d
⊢ x ∈ p.support.erase d ∪ {d'}

pp: case neg
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hp : x ∈ p.support
hxd : ¬x = d
⊢ x ∈ p.support.erase d ∪ {d'}

Tactic:
· exact absurd (hxd ▸ hx) hd_not

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hp : x ∈ p.support
hxd : ¬x = d
⊢ x ∈ p.support.erase d ∪ {d'}
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
by
  by_cases c : i = j
  · simp only [c, if_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, degreeOf_def, degrees_X]

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

Goal state before:
pp: case neg
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : S₁
hx : ↑(C a).coeffs ⊆ range ⇑f
h : ¬a = 0
⊢ C a ∈ range ⇑(map f)

Tactic:
simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars

Tactic:
by
  classical
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih

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₁
inst✝ : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
⊢ φ = aeval (⇑φ ∘ X)

Tactic:
by
  ext i
  simp

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₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
⊢ φ.comp (aeval f) = aeval fun i ↦ φ (f i)

Tactic:
by
  ext i
  simp

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
this : f✝ (b + coeff a f) ∈ s
⊢ f✝ (coeff a f) ∈ s

Tactic:
MvPolynomial.notMem_support_iff.1 ha,

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
this : f✝ (b + coeff a f) ∈ s
⊢ f✝ 0 ∈ s
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Tactic:
rintro rfl
    simp

Goal state after:
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
σ : Type u_2
inst✝ : Unique σ
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C a)) = Polynomial.C a

Tactic:
Polynomial.eval₂_C,

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
σ : Type u_2
inst✝ : Unique σ
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (C a) = Polynomial.C a
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
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n) * X default ^ (p + 1)) =
    Polynomial.C n * Polynomial.X ^ (p + 1)

Tactic:
Polynomial.eval₂_C,

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
σ : Type u_2
inst✝ : Unique σ
p✝ : R[X]
p : ℕ
n : R
x✝ :
  eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C n * Polynomial.X ^ p)) =
    Polynomial.C n * Polynomial.X ^ p
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (C n * X default ^ (p + 1)) = Polynomial.C n * Polynomial.X ^ (p + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0

Tactic:
by
  rcases eq_or_ne p 0 with h | h
  · simp [h]
  simp only [h, or_false]
  refine ⟨fun h2 ↦ ?_, degree_map_eq_of_leadingCoeff_ne_zero f⟩
  have h3 : natDegree (map f p) = natDegree p := by simp_rw [natDegree, h2]
  have h4 : map f p ≠ 0 := by
    rwa [ne_eq, ← degree_eq_bot, h2, degree_eq_bot]
  rwa [← coeff_natDegree, ← coeff_map, ← h3, coeff_natDegree, ne_eq, leadingCoeff_eq_zero]

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

Goal state before:
pp: case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).eraseLead.coeff n -
      ((monomial ((X - C x) * P).eraseLead.natDegree) ((X - C x) * P).eraseLead.leadingCoeff).coeff n =
    ((X - C x) * P.eraseLead).coeff n

Tactic:
coeff_monomial,

Goal state after:
case neg.inl
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ (((X - C x) * P).eraseLead.coeff n -
      if ((X - C x) * P).eraseLead.natDegree = n then ((X - C x) * P).eraseLead.leadingCoeff else 0) =
    ((X - C x) * P.eraseLead).coeff n