mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype).range ≤ I • ⊤

Tactic:
rintro _ ⟨t, rfl⟩

Goal state after:
R : Type u_1
Q : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
I : Submodule R R
t : ↥I ⊗[R] Q
⊢ (↑(TensorProduct.lid R Q) ∘ₗ rTensor Q I.subtype) t ∈ I • ⊤
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) = quasispectrum R (b * a)

Tactic:
← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},

Goal state after:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S) (f s) = s

Tactic:
by
    rw [mem_quasispectrum_iff] at hs
    obtain (rfl | hs) := hs
    · simpa using hf 0
    · obtain ⟨r, rfl⟩ := h hs
      rw [hf r]

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} ↑(finrank R M)

Tactic:
by rw [finrank_eq_rank]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
hp : p < ⊤
⊢ ∃ f, f ≠ 0 ∧ p ≤ f.ker

Tactic:
rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩

Goal state after:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
hp : p < ⊤
v : V
hpv : v ∉ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ f.ker
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ finrank R M = 0

Tactic:
by
  rw [finrank, rank_subsingleton', map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = σ (Classical.choose ⋯) • y + σ (Classical.choose ⋯) • y

Tactic:
rw [← add_smul, ← RingHom.map_add, H]

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ Classical.choose ⋯ • x = (Classical.choose ⋯ + Classical.choose ⋯) • x
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
f : V →ₗ[K] V
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
rw [range_eq_top, ker_eq_bot, injective_iff_surjective]

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

Goal state before:
pp: R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ T (p.sum g) = p.sum fun n a ↦ T (g n a)

Tactic:
sum,

Goal state after:
R : Type u
S : Type v
T✝ : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }
A : ∀ (y : R[X]), eval₂ f x y = T y
⊢ T (∑ n ∈ p.support, g n (p.coeff n)) = p.sum fun n a ↦ T (g n a)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (p * X) = eval₂ f x p * x

Tactic:
refine _root_.trans (eval₂_mul_noncomm _ _ fun k => ?_) (by rw [eval₂_X])

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
⊢ Commute (f (X.coeff k)) x
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (p.sum fun e a ↦ f a * f r ^ e) = f (p.sum fun e a ↦ a * r ^ e)

Tactic:
sum,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = f (p.sum fun e a ↦ a * r ^ e)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = f (p.sum fun e a ↦ a * r ^ e)

Tactic:
sum,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = f (∑ n ∈ p.support, p.coeff n * r ^ n)
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 y : k[G]
⊢ (x.coeff.support.biUnion fun a ↦ (y.coeff.sum fun i n ↦ (single (a * i) (x.coeff a * n)).coeff).support) ⊆
    x.coeff.support * y.coeff.support

Tactic:
biUnion_subset

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x y : k[G]
⊢ ∀ x_1 ∈ x.coeff.support,
    (y.coeff.sum fun i n ↦ (single (x_1 * i) (x.coeff x_1 * n)).coeff).support ⊆ x.coeff.support * y.coeff.support
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✝ y : k[G]
x : G
hx : x ∈ x✝.coeff.support
⊢ (y.coeff.support.biUnion fun a ↦ (single (x * a) (x✝.coeff x * y.coeff a)).coeff.support) ⊆
    x✝.coeff.support * y.coeff.support

Tactic:
biUnion_subset

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x✝ y : k[G]
x : G
hx : x ∈ x✝.coeff.support
⊢ ∀ x_1 ∈ y.coeff.support,
    (single (x * x_1) (x✝.coeff x * y.coeff x_1)).coeff.support ⊆ x✝.coeff.support * y.coeff.support
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this✝ : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : (2 * i + 3).succ ∣ n
ml : x✝ < m
me : x✝.succ = m
d' : 2 * (i + 2) ∣ n
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2

Tactic:
by contradiction

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

Goal state before:
pp: case mp
n : ℕ
h : n.minFac = 2
⊢ n.minFac ∣ n

Tactic:
exact minFac_dvd n

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
a : R
v : ↥(map (LinearMap.fst R E F) g)
hsmul : a • ↑v ∈ map (LinearMap.fst R E F) g
hav : (a • ↑v, valFromGraph hg hsmul) ∈ g
hav' : (a • ↑v, a • valFromGraph hg ⋯) ∈ g
⊢ valFromGraph hg ⋯ = (RingHom.id R) a • valFromGraph hg ⋯

Tactic:
exact (existsUnique_from_graph @hg hsmul).unique hav hav'

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ (toFinsupp✝¹ + toFinsupp✝).coeff n = toFinsupp✝¹.coeff n + toFinsupp✝.coeff n

Tactic:
exact Finsupp.add_apply _ _ _

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
⊢ ∀ (m : M) (r : R) (x : R[M]),
    m ∉ x.coeff.support →
      r ≠ 0 →
        f (x • v) = (RingHom.id R[M]) x • f v → f ((single m r + x) • v) = (RingHom.id R[M]) (single m r + x) • f v

Tactic:
intro g r c' _nm _nz w

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁹ : Monoid M
inst✝⁸ : CommSemiring R
V : Type u_10
W : Type u_11
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : Module R[M] V
inst✝⁴ : IsScalarTower R R[M] V
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module R[M] W
inst✝ : IsScalarTower R R[M] W
f : V →ₗ[R] W
h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v
c : R[M]
v : V
g : M
r : R
c' : R[M]
_nm : g ∉ c'.coeff.support
_nz : r ≠ 0
w : f (c' • v) = (RingHom.id R[M]) c' • f v
⊢ f ((single g r + c') • v) = (RingHom.id R[M]) (single g r + c') • f v
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
m : Multiset R[A]
⊢ m.prod.coeff.support.sup degb ≤ (Multiset.map (fun f ↦ f.coeff.support.sup degb) m).sum

Tactic:
by
  induction m using Quot.inductionOn
  rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]
  exact sup_support_list_prod_le degb0 degbm _

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ C a = 0

Tactic:
rw [ha, C_0]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ (p.support.erase n).max ≤ max p.degree ↑n

Tactic:
exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)

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

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

Tactic:
rw [add_comm, degree_add_eq_left_of_degree_lt h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natDegree + q.natDegree) ≠ 0

Tactic:
rwa [coeff_mul_degree_add_degree]

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

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)

pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)

Tactic:
· rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩

Goal state after:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ (i + 1)).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ (i + 1)

Tactic:
rw [pow_succ, pow_succ, Nat.succ_mul]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < (X ^ n).degree

Tactic:
by
    rwa [degree_X_pow, Nat.cast_pos]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ R[ X] = ⊤

Tactic:
refine top_unique fun p _hp => ?_

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ R[ X]
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ f (p.coeff p.natDegree) ≠ 0

Tactic:
exact hf

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

Goal state before:
pp: case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f (comapDomain (⇑f) u ⋯) = u

Tactic:
rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add.mpr ⟨v, h.symm⟩) (by simp)))]

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

Goal state before:
pp: case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ (single a (f a)).sum g ≤ f.sum g

Tactic:
sum,

Goal state after:
case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ ∑ a_1 ∈ (single a (f a)).support, g a_1 ((single a (f a)) a_1) ≤ f.sum g
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
B : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring B
inst✝ : Algebra R B
P : R[X]
b : B
⊢ eval b (map (algebraMap R B) P) = (aeval b) P

Tactic:
by
  rw [aeval_def, eval_map]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex x j_1 = toLex (update x i a) j_1
h : toLex x j < toLex (update x i a) j
⊢ x i < a

Tactic:
dsimp at h

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex x j_1 = toLex (update x i a) j_1
h : x j < update x i a j
⊢ x i < a
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : toLex (update x i a) j < toLex x j
⊢ a < x i

Tactic:
dsimp at h

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : update x i a j < x j
⊢ a < x i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case tmul
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
s : S
n : N
⊢ X ^ k • C s ⊗ₜ[R] n = (monomial k) s ⊗ₜ[R] n

Tactic:
rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : m ∈ p.support \ q.support
⊢ m ∈ (p + q).support

Tactic:
simp only [Classical.not_not, mem_support_iff, Finset.mem_sdiff, Ne] at hm

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : ¬coeff m p = 0 ∧ coeff m q = 0
⊢ m ∈ (p + q).support
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:
rw [coeffs_C]
  split <;> 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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
⊢ eval₂ ((map f).comp C) h p = eval₂ C h ((map f) p)

Tactic:
by
  induction p using MvPolynomial.induction_on <;> simp_all

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
hl : ∀ (n : σ →₀ ℕ), coeff n p ≠ 0 → coeff n q = 0
hr : ∀ (n : σ →₀ ℕ), coeff n q ≠ 0 → coeff n p = 0
hor : ∀ (n : σ →₀ ℕ), ¬coeff n p + coeff n q = 0 → coeff n p ≠ 0 ∨ coeff n q ≠ 0
n : σ →₀ ℕ
hn : ¬coeff n q = 0
⊢ ¬coeff n p + coeff n q = 0 ∧ coeff n q = coeff n p + coeff n q

Tactic:
by simp [hr n hn, hn]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.vars = p.degrees.toFinset

Tactic:
rw [vars]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.degrees.toFinset = p.degrees.toFinset
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
this : p.degrees.card = 0
⊢ p.totalDegree = 0

Tactic:
grind [totalDegree_le_degrees_card p]

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

Goal state before:
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
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : ¬c = 0
h2 : x ∈ {d'}
⊢ x ∈ p.support.erase d ∪ {d'}

Tactic:
exact Finset.mem_union_right _ (by rwa [Finset.mem_singleton] at h2 ⊢)

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
⊢ 0 ∈ s

Tactic:
exact zero_mem _

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.natDegree ≤ 0
hn : p.coeff 0 = 0
⊢ p.natDegree ≤ 0 - 1

Tactic:
exact hf

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

Goal state before:
pp: case insert.inl
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)
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree

Tactic:
sup_eq_right.mpr H.le,

Goal state after:
case insert.inl
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)
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (s.sum f).degree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
by
  have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
  have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
  refine le_antisymm ?_ le_trailingDegree_mul
  rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ←
    ENat.natCast_add]
  apply trailingDegree_le_of_ne_zero
  rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).natTrailingDegree = n

Tactic:
rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
⊢ p.coeff n = (X ^ p.natDegree).coeff n

Tactic:
rw [coeff_X_pow]

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
⊢ p.coeff n = if n = p.natDegree then 1 else 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
⊢ b ∈ s → (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
hb

Goal state after:
case pos.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)