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

Goal state before:
pp: 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 y : E
x✝¹ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
x✝ : y ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
hfy : y ∈ f.domain
hgy : y ∈ g.domain
hy : ↑f ⟨y, hfy⟩ = ↑g ⟨y, hgy⟩
⊢ ↑f ⟨x + y, ⋯⟩ = ↑g ⟨x + y, ⋯⟩

Tactic:
by
      simp_all [← AddMemClass.mk_add_mk, f.map_add, g.map_add]

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
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ((↑p).domRestrict ⇑f) ↔ Set.SurjOn ⇑f ↑p ↑p

Tactic:
← Set.MapsTo.restrict_surjective_iff h

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
inst✝ : FiniteDimensional K ↥p
f : V →ₗ[K] V
h : ∀ x ∈ p, f x ∈ p
⊢ Injective ((↑p).domRestrict ⇑f) ↔ Surjective (Set.MapsTo.restrict (⇑f) (↑p) (↑p) h)
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
⊢ comap g f.ker = f.ker ⊔ g.ker

Tactic:
comap_eq_sup_ker_of_disjoint _ h'

Goal state after:
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.ker ⊔ g.ker = f.ker ⊔ g.ker

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
⊢ ∀ x ∈ f.ker, g x ∈ f.ker
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
S : Submodule K V
⊢ IsAtom S ↔ finrank K ↥S = 1

Tactic:
by
  refine ⟨fun hS ↦ ?_, fun hS ↦ ⟨by aesop, fun T hT ↦ ?_⟩⟩
  · obtain ⟨v : V, hv : v ∈ S, hv_ne : v ≠ 0⟩ := S.ne_bot_iff.mp hS.ne_bot
    suffices K ∙ v = S by rw [← this, finrank_span_singleton hv_ne]
    have : K ∙ v ≠ ⊥ := by
      rw [Submodule.ne_bot_iff]
      exact ⟨v, mem_span_singleton_self v, hv_ne⟩
    rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]
  · have : FiniteDimensional K S := .of_finrank_eq_succ hS
    have : FiniteDimensional K T := .of_injective (inclusion hT.le) (inclusion_injective hT.le)
    rw [← finrank_eq_zero (R := K)]
    by_contra h
    exact hT.ne <| eq_of_le_of_finrank_le hT.le <| by lia

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), 0 * a = 0

Tactic:
by
    rintro ⟨⟩
    exact Quot.sound Rel.zero_mul

Goal state after:
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'
⊢ ∀ (m : R) (x : ↥(f.domain ⊔ g.domain)), fg (m • x) = σ m • fg x

Tactic:
· intro c z
    rw [smul_add, ← map_smulₛₗ, ← map_smulₛₗ]
    apply fg_eq
    simp only [coe_smul, ← smul_add, hxy]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.ofScalar
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ (algebraMap R A) x = F ((algebraMap R (FreeAlgebra R X)) x)

Tactic:
rw [AlgHom.commutes F _]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x : X
⊢ ((lift R) f) (ι R x) = f x

Tactic:
by
  rw [ι_def, lift]
  rfl

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 p q : R[X]
hp : (C a * p).comp r = C a * p.comp r
hq : (C a * q).comp r = C a * q.comp r
⊢ (C a * (p + q)).comp r = C a * (p + q).comp r

Tactic:
simp [hp, hq, mul_add]

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x y : k[G]
⊢ (x * y).coeff.support ⊆ x.coeff.support * y.coeff.support

Tactic:
simp only [MonoidAlgebra.mul_def, coeff_finsuppSum]

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x y : k[G]
⊢ (x.coeff.sum fun i n ↦ y.coeff.sum fun i_1 n_1 ↦ (single (i * i_1) (n * n_1)).coeff).support ⊆
    x.coeff.support * y.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsRightCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (f * single x r).coeff.support ↔ a✝ ∈ Finset.map (mulRightEmbedding x) f.coeff.support

Tactic:
simp [support_coeff_mul_single_eq_image f hr (.all x)]

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
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
rw [mem_graph_iff] at h
    rcases h with ⟨y, hy, h⟩
    rw [LinearPMap.neg_apply] at h
    rw [Submodule.mem_map]
    simp only [mem_graph_iff, LinearMap.prodMap_apply, LinearMap.id_coe, id,
      LinearMap.neg_apply, Prod.mk_inj, Prod.exists, exists_exists_and_eq_and]
    use x_fst, y, hy

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
⊢ ringChar R ≠ 1

Tactic:
by
  simpa using not_subsingleton R

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 1 ≠ 0

pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Tactic:
· exact one_ne_zero

Goal state after:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (if hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0 then g.toLinearPMapAux hg else 0) x = valFromGraph hg ⋯

Tactic:
rw [dif_pos]

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 : ↥(map (LinearMap.fst R E F) g)
⊢ (g.toLinearPMapAux ?hc) x = valFromGraph hg ⋯

case hc
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 : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
b : β
⊢ b ≤ f a ↔ ∀ a ∈ s, b ≤ f a

Tactic:
exact ⟨fun hba x hx ↦ le_trans hba (hfsa hx), fun hb ↦ hb a ha⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
f : A →ₐ[R] B
m : M
a : A
a✝ : M
⊢ ((mapAlgHom M f) (single m a)).coeff a✝ = (single m (f a)).coeff a✝

Tactic:
simp [single_apply, apply_ite f]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (C a * X ^ n).degree ≤ ↑n

Tactic:
rw [C_mul_X_pow_eq_monomial]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).degree ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Tactic:
· rwa [degree_eq_natDegree hp, Nat.cast_lt]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).leadingCoeff = 1

Tactic:
simpa only [C_1, one_mul] using leadingCoeff_C_mul_X_pow (1 : R) n

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

Goal state before:
pp: case neg.p1
R : Type u
inst✝⁴ : Semiring R
p : R[X]
S : Type u_1
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : Module S R
inst✝ : Module.IsTorsionFree S R
a : S
ha : a ≠ 0
hp : ¬p = 0
⊢ (a • p).coeff p.natDegree ≠ 0

Tactic:
· simp only [coeff_smul]
      apply smul_ne_zero ha
      simp [hp]

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.degree < p.degree
⊢ ¬p ∣ q

Tactic:
by_contra hcontra

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.degree < p.degree
hcontra : p ∣ q
⊢ False
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_contra hcontra

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h0 : q ≠ 0
hl : q.natDegree < p.natDegree
hcontra : p ∣ q
⊢ False
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p

Tactic:
hd,

Goal state after:
case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ max (supDegree D q) (supDegree D q) ≤ supDegree D q
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ leadingCoeff D p - q.coeff (Function.invFun D (supDegree D p)) = 0

Tactic:
hd,

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ leadingCoeff D p - q.coeff (Function.invFun D (supDegree D q)) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Units

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

Tactic:
by
  contrapose! ha with h
  rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
  simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap

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 : ℕ
⊢ (eval₂ (C.comp f) X p).coeff n = f (p.coeff n)

Tactic:
eval₂_def,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ (p.sum fun e a ↦ (C.comp f) a * X ^ e).coeff n = f (p.coeff n)
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p : S[X]
n : ℕ
s : S
r : R
hr : f r = s
⊢ (monomial n) (f r) = (monomial n) s

Tactic:
hr

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
p : S[X]
n : ℕ
s : S
r : R
hr : f r = s
⊢ (monomial n) s = (monomial n) s
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ p.IsRoot x

Tactic:
rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]

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
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
hq : Monic D q
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
by
  obtain rfl | hp := eq_or_ne p 0
  · rw [zero_mul]
  rw [leadingCoeff, hq.supDegree_mul_of_ne_zero_left hD hadd hp,
    coeff_supDegree_add_supDegree hD hadd, hq, mul_one]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝⁶ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : LinearOrder B
inst✝² : OrderBot B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
hp : Monic D p
n : ℕ
ih : Monic D (p ^ n)
⊢ Monic D (p * p ^ n)

Tactic:
exact hp.mul hD hadd ih

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
by
  have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]
  rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]
  simp only [one_pow, mul_one, mul_comm (y ^ _) (d.choose _)]
  rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel_right,
    mul_sum, sum_range_succ', Nat.cast_zero, zero_mul, mul_zero, add_zero]
  refine sum_congr rfl fun y _hy => ?_
  rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (eval₂ C q p).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
eval₂_def,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun e a ↦ C a * q ^ e).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
hj : m < j
⊢ P.coeff i * Q.coeff j = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]

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

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
⊢ r ∈ M * N → ∀ (i : σ →₀ ℕ), (monomial i) r ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
hr

Goal state after:
case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
r : S
hr : r ∈ M * N
⊢ ∀ (i : σ →₀ ℕ), (monomial i) r ∈ coeffsIn σ M * coeffsIn σ N
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 + 2)) = coeffsIn σ M ^ (n + 2)

Tactic:
rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]; exact n.succ_ne_zero

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

Goal state before:
pp: case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

pp: case neg
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
on_goal 2 =>
    rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
    · rw [Finsupp.prod_zero_index, mul_one]
      rfl
    on_goal 1 => intro d hd hd0

Goal state after:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

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

Tactic:
rw [Algebra.smul_def]

Goal state after:
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s t : Multiset σ
c : R
x : MvPolynomial σ R
hx : x ∈ {p | p.degrees ≤ s}
⊢ ((algebraMap R (MvPolynomial σ R)) c * x).degrees ≤ s
Module: Mathlib.Algebra.MvPolynomial.Variables

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

Tactic:
rcases hf hip with ⟨i, rfl⟩

Goal state after:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : τ
hip a✝ : f i ∈ p.vars
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X (f i)) =
    (RingHom.id (MvPolynomial σ R)) (X (f i))
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
r : R
⊢ supDegree (⇑toLex) (C r) = 0

Tactic:
by
  classical
    exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ (C a * X ^ n).trailingDegree

Tactic:
rw [C_mul_X_pow_eq_monomial]

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ↑n ≤ ((monomial n) a).trailingDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead ≠ 0

Tactic:
rw [Ne, ← card_support_eq_zero, eraseLead_support]
  exact
    (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

Tactic:
by_contra

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
this : ¬#f.eraseLead.support + 1 = 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ (sumRingEquiv R S₁ S₂) (C r) = C (C r)

Tactic:
unfold sumRingEquiv C MvPolynomial

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ ((mapDomainRingEquiv R sumFinsuppAddEquivProdFinsupp).trans curryRingEquiv)
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r) =
    (have __src := singleZeroRingHom;
      { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((have __src := singleZeroRingHom;
        { toFun := ⇑(monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r)
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
⊢ (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)).comp
      (Polynomial.aevalTower (rename Option.some) (X none)) =
    AlgHom.id R (MvPolynomial S₁ R)[X]

Tactic:
ext : 2 <;> simp

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (optionEquivLeft R S₁) ((monomial m) r) = (Polynomial.monomial (m none)) ((monomial m.some) r)

Tactic:
rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
  · rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]
    simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
      map_mul, mul_assoc]
    simp only [mul_comm, map_finsuppProd, map_pow]
  · simp
  · intros; rw [pow_add]

Goal state after: