mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M

Tactic:
rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
inst✝⁷ : NonUnitalRing R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : StarRing R✝
inst✝⁴ : StarOrderedRing R✝
p q : R✝
R : Type u_3
inst✝³ : NonUnitalRing R
inst✝² : LinearOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
⊢ star r = r

Tactic:
by
    obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by grind
    · exact hr.star_eq
    · simpa using hr.star_eq

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

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)

Tactic:
rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small]

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ ⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R (M × M₁)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
lt : finrank R ↥s < finrank R M
⊢ s < ⊤

Tactic:
← finrank_top R M

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
lt : finrank R ↥s < finrank R ↥⊤
⊢ s < ⊤
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R ↥⊤ ≤ Fintype.card ι

Tactic:
← hv

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R ↥(span R (range v)) ≤ Fintype.card ι
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
i : m
⊢ (bW.sumQuot bQ).repr ↑(bW i) = Finsupp.single (Sum.inl i) 1

Tactic:
rw [← Module.Basis.apply_eq_iff, sumQuot_inl]

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

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = K ∙ v

Tactic:
by_contra heq

Goal state after:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False
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✝⁴ : StarRing R
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
S : NonUnitalSubalgebra R A
x y : A
hx : x ∈ star S.carrier
hy : y ∈ star S.carrier
⊢ x * y ∈ star S.carrier

Tactic:
simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier]
        using (star_mul x y).symm ▸ mul_mem hy hx

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

Goal state before:
pp: case refine_1
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'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
x : ↥p
⊢ (g ∘ₗ p.subtype) x = f x

Tactic:
have := LinearPMap.supSpanSingleton_apply_mk_of_mem ⟨p, f⟩ y hv x.2

Goal state after:
case refine_1
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'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
x : ↥p
this : ↑({ domain := p, toFun := f }.supSpanSingleton v y hv) ⟨↑x, ⋯⟩ = ↑{ domain := p, toFun := f } ⟨↑x, ⋯⟩
⊢ (g ∘ₗ p.subtype) x = f x
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
this : f (b j) = 0
⊢ f (b j) = (f (b i) • b.coord i) (b j)

Tactic:
by
      simp [Finsupp.single_eq_of_ne h, this]

Goal state after:
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
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
a✝ : Nontrivial M
⊢ Module.Finite R M ∧ Finite ι

Tactic:
obtain ⟨s, hs⟩ := id h

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
a✝ : Nontrivial M
s : Finset (ι →₀ M)
hs : span R ↑s = ⊤
⊢ Module.Finite R M ∧ Finite ι
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
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
x✝¹ x✝ : V
⊢ x✝¹ = x✝

Tactic:
← hv

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
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ ∃ v, ∀ (w : V), ∃ c, c • v = w

Tactic:
rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r a : R
hr : r ≠ 0
⊢ ¬(C r).IsRoot a

Tactic:
simpa using hr

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

Goal state before:
pp: case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
⊢ n.minFac = 2

Tactic:
refine ub.eq_or_lt.resolve_right fun h' => ?_

Goal state after:
case mpr
n : ℕ
h : 2 ∣ n
ub : n.minFac ≤ 2
lb : 0 < n.minFac
h' : n.minFac < 2
⊢ False
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: case single
R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
m : M
a : A
⊢ φ₁ (single m a) = φ₂ (single m a)

Tactic:
simpa [← map_mul] using congr($(single_one_right m) * $single_one_left a)

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : M →* A
a : M
b : R
⊢ ((lift R A M) F) (single a b) = b • F a

Tactic:
by
  rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
⊢ IsMaxFilter g l a

Tactic:
refine hle.mp (h.mono fun x hf hgf => ?_)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a
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✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ (f.coeff.support + g.coeff.support).sup degb ≤ f.coeff.support.sup degb + g.coeff.support.sup degb

Tactic:
Finset.sup_add_le

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
⊢ ∀ x ∈ f.coeff.support, ∀ y ∈ g.coeff.support, degb (x + y) ≤ f.coeff.support.sup degb + g.coeff.support.sup degb
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (X ^ n * p).coeff (d + n) = p.coeff d

Tactic:
by
  rw [(commute_X_pow p n).eq, coeff_mul_X_pow]

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

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

Tactic:
rw [(commute_X_pow p n).eq, coeff_mul_X_pow']

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ p.natDegree = q.natDegree

Tactic:
by unfold natDegree; rw [h]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
· rw [eq_C_of_degree_le_zero hpd, ← C_add, natDegree_C, natDegree_C]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree

Tactic:
rw [degree_eq_natDegree hp, Nat.cast_pos, ← natDegree_C a] at hpd
    exact natDegree_add_eq_left_of_natDegree_lt hpd

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
HEq : p.degree = q.degree
hlt : max q.degree q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0

Tactic:
max_self

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 0 • p.degree

Tactic:
zero_nsmul

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 0
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
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ max q.degree q.degree = q.degree

Tactic:
max_self

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ q.degree = q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.leadingCoeff ^ n ≠ 0

Tactic:
← leadingCoeff_pow,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p ^ n).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ ↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree

Tactic:
rw [sub_eq_sub_iff_add_eq_add]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ ↑p₁.natDegree + ↑q₂.natDegree = ↑p₂.natDegree + ↑q₁.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : 1 ≠ 0
⊢ 0 = 0 • p.degree

Tactic:
zero_nsmul

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : 1 ≠ 0
⊢ 0 = 0
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
h : ¬p = 0
⊢ ¬leadingCoeff D p = 0

Tactic:
rw [leadingCoeff, ← Ne, ← Finsupp.mem_support_iff]

Goal state after:
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
h : ¬p = 0
⊢ Function.invFun D (supDegree D p) ∈ p.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ supDegree D (p - q) < supDegree D p ∨ p = q

Tactic:
by
  rw [or_iff_not_imp_right]
  refine fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_
  · rw [hd, sup_idem]
  · rw [← sub_eq_zero, ← leadingCoeff_eq_zero hD, leadingCoeff] at he
    refine fun h => he ?_
    rwa [h, coeff_sub, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = X + C (p.coeff 0)

Tactic:
by
  rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).degree = 1

Tactic:
degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha,

Goal state after:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X).degree = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ (X ^ n - C r).natDegree = n

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
h : f = g
⊢ f.neLocus f = ∅

Tactic:
by simp only [neLocus, Ne, not_true, Finset.filter_false]

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
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ (killCompl hf) ((monomial s) c) = 0

Tactic:
by
  rw [killCompl, aeval_monomial, Finsupp.prod]
  apply mul_eq_zero_of_right
  apply Finset.prod_eq_zero ha
  simp [hs, zero_pow (Finsupp.mem_support_iff.mp ha)]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
⊢ coeff d p ≠ 0

Tactic:
coeff,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
⊢ p.coeff d ≠ 0
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
p : MvPolynomial σ R
⊢ φ ((aeval f) p) = (aeval fun i ↦ φ (f i)) p

Tactic:
← comp_aeval,

Goal state after:
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
p : MvPolynomial σ R
⊢ φ ((aeval f) p) = (φ.comp (aeval f)) p
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬coeff 0 p = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0

Tactic:
coeff,

Goal state after:
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬p.coeff 0 = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0
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 : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : coeff 0 p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty

Tactic:
coeff,

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : p.coeff 0 = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support.Nonempty
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 : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬coeff 0 p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty

Tactic:
coeff,

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬p.coeff 0 = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support.Nonempty
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = p.coeff m + q.coeff m

Tactic:
natDegree_le_iff_coeff_eq_zero.mp qn _ hm,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = p.coeff m + 0
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).natTrailingDegree

Tactic:
natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h),

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * X ^ n).support.min' ⋯
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0

Tactic:
rw [hp, zero_mul]

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

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = (revAt (n + n')) n + (revAt (o + o')) o

Tactic:
repeat' rw [revAt_le (le_add_right rfl.le)]

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (optionEquivLeft R S₁) ((monomial m) r) = (Polynomial.monomial (m none)) ((monomial m.some) r)

Tactic:
rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) ((monomial m.some) r)

case h_zero
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁), (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ 0 = 1

case h_add
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ ∀ (o : Option S₁) (m₁ m₂ : ℕ),
    (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ (m₁ + m₂) =
      (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₁ * (o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m₂
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
rw [Monic, leadingCoeff_mul, leadingCoeff_C,
    mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]

Goal state after:
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
  · 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]
    rfl
  · refine Fin.cases ?_ ?_ i <;> simp [optionEquivLeft_apply, finSuccEquiv]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ (-f).reverse = -f.reverse

Tactic:
rw [reverse, reverse, reflect_neg, natDegree_neg]

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

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : (∀ p ∈ tl, p.degree ≤ n) → tl.sum.degree ≤ n
hl : hd.degree ≤ n ∧ ∀ a ∈ tl, a.degree ≤ n
⊢ (hd :: tl).sum.degree ≤ n

Tactic:
rcases hl with ⟨hhd, htl⟩

Goal state after:
case cons
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : (∀ p ∈ tl, p.degree ≤ n) → tl.sum.degree ≤ n
hhd : hd.degree ≤ n
htl : ∀ a ∈ tl, a.degree ≤ n
⊢ (hd :: tl).sum.degree ≤ n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ m ∈ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support ↔ m ∈ {m ∈ f.support | m 0 = i}

Tactic:
Finset.mem_filter,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ m ∈ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support ↔ m ∈ f.support ∧ m 0 = i
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ r * r ^ (p ^ a - 1) - r ∣ r * r ^ (p ^ b - 1) - r

Tactic:
← mul_sub_one,

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ r * (r ^ (p ^ a - 1) - 1) ∣ r * r ^ (p ^ b - 1) - r