mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
⊢ IsUnit a ∨ IsUnit b

Tactic:
simp only [Nat.isUnit_iff]

Goal state after:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
⊢ a = 1 ∨ b = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : CharZero R
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x

Tactic:
by rw [zero_dvd_iff, ← Nat.cast_zero, Nat.cast_inj]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case right
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 g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx⟩) ∈ f.graph

Tactic:
rw [hxy] at hx

Goal state after:
case right
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 g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx✝⟩) ∈ f.graph
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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 g : E →ₗ.[R] F
h : f ≤ g
⊢ f.graph ≤ g.graph

Tactic:
by
  intro x hx
  rw [mem_graph_iff] at hx ⊢
  obtain ⟨y, hx⟩ := hx
  use ⟨y, h.1 y.2⟩
  simp only [hx, true_and]
  convert! hx.2 using 1
  refine (h.2 ?_).symm
  simp only [hx.1]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (C x * X ^ k + C y * X ^ m).coeff k ≠ 0 ∧ (C x * X ^ k + C y * X ^ m).coeff m ≠ 0

Tactic:
coeff_add,

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (C x * X ^ k).coeff k + (C y * X ^ m).coeff k ≠ 0 ∧ (C x * X ^ k).coeff m + (C y * X ^ m).coeff m ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k ≠ 0 ∧
    (C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff m ≠ 0 ∧ (C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff n ≠ 0

Tactic:
coeff_add,

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (C x * X ^ k).coeff k + (C y * X ^ m).coeff k + (C z * X ^ n).coeff k ≠ 0 ∧
    (C x * X ^ k).coeff m + (C y * X ^ m).coeff m + (C z * X ^ n).coeff m ≠ 0 ∧
      (C x * X ^ k).coeff n + (C y * X ^ m).coeff n + (C z * X ^ n).coeff n ≠ 0
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
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

Tactic:
dsimp at *

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) = c' • f v
⊢ f ((single g r + c') • v) = (single g r + c') • f v
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✝⁹ : 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
⊢ f (c • v) = (RingHom.id R[M]) c • f v

Tactic:
by
    refine induction c ?_ ?_
    · simp
    · intro g r c' _nm _nz w
      dsimp at *
      simp only [add_smul, f.map_add, w, single_eq_algebraMap_mul_of, ← smul_smul]
      rw [algebraMap_smul, algebraMap_smul, f.map_smul, of_apply, h g v]

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

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

Tactic:
← tsub_add_cancel_of_le h,

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : n ≤ d
⊢ (p * X ^ n).coeff (d - n + n) = p.coeff (d - n + n - n)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else p.coeff n✝) = (p + C (a - p.coeff n) * X ^ n).coeff n✝

Tactic:
coeff_add,

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else p.coeff n✝) = p.coeff n✝ + (C (a - p.coeff n) * X ^ n).coeff n✝
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
coeff_add,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree + q.coeff p.natDegree ≠ 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 q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ (p + q).coeff (Function.invFun D (supDegree D p)) = leadingCoeff D p

Tactic:
coeff_add,

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 q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ (p.coeff + q.coeff) (Function.invFun D (supDegree D p)) = leadingCoeff D p
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
⊢ Function.invFun D (supDegree D p) ∈ p.coeff.support

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

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

Goal state before:
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 ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ supDegree D (∑ i ∈ s, f i) ≠ ⊥

Tactic:
have (k) (hk : k ∈ s) (hne : k ≠ i) : supDegree D (f k) < supDegree D (f i) :=
    ((le_sup hk).trans_eq he).lt_of_ne (hd.ne hk hi hne)

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 ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ k ∈ s, k ≠ i → supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (∑ i ∈ s, f i) ≠ ⊥
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
aq : A
hq : supDegree D q = D aq
⊢ (p * q).coeff (Function.invFun D (D ap + D aq)) =
    p.coeff (Function.invFun D (D ap)) * q.coeff (Function.invFun D (D aq))

Tactic:
← hadd,

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 (D (ap + aq))) =
    p.coeff (Function.invFun D (D ap)) * q.coeff (Function.invFun D (D aq))
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a✝ : Nontrivial R
⊢ (X ^ n).natDegree ≤ n

Tactic:
Polynomial.natDegree_X_pow

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a✝ : Nontrivial R
⊢ n ≤ n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X ^ n + C r).coeff n = 1

Tactic:
coeff_add,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X ^ n).coeff n + (C r).coeff n = 1
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
⊢ (map f p).nextCoeff = f p.nextCoeff

Tactic:
grind [nextCoeff, natDegree_map_of_leadingCoeff_ne_zero, coeff_map]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ single i a ≤ 0 ↔ a ≤ 0

Tactic:
by classical exact Pi.single_nonpos

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p q r✝ : R[X]
r : R
⊢ (toFinsuppIso R).toFun ((algebraMap R R[X]) r) = (algebraMap R R[ℕ]) r

Tactic:
dsimp

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

Goal state before:
pp: R : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p : R[X]
f : A →ₐ[R] B
a : A
⊢ f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p

Tactic:
simp only [eval₂_eq_sum, sum_def]
  simp only [map_sum, map_mul, map_pow, AlgHom.commutes]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
c : R[X]ˣ
p : R[X]
⊢ C ((↑c).coeff 0) * p = ↑c * p

Tactic:
← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
c : R[X]ˣ
p : R[X]
⊢ ↑c * p = ↑c * p
Module: Mathlib.Algebra.MvPolynomial.Basic

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

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

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₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (fun s a ↦ f a * s.prod fun n e ↦ g₁ n ^ e) C (p.coeff C) = (fun s a ↦ f a * s.prod fun n e ↦ g₂ n ^ e) C (p.coeff C)

Tactic:
dsimp

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (f (p.coeff C) * C.prod fun n e ↦ g₁ n ^ e) = f (p.coeff C) * C.prod fun n e ↦ g₂ n ^ e
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ (fun n e ↦ g₁ n ^ e) i (C i) = (fun n e ↦ g₂ n ^ e) i (C i)

Tactic:
dsimp

Goal state after:
case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ g₁ i ^ C i = g₂ i ^ C i
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddLeftStrictMono (α i)
x✝³ x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex (x✝³ + x✝²)) a) ((ofLex (x✝³ + x✝¹)) a)

Tactic:
dsimp

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddLeftStrictMono (α i)
x✝³ x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (ofLex x✝³) a + (ofLex x✝²) a < (ofLex x✝³) a + (ofLex x✝¹) a
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddRightStrictMono (α i)
f x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex (Function.swap (fun x1 x2 ↦ x1 + x2) f x✝²)) a)
    ((ofLex (Function.swap (fun x1 x2 ↦ x1 + x2) f x✝¹)) a)

Tactic:
dsimp

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : LinearOrder ι
inst✝² : (i : ι) → AddMonoid (α i)
inst✝¹ : (i : ι) → LinearOrder (α i)
inst✝ : ∀ (i : ι), AddRightStrictMono (α i)
f x✝² x✝¹ : Lex (Π₀ (i : ι), α i)
x✝ : x✝² < x✝¹
a : ι
lta : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j a → (ofLex x✝²) j = (ofLex x✝¹) j
ha : (fun {i} ↦ (fun x x1 x2 ↦ x1 < x2) i) ((ofLex x✝²) a) ((ofLex x✝¹) a)
⊢ (ofLex x✝²) a + (ofLex f) a < (ofLex x✝¹) a + (ofLex f) a
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
i : σ
⊢ ((killCompl hf).comp (rename f)) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

Tactic:
dsimp

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ (killCompl hf) ((rename f) (X i)) = X i
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : 0 ≠ r
⊢ ↑(Finsupp.mapDomain f s).support ⊆ range f

Tactic:
apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support

Goal state after:
case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : 0 ≠ r
⊢ ↑(Finset.image f s.support) ⊆ range f
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ p.degrees ≤ (p + q).degrees

Tactic:
by
  classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption

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

Goal state before:
pp: case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
i : σ
⊢ f i ∈ ↑(aeval f).range

Tactic:
use X i, by aesop

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

Goal state before:
pp: case monomial_add.refine_2
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
i : σ →₀ ℕ
this : f✝ (coeff i ((monomial a) b + f)) ∈ s
⊢ f✝ (coeff i f) ∈ s

Tactic:
coeff_add,

Goal state after:
case monomial_add.refine_2
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
i : σ →₀ ℕ
this : f✝ (coeff i ((monomial a) b) + coeff i f) ∈ s
⊢ f✝ (coeff i f) ∈ s
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ c • x ∈ {p | p.degrees ≤ s}

Tactic:
dsimp

Goal state after:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ (c • x).degrees ≤ s
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 + q).coeff m

Tactic:
coeff_add,

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 + q.coeff m
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
rwa [coeff_mul_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ∈ f.support.erase f.natDegree
⊢ a < f.natDegree

Tactic:
mem_erase

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
a : ℕ
h : a ≠ f.natDegree ∧ a ∈ f.support
⊢ a < f.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g

Tactic:
by
  ext
  simp only [coeff_add, coeff_reflect]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else (p + q).coeff n) = (p.eraseLead + q).coeff n

Tactic:
coeff_add,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = (p.eraseLead + q).coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = (p.eraseLead + q).coeff n

Tactic:
coeff_add,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = p.eraseLead.coeff n + q.coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else (p + q).coeff n) = (p + q.eraseLead).coeff n

Tactic:
coeff_add,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = (p + q.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = (p + q.eraseLead).coeff n

Tactic:
coeff_add,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = p.coeff n + q.eraseLead.coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
· left
    apply eraseLead_natDegree_lt h

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)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
    intro x hx
    simp [H x hx]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
⊢ False

Tactic:
by
    have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
    rw [A, eval₂_C] at hz
    simp only [inj (p.coeff 0) hz, map_zero] at A
    exact hp A

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ coeff (Finsupp.single default (d default)) ((uniqueAlgEquiv R σ).symm P) =
    P.coeff ((Finsupp.single default (d default)) default)

Tactic:
← coeff_uniqueAlgEquiv R,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ ((uniqueAlgEquiv R σ) ((uniqueAlgEquiv R σ).symm P)).coeff (d default) =
    P.coeff ((Finsupp.single default (d default)) default)