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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ centralizer R ↑(centralizer R s)
h₂ : x✝ ∈ centralizer R ↑(centralizer R s)
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
← SetLike.mem_coe,

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ ↑(centralizer R ↑(centralizer R s))
h₂ : x✝ ∈ ↑(centralizer R ↑(centralizer R s))
⊢ x✝¹ * x✝ = x✝ * x✝¹
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
hd : Module.rank K V ≤ 1
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v

Tactic:
rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : finrank F ↥S = 1
inst✝ : Free F ↥S
⊢ S = ⊥

Tactic:
by
  refine Subalgebra.eq_bot_of_rank_le_one ?_
  rw [finrank, toNat_eq_one] at h
  rw [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
⊢ g ≤ f.sup g h

Tactic:
refine ⟨le_sup_right, fun z₁ z₂ hz => ?_⟩

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₂
⊢ ↑g z₁ = ↑(f.sup g h) z₂
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
f g h : E →ₛₗ.[σ] F
⊢ f + g + h = f + (g + h)

Tactic:
ext x y hxy
    · simp only [add_domain, inf_assoc]
    · simp only [add_apply, add_assoc]

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

Goal state before:
pp: case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : ∀ p_1 ∈ ps ++ [p], ∀ (k : ℕ), Commute (f (p_1.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod

Tactic:
simp only [List.forall_mem_append, List.forall_mem_singleton] at hf

Goal state after:
case append_singleton
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
p : R[X]
ihp : (∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x) → eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod
hf : (∀ x_1 ∈ ps, ∀ (k : ℕ), Commute (f (x_1.coeff k)) x) ∧ ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x (ps ++ [p]).prod = (List.map (eval₂ f x) (ps ++ [p])).prod
Module: Mathlib.Algebra.Polynomial.Eval.Defs

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

Tactic:
by
  rw [map, eval₂_mul_noncomm]
  exact fun k => (commute_X _).symm

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

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

Tactic:
rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]

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

Goal state before:
pp: case inl
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
p : ℕ
hchar : CharP R p
h : Nat.Prime p
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

pp: case inr
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hchar : CharP R 0
⊢ CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p

Tactic:
exacts [Or.inr ⟨p, Fact.mk h, hchar⟩, Or.inl (charP_to_charZero R)]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
y : F
x : E
hx : x ∈ f.domain
h : ↑f ⟨x, hx⟩ = y
⊢ ∃ x, (x, y) ∈ f.graph

Tactic:
use x

Goal state after:
case h
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
y : F
x : E
hx : x ∈ f.domain
h : ↑f ⟨x, hx⟩ = y
⊢ (x, y) ∈ f.graph
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: 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✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Monoid N
r : R
⊢ (↑↑singleOneRingHom).toFun ((algebraMap R A) r) = (algebraMap R A[M]) r

Tactic:
by ext; simp; rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * q).coeff n = ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2

Tactic:
by
  rcases p with ⟨p⟩; rcases q with ⟨q⟩
  simp_rw [← ofFinsupp_mul, coeff]
  exact AddMonoidAlgebra.coeff_mul_antidiag p q n _ Finset.mem_antidiagonal

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

Tactic:
exact Finset.le_sup (mem_support_iff.2 h)

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ p.degree = ⊥

Tactic:
Subsingleton.elim p 0,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ degree 0 = ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ p.natDegree = 0

Tactic:
Subsingleton.elim p 0,

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ natDegree 0 = 0
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 : q.degree > (p + q).degree
⊢ (p + q).coeff q.natDegree = 0

Tactic:
exact coeff_natDegree_eq_zero_of_degree_lt hlt

Goal state after:
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:
rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp

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

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0

Tactic:
pow_succ',

Goal state after:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff * p.leadingCoeff ^ n ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
pow_succ',

Goal state after:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ

Tactic:
pow_succ',

Goal state after:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p * p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

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

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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q

Tactic:
· simp_rw [leadingCoeff_zero, mul_zero, leadingCoeff_zero]

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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : p ≠ 0
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
rw [leadingCoeff_mul']
      exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

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

Goal state before:
pp: case succ
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D (p ^ (n + 1)) = (n + 1) • supDegree D p

Tactic:
pow_succ',

Goal state after:
case succ
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D (p * p ^ n) = (n + 1) • supDegree D p
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
p : A[X]
⊢ (mapAlg A C) p = (mapAlg B C) ((mapAlg A B) p)

Tactic:
simp [mapAlg_eq_map, map_map, IsScalarTower.algebraMap_eq A B C]

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, a < b

Tactic:
by
    let ⟨b, hb⟩ := exists_gt (a i)
    classical
    exact ⟨Function.update a i b, i, fun j hj =>
      (Function.update_of_ne hj.ne b a).symm, by rwa [Function.update_self i b]⟩

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:
pow_succ',

Goal state after:
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 * X ^ n)) • m ∈ q
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
simp [X_pow_eq_monomial, eval₂_monomial f g]

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

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

Tactic:
exact eval₂_one _ _

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
have : (x.neLocus y : Set ι).WellFoundedOn r := (x.neLocus y).finite_toSet.wellFoundedOn

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt✝ : x < y
hle : ⇑x ≤ ⇑y
j : ι
hlt : x j < y j
this : (↑(x.neLocus y)).WellFoundedOn r
i : { x_1 // x_1 ∈ ↑(x.neLocus y) }
hi : i ∈ {i | x ↑i < y ↑i}
hl : ∀ x_1 ∈ {i | x ↑i < y ↑i}, ¬Subrel r (fun x_2 ↦ x_2 ∈ ↑(x.neLocus y)) x_1 i
k : ι
hk : r k ↑i
⊢ y k ≤ x k

Tactic:
exact of_not_not fun h ↦ hl ⟨k, mem_neLocus.2 (ne_of_not_le h).symm⟩ ((hle k).lt_of_not_ge h) hk

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

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

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

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

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsRegular (X n)

Tactic:
suffices IsLeftRegular (X n : MvPolynomial σ R) from
    ⟨this, this.right_of_commute <| Commute.all _⟩
  intro P Q (hPQ : (X n) * P = (X n) * Q)
  ext i
  rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]

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
⊢ (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a = 0

Tactic:
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 : MvPolynomial σ R
i : σ
⊢ i ∈ p.degrees ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support

Tactic:
by
  classical
  simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset]

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
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ ((rename f) ((killCompl hf) p)).support ⊆ p.support

Tactic:
rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ {x ∈ p.support | x ∈ range (Finsupp.mapDomain f)} ⊆ p.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m ↦ m j) + 1 = f.support.sup fun m ↦ m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ ∃ b ∈ f.support, x j + 1 ≤ ((fun m ↦ m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) b

Tactic:
use x

Goal state after:
case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m ↦ m j) + 1 = f.support.sup fun m ↦ m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x ∈ f.support ∧ x j + 1 ≤ ((fun m ↦ m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg
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 : ¬constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]

Goal state after:
case neg
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 : ¬constantCoeff p = 0
⊢ (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = f (constantCoeff p)

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 : ¬constantCoeff p = 0
⊢ ∀ b ∈ p.support, b ≠ 0 → (f (coeff b p) * b.prod fun i k ↦ g i ^ k) = 0

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 : ¬constantCoeff p = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (d.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
refine not_not.mp (mt h ?_)

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (d.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ ¬(d.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ ?m.25

Tactic:
by simpa using min_mem_image_coe <| support_nonempty.2 hp

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

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
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
hb' : ¬f b = 0
⊢ ↑(f b).natDegree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb

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

Goal state before:
pp: case neg
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
he₂ : ¬((X - C x) * P).eraseLead = 0
h₂ : #(X - C x).support = 2
hmul : #((X - C x) * P).support ≤ #(X - C x).support * #P.support
⊢ #((X - C x) * P).support ≤ 2

Tactic:
rw [h₂] at hmul

Goal state after:
case neg
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
he₂ : ¬((X - C x) * P).eraseLead = 0
h₂ : #(X - C x).support = 2
hmul : #((X - C x) * P).support ≤ 2 * #P.support
⊢ #((X - C x) * P).support ≤ 2
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case succ
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree ^ (k + 1) * q.natDegree

Tactic:
pow_succ',

Goal state after:
case succ
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
k : ℕ
IH : (p.comp^[k] q).natDegree = p.natDegree ^ k * q.natDegree
⊢ p.natDegree * (p.natDegree ^ k * q.natDegree) = p.natDegree * p.natDegree ^ k * q.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
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
⊢ ((X - C x) * P).eraseLead.eraseLead.natDegree < n

Tactic:
grw [eraseLead_natDegree_le, eraseLead_natDegree_le]

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
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
⊢ ((X - C x) * P).natDegree - 1 - 1 < n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ p.comp (-X) = 0 ↔ p = 0

Tactic:
simp [← leadingCoeff_eq_zero]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivLeft R S₁).symm (Polynomial.C (X x)) = X (Option.some x)

Tactic:
simp [optionEquivLeft]

Goal state after: