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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ adjoin A ↑(Subalgebra.map includeRight ⊤) = ⊤

Tactic:
rw [← Algebra.toSubmodule_eq_top, ← top_le_iff, Algebra.map_top, ← Submodule.baseChange_top,
    Submodule.baseChange_eq_span, Submodule.map_top]

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ Submodule.span A ↑((TensorProduct.mk R A B) 1).range ≤ Subalgebra.toSubmodule (adjoin A ↑includeRight.range)
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: 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✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (algebraMap R C) (toProd 1).1 + φ (toProd 1).2 = 1

Tactic:
by simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ u * x * star u ↔ 0 ≤ x

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ star_right_conjugate_nonneg h _⟩
  obtain ⟨v, hv⟩ := hu.exists_left_inv
  have := by simpa [← mul_assoc] using star_right_conjugate_nonneg h v
  rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this

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

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R f s ∧ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t

Tactic:
and_iff_right hs

Goal state after:
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
x✝¹ : { s // LinearIndepOn R id s }
s : Set (M ⧸ M')
hs : LinearIndepOn R id s
x✝ : { s // LinearIndepOn R id s }
t : Set ↥M'
ht : LinearIndepOn R id t
f : M ⧸ M' → M
hf : ∀ (b : M ⧸ M'), Submodule.Quotient.mk (f b) = b
⊢ LinearIndependent (ι := ↑s) R (Submodule.Quotient.mk ∘ fun i ↦ f ↑i)

Tactic:
simpa [Function.comp_def, hf] using! hs

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
s : Set V
hs : ⊤ ≤ span K s
⊢ range ⇑(ofSpan hs) = ⋯.extend ⋯

Tactic:
rw [coe_ofSpan, Subtype.range_coe_subtype, ofPred_mem_eq]

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

Goal state before:
pp: case right.inl
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
hs : 0 • v ∈ T
hz : 0 • v ≠ 0
⊢ v ∈ T

Tactic:
simp only [zero_smul, ne_eq, not_true] at hz

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
this : v ∉ ⊥
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
obtain ⟨g, _, hg⟩ := LinearMap.exists_extend_of_notMem (K := K) 0 this w

Goal state after:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
this : v ∉ ⊥
g : V →ₗ[K] V'
left✝ : g ∘ₗ ⊥.subtype = 0
hg : g v = w
⊢ Nontrivial (V →ₗ[K] V')
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ 0 < finrank R M ↔ ∃ x, x ≠ 0

Tactic:
← @rank_pos_iff_exists_ne_zero R M,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ 0 < finrank R M ↔ 0 < Module.rank R M
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ i, ↑(K i)

Tactic:
by rw [coe_iSup_of_directed dir]

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
s : Submodule K V
inst✝ : Free K ↥s
x✝ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
h' : ⟨v₀, hv₀⟩ = 0
⊢ v₀ = 0

Tactic:
rwa [AddSubmonoid.mk_eq_zero] at h'

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ 0 + ↑g z₁ = ↑(f.sup g h) z₂

Tactic:
← f.map_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f 0 + ↑g z₁ = ↑(f.sup g h) z₂
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr.mk
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2

Tactic:
rcases hx' with ⟨y, hy, hx'⟩

Goal state after:
case mpr.mk
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2
h : fst✝ = x_fst ∧ -snd✝ = x_snd
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2

Tactic:
rcases hx' with ⟨y, hy, hx'⟩

Goal state after:
case mpr.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ -snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ max 0 1 = 1

Tactic:
max_eq_right (Nat.zero_le _)

Goal state after:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ C a * f = a • f

Tactic:
ext
  rw [coeff_C_mul, coeff_smul, smul_eq_mul]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (p * X ^ n).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
split_ifs with h
  · rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
  · refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, mul_zero]
    exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

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

Goal state before:
pp: case h
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
a✝ : List R[A]
⊢ (↑a✝).prod.coeff.support.sup degb ≤ (Multiset.map (fun f ↦ f.coeff.support.sup degb) ↑a✝).sum

Tactic:
Multiset.map_coe,

Goal state after:
case h
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
a✝ : List R[A]
⊢ (↑a✝).prod.coeff.support.sup degb ≤ (↑(List.map (fun f ↦ f.coeff.support.sup degb) a✝)).sum
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degree = p.degree + ↑q.natDegree

Tactic:
← degree_eq_natDegree hq,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degree = p.degree + q.degree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

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

Tactic:
obtain ⟨aq, -, hq⟩ := exists_supDegree_mem_support D hq

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

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

Tactic:
coeff_sum,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ (p.sum fun a b ↦ ((C.comp f) b * X ^ a).coeff n) = f (p.coeff n)
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 q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
h✝ : Nontrivial R
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0

Tactic:
simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p * q).degree = p.degree + q.degree

Tactic:
simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
i : ι
inst✝ : NoMaxOrder (β i)
a : Lex ((i : ι) → β i)
b : β i
hb : a i < b
⊢ (fun {i} x1 x2 ↦ x1 < x2) (a i) (Function.update a i b i)

Tactic:
by rwa [Function.update_self i b]

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (X n).support = {Finsupp.single n 1}

Tactic:
rw [X, support_monomial, if_neg]

Goal state after:
case hnc
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬1 = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ coeffs 1 = {1}

Tactic:
apply Finset.Subset.antisymm coeffs_one
  simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]
  exact ⟨0, by simp⟩

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

Goal state before:
pp: case H₂
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ⇑f
x : σ →₀ ℕ
hx : f (coeff x p) = 0
⊢ coeff x p = 0

Tactic:
← f.map_zero

Goal state after:
case H₂
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective ⇑f
x : σ →₀ ℕ
hx : f (coeff x p) = f 0
⊢ coeff x p = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ vars 0 = ∅

Tactic:
rw [vars_def, degrees_zero, Multiset.toFinset_zero]

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
⊢ d ∉ (p - ((monomial d) c - (monomial d') c)).support

Tactic:
by
  classical
  rw [notMem_support_iff, coeff_sub, coeff_sub, coeff_monomial, coeff_monomial,
    if_pos rfl, if_neg hdd'.symm, sub_zero, hc, sub_self]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ degreeOf i f

Tactic:
rw [degreeOf_eq_sup i]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ f.support.sup fun m ↦ m i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
rw [totalDegree_eq]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (p.support.sup fun m ↦ (toMultiset m).card) ≤ p.degrees.card
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x ↦ id

Tactic:
by
  if hc : c = 0 then
    simp only [hc, map_zero, totalDegree_zero, zero_le]
  else
    rw [totalDegree_monomial _ hc, Function.id_def]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
⊢ False

Tactic:
have := eq_C_of_degree_le_zero hlt
    rw [IsRoot, this, eval_C] at h
    simp only [h, map_zero] at this
    exact hp this

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

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
← C_mul_X_pow_eq_self Cf,

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * g) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O g
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
hf : Function.Injective ⇑f
p : R[X]
⊢ (map f p).nextCoeff = f p.nextCoeff

Tactic:
simp only [hf, nextCoeff, natDegree_map_eq_of_injective]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
p : R[X]
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_2.succ.succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree = 1
n : ℕ
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).coeff (n + 1 + 1) = p.coeff (n + 1 + 1)

Tactic:
simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]
      rw [coeff_eq_zero_of_natDegree_lt]
      simp [hp]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p.comp (-X)).degree = p.degree

Tactic:
rw [degree_eq_natDegree (by simp [hp]), degree_eq_natDegree hp, Nat.cast_inj,
    natDegree_comp_eq_of_mul_ne_zero (by simp [hp]), natDegree_neg, natDegree_X, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : (X + C r).natDegree = 0
⊢ False

Tactic:
natDegree_X_add_C

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : 1 = 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: 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

Tactic:
simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe,
      coe_eval₂Hom, comp_apply, renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]

Goal state after:
case hC
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ (algebraMap R (MvPolynomial (Fin n) R)[X]) i = Polynomial.C (C i)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = (X + C a).natDegree + g.natDegree
⊢ False

Tactic:
natDegree_X_add_C

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = 1 + g.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ tl.prod.natDegree ≤ n * tl.length

Tactic:
refine (natDegree_list_prod_le _).trans ?_

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ n * tl.length
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
h : ∀ i ∈ t, (f i).Monic
⊢ (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum

Tactic:
revert h
  refine Multiset.induction_on t ?_ fun a t ih ht => ?_
  · simp only [Multiset.notMem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
      Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]
    rw [← C_1]
    rw [nextCoeff_C_eq_zero]
  · rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]
    exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
      monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
⊢ op ((1 - x) * ∑ i ∈ range n, x ^ i) = op (1 - x ^ n)

Tactic:
simpa using geom_sum_mul_neg (op x) n

Goal state after:
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
⊢ (p.sum fun n a ↦ (monomial n) a) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
Polynomial.sum

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
⊢ ∑ n ∈ p.support, (monomial n) (p.coeff n) ∈ 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
⊢ (p.sum fun n a ↦ (monomial n) a) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
Polynomial.sum

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n k : ℕ
hk : k ∈ ↑(range n)
⊢ ((fun n ↦ X ^ n) k).degree < ↑n

Tactic:
exact degree_X_pow_le _ |>.trans_lt <| WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m

Tactic:
sum_Ico_eq_sub _ hmn,

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ (∑ k ∈ range n, x ^ k - ∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m