mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₛₗ.[σ] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
⊢ f (x + y) = f x + f y

Tactic:
set x' := inclusion hpx.1 ⟨x, (P x).2⟩

Goal state after:
case w.refine_1
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₛₗ.[σ] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
x' : ↥p.domain := (inclusion ⋯) ⟨↑x, ⋯⟩
⊢ f (x + y) = f x + f y
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝ : Semiring k
f : k[G]
⊢ f ∈ Submodule.span k (of' k G '' ↑f.coeff.support)

Tactic:
by
  simp [of', ← supported_eq_span_single, mem_supported]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
i : ℤ
⊢ (↑i).comp p = ↑i

Tactic:
cases i <;> simp

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < n

Tactic:
by rw [h0, mul_zero]; decide

Goal state after:
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 : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
rw [mem_domain_iff]
  exact ⟨y, h⟩

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

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ p.coeff (i, j).1 * (X ^ n).coeff (i, j).2 = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Goal state after:
case h₀.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ p.coeff x.1 * (X ^ n).coeff x.2 = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Goal state after:
case neg.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ (Multiset.map (fun f ↦ f.coeff.support.inf degt) m).sum ≤ m.prod.coeff.support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_coeff_multisetProd_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
  · exact degt0
  · exact degtm _ _

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

Goal state before:
pp: i : ℤ
R : Type u_1
inst✝ : Ring R
⊢ (↑i).coeff 0 = ↑i

Tactic:
cases i <;> simp

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

Goal state before:
pp: case inl.inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
⊢ (0 ^ 0).natDegree = 0 * natDegree 0

Tactic:
simp [*]

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

Goal state before:
pp: case inl.inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
hn : n ≠ 0
⊢ (0 ^ n).natDegree = n * natDegree 0

Tactic:
simp [*]

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]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ¬p ^ n = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case bot
m : WithBot ℕ
h : ⊥ < m
⊢ ⊥ + 1 ≤ m

Tactic:
simp only [WithBot.bot_add, bot_le]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
⊢ ¬p ∣ q

Tactic:
by
  by_contra hcontra
  exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
simp [*]

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 = C (p.coeff 1) * X + C (p.coeff 0)

Tactic:
← eq_X_add_C_of_natDegree_le_one hnd.le

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = p
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
rw [hp2, zero_mul, coeff_zero]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval x (map g (map f p)) = eval x (map (g.comp f) p)

Tactic:
map_map

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
p : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval x (map (g.comp f) p) = eval x (map (g.comp f) p)
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:
natDegree_X_pow_add_C

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ n = n
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
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 [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]

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:
by
      dsimp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x✝ : β
⊢ x✝ ∈ ↑y.support → x✝ ∈ ↑(y + w).support

Tactic:
by simp; grind

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

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ C ↑0 = ↑0

Tactic:
simp [*]

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

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
a✝ : C ↑n✝ = ↑n✝
⊢ C ↑(n✝ + 1) = ↑(n✝ + 1)

Tactic:
simp [*]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : i ∉ (Finsupp.indicator t fun i x_1 ↦ x i).support
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1

Tactic:
rw [Finsupp.mem_support_iff, ne_eq, not_not] at hi'

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
i : σ
hi : i ∈ t
hi' : (Finsupp.indicator t fun i x_1 ↦ x i) i = 0
⊢ X i ^ (Finsupp.indicator t fun i x_1 ↦ x i) i = 1
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
⊢ (eval x) (s • p) = s * (eval x) p

Tactic:
rw [smul_eq_C_mul, (eval x).map_mul, eval_C]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval (⇑(eval g) ∘ f)) p = (eval g) (eval₂ C f p)

Tactic:
rw [eval₂_comp_left (eval g)]
  unfold eval; simp only [coe_eval₂Hom]
  congr with a; simp

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
a✝ : R
⊢ eval₂ f g ((rename k) (C a✝)) = eval₂ f (g ∘ k) (C a✝)

Tactic:
simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ q✝ : MvPolynomial σ R
a✝¹ : eval₂ f g ((rename k) p✝) = eval₂ f (g ∘ k) p✝
a✝ : eval₂ f g ((rename k) q✝) = eval₂ f (g ∘ k) q✝
⊢ eval₂ f g ((rename k) (p✝ + q✝)) = eval₂ f (g ∘ k) (p✝ + q✝)

Tactic:
simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ : MvPolynomial σ R
n✝ : σ
a✝ : eval₂ f g ((rename k) p✝) = eval₂ f (g ∘ k) p✝
⊢ eval₂ f g ((rename k) (p✝ * X n✝)) = eval₂ f (g ∘ k) (p✝ * X n✝)

Tactic:
simp [*]

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
a✝ : R
⊢ (rename k) (eval₂ C (g ∘ k) (C a✝)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (C a✝))

Tactic:
simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ q✝ : MvPolynomial σ R
a✝¹ : (rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p✝)
a✝ : (rename k) (eval₂ C (g ∘ k) q✝) = eval₂ C (⇑(rename k) ∘ g) ((rename k) q✝)
⊢ (rename k) (eval₂ C (g ∘ k) (p✝ + q✝)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p✝ + q✝))

Tactic:
simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : (rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (⇑(rename k) ∘ g) ((rename k) p✝)
⊢ (rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (⇑(rename k) ∘ g) ((rename k) (p✝ * X n✝))

Tactic:
simp [*]

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
a✝ : R
⊢ (rename (Prod.mk j)) (eval₂ C g (C a✝)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (C a✝)

Tactic:
simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ q✝ : MvPolynomial σ R
a✝¹ : (rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p✝
a✝ : (rename (Prod.mk j)) (eval₂ C g q✝) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) q✝
⊢ (rename (Prod.mk j)) (eval₂ C g (p✝ + q✝)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p✝ + q✝)

Tactic:
simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : (rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) p✝
⊢ (rename (Prod.mk j)) (eval₂ C g (p✝ * X n✝)) = eval₂ C (fun x ↦ (rename (Prod.mk j)) (g x)) (p✝ * X n✝)

Tactic:
simp [*]

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

Goal state before:
pp: case C
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p : MvPolynomial τ R
a✝ : R
⊢ eval₂ f g ((rename (Prod.mk i)) (C a✝)) = eval₂ f (fun j ↦ g (i, j)) (C a✝)

Tactic:
simp [*]

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

Goal state before:
pp: case add
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p p✝ q✝ : MvPolynomial τ R
a✝¹ : eval₂ f g ((rename (Prod.mk i)) p✝) = eval₂ f (fun j ↦ g (i, j)) p✝
a✝ : eval₂ f g ((rename (Prod.mk i)) q✝) = eval₂ f (fun j ↦ g (i, j)) q✝
⊢ eval₂ f g ((rename (Prod.mk i)) (p✝ + q✝)) = eval₂ f (fun j ↦ g (i, j)) (p✝ + q✝)

Tactic:
simp [*]

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

Goal state before:
pp: case mul_X
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ × τ → S
i : σ
p p✝ : MvPolynomial τ R
n✝ : τ
a✝ : eval₂ f g ((rename (Prod.mk i)) p✝) = eval₂ f (fun j ↦ g (i, j)) p✝
⊢ eval₂ f g ((rename (Prod.mk i)) (p✝ * X n✝)) = eval₂ f (fun j ↦ g (i, j)) (p✝ * X n✝)

Tactic:
simp [*]

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₁
hf : Injective ⇑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q

Tactic:
exact hf (h m)

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

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

Tactic:
map_map

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ (eval g) ((map (φ.comp f)) p) = (eval g) ((map (φ.comp f)) p)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0

Tactic:
refine ⟨fun h => by by_contra ha; simp [ha] at h, fun h => ?_⟩
  apply Nat.le_antisymm (degreeOf_mul_X_self j f)
  have : (f.support.sup fun m ↦ m j) + 1 = (f.support.sup fun m ↦ (m j + 1)) :=
    Finset.apply_sup_eq_sup_comp_of_nonempty @Nat.succ_le_succ (support_nonempty.mpr h)
  simp only [degreeOf_eq_sup, support_mul_X, this]
  apply Finset.sup_le
  intro x hx
  simp only [Finset.sup_map, bot_eq_zero', add_pos_iff, zero_lt_one, or_true, Finset.le_sup_iff]
  use x
  simpa using mem_support_iff.mp hx

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f) → (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
x✝ : S
⊢ x✝ ∈ {i | i ∈ s ∧ f i ≠ 0} → x✝ ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

Tactic:
by simp +contextual

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

Goal state before:
pp: case refine_2.inr.inr
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = if n = p.natDegree then 1 else 0

Tactic:
rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]

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

Goal state before:
pp: case pos
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 fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
case pos
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 fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
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 fun i ↦ (f i).degree) = ↑(s.sup fun i ↦ (f i).natDegree)

Tactic:
← Finset.sup'_eq_sup hs,

Goal state after:
case pos
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 fun i ↦ (f i).degree) = ↑(s.sup' hs fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: 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 σ
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (C a) = Polynomial.C a

Tactic:
MvPolynomial.eval₂_C

Goal state after:
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 σ
p : R[X]
a : R
⊢ Polynomial.C a = Polynomial.C a
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 d ((uniqueAlgEquiv R σ).symm P) = P.coeff (d default)

Tactic:
rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]

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

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

Tactic:
rw [← natDegree_neg] at dg

Goal state after:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
dg : (-q).natDegree < n
⊢ (p - q).coeff n = p.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case refine_3
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p) → p.natDegree = 1

Tactic:
rintro ⟨a, ha, b, rfl⟩

Goal state after:
case refine_3
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
⊢ (C a * X + C b).natDegree = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: 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
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X i)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))

Tactic:
cases i <;> simp

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

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

Tactic:
induction cf generalizing f with

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

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ (comp 0 (-X)).degree = degree 0

Tactic:
zero_comp

Goal state after:
case inl
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
⊢ degree 0 = degree 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x, X x ^ j x.succ)).coeff i) = r * if j = cons i m then 1 else 0

Tactic:
mul_comm (Polynomial.X ^ j 0),

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.C (∏ x, X x ^ j x.succ) * Polynomial.X ^ j 0).coeff i) = r * if j = cons i m then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case e'_2.e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ none = if h : a = a then none else Option.some ⟨a, h⟩

Tactic:
dif_pos rfl

Goal state after:
case e'_2.e'_4
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ none = none
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
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
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ (∑ i, C (x i) * X ^ k i).coeff (k i) ≠ 0

Tactic:
finsetSum_coeff

Goal state after:
case neg
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
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ ∑ b, (C (x b) * X ^ k b).coeff (k i) ≠ 0
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
n✝ : ℕ
⊢ ∑ r ∈ range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ i : ℕ
hi : i ∈ range (n✝ + 1)
⊢ x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommRing R
s : Finset ι
f : ι → R
hs : 0 < #s
⊢ 0 < (Multiset.map f s.val).card

Tactic:
by simpa using hs

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

Goal state before:
pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).coeff (f i).natDegree ≠ 0

Tactic:
finsetSum_coeff

Goal state after:
case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ ∑ b ∈ s, (v b • map (algebraMap R A) (f b)).coeff (f i).natDegree ≠ 0