mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ 1 • x ∈ (mkSpanSingleton' x y H).domain

Tactic:
· rwa [one_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent K Subtype.val) → ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s

Tactic:
· rintro ⟨s, rfl, si⟩
    exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

Goal state after:
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
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
this : ∀ (x : V), f x = 0 → f (g x) = 0
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker

Tactic:
rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} (Module.rank F F)
⊢ Module.rank F ↥⊥ ≤ 1

Tactic:
rank_self,

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} 1
⊢ Module.rank F ↥⊥ ≤ 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
c : R
z : ↥(f.domain ⊔ g.domain)
⊢ fg (c • z) = σ c • fg z

Tactic:
rw [smul_add, ← map_smulₛₗ, ← map_smulₛₗ]

Goal state after:
case w.refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
c : R
z : ↥(f.domain ⊔ g.domain)
⊢ fg (c • z) = ↑f (c • ⟨x z, ⋯⟩) + ↑g (c • ⟨y z, ⋯⟩)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
⊢ g ≤ f.sup g h

Tactic:
by
  refine ⟨le_sup_right, fun z₁ z₂ hz => ?_⟩
  rw [← zero_add (g _), ← f.map_zero]
  refine (sup_apply h _ _ _ ?_).symm
  simpa

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 g : E →ₛₗ.[σ] F
x : E
⊢ x ∈ (-(f + g)).domain ↔ x ∈ (-g + -f).domain

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 g : E →ₛₗ.[σ] F
x : E
hf✝ : x ∈ (-(f + g)).domain
h : x ∈ (-g + -f).domain
⊢ ↑(-(f + g)) ⟨x, hf✝⟩ = ↑(-g + -f) ⟨x, h⟩

Tactic:
· simp [add_domain, neg_domain, And.comm]

Goal state after:
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 g : E →ₛₗ.[σ] F
x : E
hf✝ : x ∈ (-(f + g)).domain
h : x ∈ (-g + -f).domain
⊢ ↑(-(f + g)) ⟨x, hf✝⟩ = ↑(-g + -f) ⟨x, h⟩
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
x : R
⊢ eval x (p.comp q) = eval (eval x q) p

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add r s hr hs => simp [add_comp, hr, hs]
  | monomial n a => simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ¬∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
H1 : Nat.find ⋯ ∣ x
⊢ ↑x = 0

Tactic:
by
          rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
            zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : ↑y = (x_fst, x_snd).1
hx2 : ↑g.toLinearPMap y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g

Tactic:
convert! g.mem_graph_toLinearPMap hg y using 1

Goal state after:
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : ↑y = (x_fst, x_snd).1
hx2 : ↑g.toLinearPMap y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) = (↑y, ↑g.toLinearPMap y)
Module: Mathlib.Order.Filter.Extr

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

Tactic:
by
  refine hle.mp (h.mono fun x hf hgf => ?_)
  rw [← hfga]
  exact le_trans hgf hf

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

Goal state before:
pp: case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ (C 0).degree ≤ 0

Tactic:
C_0

Goal state after:
case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ degree 0 ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ C 0 = 0

Tactic:
C_0

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ ((monomial m) a).natDegree ≤ m

Tactic:
Polynomial.natDegree_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
p : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ ↑n = C 0

Tactic:
C_0

Goal state after:
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
p : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ ↑n = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).degree ≤ max p.degree ↑n

Tactic:
rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl

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✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ (∑ a ∈ p.coeff.support, ∑ x ∈ q.coeff.support, if a + x = ap + aq then p.coeff a * q.coeff x else 0) =
    p.coeff ap * q.coeff aq

Tactic:
Finset.sum_eq_single ap,

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
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = p.coeff ap * q.coeff aq

case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0

case h₁
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ap ∉ p.coeff.support → (∑ x ∈ q.coeff.support, if ap + x = ap + aq then p.coeff ap * q.coeff x else 0) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg.inl
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

pp: case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
· simp_all

Goal state after:
case neg.inr
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n m : WithBot ℕ
⊢ n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0

Tactic:
by
  cases n
  · simp
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add, Nat.add_eq_one_iff]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : natDegree 1 = p.natDegree + q.natDegree
⊢ p.natDegree = 0

Tactic:
natDegree_one,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : 0 = p.natDegree + q.natDegree
⊢ p.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : a ∣ p
h : a.degree ≤ 0
⊢ IsUnit a

Tactic:
rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢

Goal state after:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ (monomial i) 1 = (monomial j) 1 ↔ i = j

Tactic:
by
  simp_rw [← ofFinsupp_single, ofFinsupp.injEq]
  exact AddMonoidAlgebra.of_injective.eq_iff

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
⊢ x < y ∨ x = y ↔ x default < y default ∨ x default = y default

Tactic:
Pi.Lex.lt_iff_of_unique,

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Lex ((i : ι) → β i)
⊢ x default < y default ∨ x = y ↔ x default < y default ∨ x default = y default
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range (p.natDegree + 1), (algebraMap R S) (p.coeff x_1) * x ^ x_1

Tactic:
exact eval₂_eq_sum_range (algebraMap R S) x

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

Tactic:
rw [toMultiset_zero]

Goal state after:
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
⊢ 0 ≤ (p + q).degrees
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✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ coeffsIn σ M ^ (n + 1) * coeffsIn σ M = coeffsIn σ M ^ (n + 2)

pp: case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Tactic:
← pow_succ

Goal state after:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ coeffsIn σ M ^ (n + 1 + 1) = coeffsIn σ M ^ (n + 2)

case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 < s i
⊢ ∃ b ∈ p.support, s i ≤ b i

Tactic:
use s

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₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ Subalgebra.toSubmodule (mapAlgHom f).range = coeffsIn σ (Subalgebra.toSubmodule f.range)

Tactic:
simp only [← SetLike.coe_set_eq, Subalgebra.coe_toSubmodule, AlgHom.coe_range]

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : CommSemiring S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ range ⇑(mapAlgHom f) = ↑(coeffsIn σ (Subalgebra.toSubmodule f.range))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ degreeOf i p ≤ s i

Tactic:
by rw [hs2]

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

Goal state before:
pp: case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m * p).coeff (m * n + n) = (p ^ m).coeff (m * n) * p.coeff n

Tactic:
coeff_mul_add_eq_of_natDegree_le _ pn

Goal state after:
case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).coeff (m * n) * p.coeff n = (p ^ m).coeff (m * n) * p.coeff n

R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: 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)

Tactic:
AlgEquiv.apply_symm_apply,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ P.coeff (d default) = P.coeff ((Finsupp.single default (d default)) default)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
⊢ C 0 = 0

Tactic:
C_0

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
⊢ 0 = 0
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

pp: case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p.comp (-X)).degree = p.degree

Tactic:
· rw [zero_comp]

Goal state after:
case inr
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p.comp (-X)).degree = p.degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
· simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]

Goal state after:
case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0

Tactic:
by
  conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]
  constructor
  · intro h
    rw [h, zero_mul]
  · intro h
    rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : natDegree 1 = (X + C a).natDegree + g.natDegree
⊢ False

Tactic:
natDegree_one,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = (X + C a).natDegree + g.natDegree
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin n
⊢ (finSuccEquiv R n) (X j.succ) = Polynomial.C (X j)

Tactic:
by
  simp [finSuccEquiv_apply]

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

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

Tactic:
simp only [hjmi, if_false]
      obtain hij | rfl := ne_or_eq i (j 0)
      · simp only [hij, if_false, coeff_zero]
      simp only [if_true]
      have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
      simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using!
        coeff_monomial m j.tail (1 : R)

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

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

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree 1 = p.natDegree + q.natDegree
⊢ p = 1

Tactic:
natDegree_one,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : 0 = p.natDegree + q.natDegree
⊢ p = 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0

Tactic:
· apply right_ne_zero_of_mul ht

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ p ∈ ⟦a✝⟧, p.natDegree ≤ n
⊢ (prod ⟦a✝⟧).coeff (Multiset.card ⟦a✝⟧ * n) = (Multiset.map (fun p ↦ p.coeff n) ⟦a✝⟧).prod

Tactic:
simpa using coeff_list_prod_of_natDegree_le _ _ hl

Goal state after: