mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
s : R[A]
hs : s.coeff.support.Nonempty
⊢ supDegree (WithBot.some ∘ D) s = ↑(supDegree D s)

Tactic:
unfold AddMonoidAlgebra.supDegree

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
s : R[A]
hs : s.coeff.support.Nonempty
⊢ s.coeff.support.sup (WithBot.some ∘ D) = ↑(s.coeff.support.sup D)
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (single 0 1) ≤ 0

Tactic:
supDegree_single

Goal state after:
case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ (if 1 = 0 then ⊥ else D 0) ≤ 0
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
simp [ext_iff]

Goal state after:
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
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ (single a r).coeff (Function.invFun D (supDegree D (single a r))) = r

Tactic:
supDegree_single

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ (single a r).coeff (Function.invFun D (if r = 0 then ⊥ else D a)) = r
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
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  obtain rfl | hq := eq_or_ne q 0
  · simp
  obtain ⟨ap, -, hp⟩ := exists_supDegree_mem_support D hp
  obtain ⟨aq, -, hq⟩ := exists_supDegree_mem_support D hq
  simp_rw [leadingCoeff, hp, hq, ← hadd, Function.leftInverse_invFun hD _]
  exact coeff_add_of_supDegree_le hadd hD hp.le hq.le

Goal state after:
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 : ℕ
⊢ (map f p).coeff n = f (p.coeff n)

Tactic:
rw [map, eval₂_def, coeff_sum, sum]
  simp_all

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

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : φ f.leadingCoeff = 0
⊢ False

Tactic:
have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf

Goal state after:
case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : φ f.leadingCoeff = 0
u : IsUnit (φ f.leadingCoeff)
⊢ False
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
x✝ : ∃ a b a_1 b_1, (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v
a b : α →₀ ℕ
a' b' : β →₀ ℕ
h1 : a + b = x ∧ a' + b' = y
h2 : a.sumElim a' = u
h3 : b.sumElim b' = v
⊢ u + v = x.sumElim y

pp: case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x

pp: case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y

Tactic:
· rw [← h2, ← h3, ← sumElim_add, h1.left, h1.right]

Goal state after:
case refine_2
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inl u ⋯ + comapDomain Sum.inl v ⋯ = x

case refine_3
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
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
p : A[X]
⊢ (C ((algebraMap R A) r) * p).toFinsupp = (p * C ((algebraMap R A) r)).toFinsupp

Tactic:
toFinsupp_mul,

Goal state after:
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
p : A[X]
⊢ (C ((algebraMap R A) r)).toFinsupp * p.toFinsupp = p.toFinsupp * (C ((algebraMap R A) r)).toFinsupp
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
p : A[X]
⊢ r • p.toFinsupp = (C ((algebraMap R A) r) * p).toFinsupp

Tactic:
toFinsupp_mul,

Goal state after:
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
p : A[X]
⊢ r • p.toFinsupp = (C ((algebraMap R A) r)).toFinsupp * p.toFinsupp
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r (p * X - p * C r) = 0

Tactic:
eval_sub,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r (p * X) - eval r (p * C r) = 0
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g ↦ F a f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
ext a

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g ↦ F a f g
a : α
⊢ a ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a ∈ g₁.neLocus g₂
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f ↦ F a f g
⊢ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂

Tactic:
ext a

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f ↦ F a f g
a : α
⊢ a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
ext a

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (n : σ),
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R},
        eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
n

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
⊢ (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
    ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * X n) * f a * s.prod fun n e ↦ g n ^ e
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : ¬s ≤ m
⊢ coeff m (p * (monomial s) r) = 0

Tactic:
· contrapose! h
    rw [← mem_support_iff] at h
    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
    exact le_add_left le_rfl

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

Goal state before:
pp: case mul_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
⊢ ∀ (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)

Tactic:
n

Goal state after:
case mul_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
n : σ
⊢ (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p →
    (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q) =
    eval₂ C (⇑(map f) ∘ g) ((map f) p + (map f) q)

Tactic:
eval₂_add

Goal state after:
case add
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p q : MvPolynomial S₂ R
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
hq : (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q) =
    eval₂ C (⇑(map f) ∘ g) ((map f) p) + eval₂ C (⇑(map f) ∘ g) ((map f) q)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.degrees = 0 ↔ p.support ⊆ {0}

Tactic:
Finset.subset_singleton_iff',

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.degrees = 0 ↔ ∀ b ∈ p.support, b = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ p * (monomial i) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp only [mem_coeffsIn, coeff_mul_monomial']

Goal state after:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
⊢ ∀ (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Tactic:
n

Goal state after:
case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
n : σ
⊢ constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: case inr.inl
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h1 : x ∈ if c = 0 then ∅ else {d}
⊢ x ∈ p.support.erase d ∪ {d'}

Tactic:
split_ifs at h1

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : c = 0
h1 : x ∈ ∅
⊢ x ∈ p.support.erase d ∪ {d'}

case neg
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : ¬c = 0
h1 : x ∈ {d}
⊢ x ∈ p.support.erase d ∪ {d'}
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
⊢ cons (t 0) t.tail = t

Tactic:
ext a

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
a : Fin (n + 1)
⊢ (cons (t 0) t.tail) a = t a
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
⊢ s = 0

Tactic:
ext a

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
c : cons y s = 0
a : Fin n
⊢ s a = 0 a
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ (rename f) ((aeval fun i ↦ Option.elim' 0 X (partialInv f i)) p) = p

Tactic:
by
      change (rename f).toRingHom.comp _ p = RingHom.id _ p
      refine hom_congr_vars ?_ ?_ ?_
      · ext1
        simp [algebraMap_eq]
      · intro i hip _
        rcases hf hip with ⟨i, rfl⟩
        simp [partialInv_left hfi]
      · rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.trailingDegree = ⊤

Tactic:
by simp [h]

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

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

Tactic:
by
  rw [add_comm]
  exact coeff_add_eq_left_of_lt pn

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ ((monomial n) 1).trailingDegree = ↑n

Tactic:
trailingDegree_monomial one_ne_zero

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n = ↑n
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
⊢ C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt N) f.natDegree + (revAt O) g.natDegree)) =
    C f.leadingCoeff * (C g.leadingCoeff * (X ^ (revAt O) g.natDegree * X ^ (revAt N) f.natDegree))

Tactic:
←
        pow_add (X : R[X]),

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
⊢ C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt N) f.natDegree + (revAt O) g.natDegree)) =
    C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt O) g.natDegree + (revAt N) f.natDegree))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := ⋯
g : MvPolynomial σ R →+* R[X] := ⋯
⊢ (f.comp g).comp C = C

Tactic:
ext a

Goal state after:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun x ↦ Polynomial.X
a : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((f.comp g).comp C) a) = coeff m✝ (C a)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos.refine_2
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
⊢ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree) ≤ s.sup' hs fun i ↦ (f i).degree

Tactic:
· rw [Finset.sup'_le_iff]
        intro b hb
        simp only [Finset.le_sup'_iff, Function.comp_apply]
        by_cases hb' : f b = 0
        · refine ⟨x, hx, ?_⟩
          contrapose! hx'
          simpa [← Nat.cast_withBot, hb', degree_eq_bot] using! hx'
        exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p = 0
⊢ p.comp q = 0

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ((↑(finSuccEquiv R n).symm).comp (Polynomial.C.comp C)) x = C x

Tactic:
rw [RingHom.comp_apply]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(finSuccEquiv R n).symm ((Polynomial.C.comp C) x) = C x
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h : (∑ x_1, if i = k x_1 then x x_1 else 0) ≠ 0
⊢ ∃ a, k a = i

Tactic:
obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h
    exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩

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

Goal state before:
pp: case hX.none
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
      (X none) =
    ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X none)

Tactic:
simp [finSuccEquiv_apply, optionEquivLeft_apply]

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

Goal state before:
pp: case hX.some
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
i : σ
⊢ ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
      (X (Option.some i)) =
    ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X (Option.some i))

Tactic:
simp [finSuccEquiv_apply, optionEquivLeft_apply]

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

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin (n + 1)
hij : i < j
⊢ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_ofPred_eq]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)

Goal state after:
case succ.refine_1
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i j : Fin (n + 1)
hij : i < j
hi : i ∈ Set.range Fin.castSucc
⊢ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ f (n + 1) n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n

Tactic:
f_last,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + (∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1

Tactic:
by
  rw [pow_mul]; exact sub_one_dvd_pow_sub_one (x ^ m) n

Goal state after: