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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e = 0

Tactic:
f,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ (∑ x ∈ t, if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
w : V
⊢ (Finsupp.uniqueEquiv default)
      (b.repr
        ((fun f ↦ f default • v) ((fun w ↦ Finsupp.single default ((b.repr w) default / (b.repr v) default)) w))) =
    (Finsupp.uniqueEquiv default) (b.repr w)

Tactic:
simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
          smul_eq_mul, Pi.smul_apply, Finsupp.uniqueEquiv_apply]

Goal state after:
K : Type u
V : Type v
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : Unique ι
h✝ : finrank K V = 1
v : V
hv : v ≠ 0
b : Basis ι K V := basisUnique ι h✝
h : (b.repr v) default ≠ 0
w : V
⊢ (RingHom.id K) ((b.repr w) default / (b.repr v) default) * (b.repr v) default = (b.repr w) default
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case pos
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 : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
x : E
hx : x ∈ S
h1 : Unique κ
y : F
hy : (algebraMap F ↥S) y = ⟨x, hx⟩
⊢ x ∈ range ⇑(algebraMap F E)

Tactic:
exact ⟨y, congr(Subtype.val $(hy))⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
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 : E →ₛₗ.[σ] F
x : E
y : x ∈ (- -f).domain
hxy : x ∈ f.domain
⊢ ↑(- -f) ⟨x, y⟩ = ↑f ⟨x, hxy⟩

Tactic:
simp only [neg_apply, neg_neg]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }

Tactic:
simp only [← ofFinsupp_mul, eval₂_ofFinsupp]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[ℕ]
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
⊢ (liftNC ↑f ⇑((powersHom S) x)) (p * q) = (liftNC ↑f ⇑((powersHom S) x)) p * (liftNC ↑f ⇑((powersHom S) x)) q
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
x : ↥(sSup (domain '' c))
this : ∃ y ∈ domain '' c, ↑x ∈ y
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain

Tactic:
rwa [Set.exists_mem_image, ← bex_def, SetCoe.exists'] at this

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

Goal state before:
pp: case add
R : Type u
a : R
inst✝ : Semiring R
p✝ : R[X]
x : R
p q : R[X]
ph : eval x (C a * p) = a * eval x p
qh : eval x (C a * q) = a * eval x q
⊢ eval x (C a * (p + q)) = a * eval x (p + q)

Tactic:
| add p q ph qh =>

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

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

Tactic:
simp +contextual only [Polynomial.map_add, add_comp, forall_const,
        imp_true_iff]

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

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
⊢ IsMaxOn f (Iio a) b

Tactic:
intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ g₀ self_mem_Iic g₀
  · exact h₁ (left_mem_Ico.2 (g₀.trans hx)) ⟨g₀.le, hx⟩ g₀.le

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

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

Tactic:
← heq.isMinFilter_iff hfga

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter f l a ∨ IsMaxFilter f l a
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Semiring R
⊢ (↑n).coeff 0 = ↑n

Tactic:
by
  simp only [coeff_natCast_ite, ite_true]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
⊢ a + q.degree ≤ a + b

Tactic:
hq

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
⊢ a + b ≤ a + b
Module: Mathlib.Algebra.Polynomial.Degree.Domain

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

Tactic:
obtain rfl | hp := eq_or_ne p 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  exact natDegree_pow' <| by
    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: case h₀
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

Tactic:
obtain h | hdf' := lt_or_ge df df'

Goal state after:
case h₀.inl
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
h : df < df'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0

case h₀.inr
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ antidiagonal (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_2
inst✝ : SMulZeroClass S R
a : S
p : R[X]
⊢ (a • p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]

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

Goal state before:
pp: case hmax
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this✝ : AddLeftMono B
this : AddRightMono B
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q

Tactic:
exact fun a ha => (Finset.le_sup ha).trans (supDegree_mul_le hadd)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff 0 * 0 ^ 0 = eval 0 p

Tactic:
symm
      rw [eval_eq_sum]
      exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow hb]) (by simp)

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
hp : p ≠ 0
⊢ ↑p.natDegree ≤ ↑p.natDegree + ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
  rw [degree_lt_iff_coeff_zero] at hm
  simp [hm m le_rfl]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support ∆ q.support ⊆ (p + q).support

Tactic:
symmDiff_def,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊔ q.support \ p.support ⊆ (p + q).support
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
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 q : MvPolynomial σ R
hp : (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p
⊢ (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q →
    (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)

Tactic:
hq

Goal state after:
case add
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 q : MvPolynomial σ R
hp : (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) p
hq : (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) q
⊢ (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s ↦ (eval x) (g s)) (p + q)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))

Tactic:
hq

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
hq : k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q)
⊢ k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
hq

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p q : MvPolynomial σ R
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
hq : k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q)
⊢ eval₂ k (⇑k ∘ g) ((map f) p) + eval₂ k (⇑k ∘ g) ((map f) q) =
    eval₂ k (⇑k ∘ g) ((map f) p) + eval₂ k (⇑k ∘ g) ((map f) q)
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)
⊢ (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q) →
    (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))

Tactic:
hq

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)
⊢ (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ ((monomial s) a).degrees = toMultiset s

Tactic:
classical
    exact (supDegree_single s a).trans (if_neg ha)

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

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)
⊢ (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
    ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))

Tactic:
hq

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p q : MvPolynomial σ R
hp : ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)
hq : ∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + 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₁
p : MvPolynomial σ R
⊢ ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)

Tactic:
apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]

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

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ toMultiset 0 ≤ (p + q).degrees

pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ toMultiset d ≤ (p + q).degrees

Tactic:
· rw [toMultiset_zero]; apply Multiset.zero_le

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ toMultiset d ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mpr
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 : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M

Tactic:
rintro hp i
    split <;> simp [hp]

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

Goal state before:
pp: case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp : constantCoeff ((rename f) p) = constantCoeff p
⊢ constantCoeff ((rename f) q) = constantCoeff q → constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)

Tactic:
hq

Goal state after:
case add
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp : constantCoeff ((rename f) p) = constantCoeff p
hq : constantCoeff ((rename f) q) = constantCoeff q
⊢ constantCoeff ((rename f) (p + q)) = constantCoeff (p + q)
Module: Mathlib.Algebra.MvPolynomial.Degrees

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
hf : Injective ⇑f
⊢ ((map f) p).degrees = p.degrees

Tactic:
simp only [degrees, MvPolynomial.support_map_of_injective _ hf]

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ f p + eval₂ c (⇑f ∘ X) q = f (p + q)

Tactic:
hq

Goal state after:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ f p + f q = f (p + q)
Module: Mathlib.Data.Finsupp.Fin

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

Tactic:
contrapose h with c

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

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

Tactic:
contrapose h with c

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

Goal state before:
pp: case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun i ↦ (f i).totalDegree

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]

Goal state after:
case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ (f a + ∑ x ∈ s, f x).totalDegree ≤ max (f a).totalDegree (s.sup fun i ↦ (f i).totalDegree)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ 0 < ∑ i ∈ m.support, m i

Tactic:
exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
      (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0

Tactic:
simp [natTrailingDegree, or_comm]

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

Goal state before:
pp: case inr
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
· simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt <|
      lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)

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

Goal state before:
pp: case insert.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (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)
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (s.sum f).degree

Tactic:
degree_add_eq_right_of_degree_lt H

Goal state after:
case insert.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (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)
H : (f x).degree < (s.sum f).degree
⊢ (s.sum f).degree = (s.sum f).degree
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

Tactic:
refine
    Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) ?_ fun h =>
      (h (mem_antidiagonal.mpr rfl)).elim

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ ∀ b ∈ antidiagonal (p.natTrailingDegree + q.natTrailingDegree),
    b ≠ (p.natTrailingDegree, q.natTrailingDegree) → p.coeff b.1 * q.coeff b.2 = 0
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:
ext
  simp only [coeff_add, coeff_reflect]

Goal state after:
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✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ p + eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = p + q

Tactic:
hq

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✝ p q : R[X]
hp : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ p + q = p + q
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]

Goal state after: