mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case surj
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ y * (algebraMap P S) ↑(h x, ⟨h ↑s, ⋯⟩).2 = (algebraMap P S) (h x, ⟨h ↑s, ⋯⟩).1

Tactic:
dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢

Goal state after:
case surj
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ y * (algebraMap R S) (h.symm.toRingHom (h ↑s)) = (algebraMap R S) (h.symm.toRingHom (h x))
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ Submodule.span R (f '' Fin.val ⁻¹' insert (sSup s) (Set.Iio (sSup s))) =
    Submodule.span R ({f ⟨sSup s, ⋯⟩} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s))

Tactic:
← Set.union_singleton,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ Submodule.span R (f '' Fin.val ⁻¹' (Set.Iio (sSup s) ∪ {sSup s})) =
    Submodule.span R ({f ⟨sSup s, ⋯⟩} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s))
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
h : adjoin A ↑(Subalgebra.map includeRight ⊤) = ⊤
⊢ adjoin A ((fun x ↦ 1 ⊗ₜ[R] x) '' s) = ⊤

Tactic:
simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : NonUnitalNonAssocSemiring B
inst✝¹⁰ : Module R A
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : SMulCommClass R B B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : IsScalarTower R B B
inst✝⁴ : StarRing R
inst✝³ : StarRing A
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x y : A ⊗[R] B
x✝³ : A
x✝² : B
x✝¹ x✝ : A ⊗[R] B
h₁ : star (x✝³ ⊗ₜ[R] x✝² * x✝¹) = star x✝¹ * star (x✝³ ⊗ₜ[R] x✝²)
h₂ : star (x✝³ ⊗ₜ[R] x✝² * x✝) = star x✝ * star (x✝³ ⊗ₜ[R] x✝²)
⊢ star (x✝³ ⊗ₜ[R] x✝² * (x✝¹ + x✝)) = star (x✝¹ + x✝) * star (x✝³ ⊗ₜ[R] x✝²)

Tactic:
simp [add_mul, mul_add, h₁, h₂]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalNonAssocSemiring A
inst✝¹¹ : NonUnitalNonAssocSemiring B
inst✝¹⁰ : Module R A
inst✝⁹ : Module R B
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : SMulCommClass R B B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : IsScalarTower R B B
inst✝⁴ : StarRing R
inst✝³ : StarRing A
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x y x✝¹ x✝ : A ⊗[R] B
h₁ : star (x✝¹ * y) = star y * star x✝¹
h₂ : star (x✝ * y) = star y * star x✝
⊢ star ((x✝¹ + x✝) * y) = star y * star (x✝¹ + x✝)

Tactic:
simp [add_mul, mul_add, h₁, h₂]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a✝ : A
r : R
a : A
⊢ (fun s ↦ star s * s) (r • a) = (fun s ↦ star s * s) r • (fun s ↦ star s * s) a

Tactic:
simp [star_smul, smul_mul_smul_comm]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : ↥(centralizer R S) ⊗[R] B
x : A
hx : x ∈ S
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w * includeLeft x

Tactic:
induction w using TensorProduct.induction_on with
    | zero => simp
    | tmul b c =>
      simp [Subalgebra.mem_centralizer_iff _ |>.1 b.2 x hx]
    | add y z hy hz => rw [map_add, mul_add, hy, hz, add_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
⊢ 0 ≤ 1

Tactic:
simpa using star_mul_self_nonneg (1 : R)

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ Module.rank R M = 0 → ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0

Tactic:
· contrapose!
    rintro ⟨x, hx⟩
    rw [← Cardinal.one_le_iff_ne_zero]
    have : LinearIndependent R (fun _ : Unit ↦ x) :=
      linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
        hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))
    simpa using this.cardinal_lift_le_rank

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (range b).toFinset.card ≤ Fintype.card ι

Tactic:
Set.toFinset_range

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ (Finset.image b Finset.univ).card ≤ Fintype.card ι
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ LinearIndependent K Subtype.val

Tactic:
convert! (ofVectorSpace K V).linearIndependent

Goal state after:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Subtype.val = ⇑(ofVectorSpace K V)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: 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₀)
⊢ finrank R M < #t'

Tactic:
card_map,

Goal state after:
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₀)
⊢ finrank R M < #(t.erase x₀)
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
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ σ (Classical.choose ⋯) • y - σ c • y = 0

Tactic:
← sub_smul,

Goal state after:
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
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ (σ (Classical.choose ⋯) - σ c) • y = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
H : x ≠ 0
⊢ ∃ y, x * y = 1

Tactic:
by
  have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
  exact this 1

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
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v = S
⊢ finrank K ↥(K ∙ v) = 1

Tactic:
finrank_span_singleton hv_ne

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
this : K ∙ v = S
⊢ 1 = 1
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
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
⊢ K ∙ x = ⊤

Tactic:
have : FiniteDimensional K V := .of_finrank_eq_succ h

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : FiniteDimensional K V
⊢ K ∙ x = ⊤
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 : V
nz : v ≠ 0
⊢ finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w

Tactic:
finrank_eq_one_iff_of_nonzero v nz

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ K ∙ v = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w
Module: Mathlib.Algebra.Polynomial.Eval.Algebra

Goal state before:
pp: case monomial
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
n : ℕ
a : R
⊢ eval₂ (algebraMap R S) x (((monomial n) a).comp q) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) ((monomial n) a)

Tactic:
| monomial n a =>

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

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

Tactic:
| monomial n a =>

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

Goal state before:
pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ ↑a = ↑a + ↑c ↔ a % p = (a + c) % p

Tactic:
left_eq_add,

Goal state after:
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ ↑c = 0 ↔ a % p = (a + c) % p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
⊢ 0 = ↑1 ↔ Subsingleton R

Tactic:
Nat.cast_one,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ 0 = 1 ↔ Subsingleton R
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
⊢ n.minFac = 1 ↔ n = 1

Tactic:
constructor
  · intro h
    by_contra hn
    have := minFac_prime hn
    rw [h] at this
    exact not_prime_one this
  · rintro rfl
    simp [minFac, minFacAux]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q ≠ 0

Tactic:
by refine mt ?_ h; exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (p - q).degree < q.degree

Tactic:
← degree_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (-(p - q)).degree < q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degree = ↑(p.natDegree + q.natDegree)

Tactic:
degree_mul' h,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.degree + q.degree = ↑(p.natDegree + q.natDegree)
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
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
⊢ supDegree D p + supDegree D q ∈ Set.range D

Tactic:
← AddSubsemigroup.coe_set_mk (Set.range D),

Goal state after:
case hb
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
⊢ supDegree D p + supDegree D q ∈ ↑{ carrier := Set.range D, add_mem' := ?hb✝ }

case hb
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
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D
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
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q

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

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

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

Tactic:
Nat.cast_one,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ↑d.succ * ∑ x ∈ range d, ↑(d.choose x) * y ^ x + ↑d.succ * (1 * y ^ d) - ↑d.succ * y ^ d =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (C (p.coeff b)).natDegree + (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
rw [natDegree_C, zero_add]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ f.antidiagonal'.support ↔ p.1 + p.2 = f

Tactic:
by
    rcases p with ⟨p₁, p₂⟩
    simp [antidiagonal', ← and_assoc, Multiset.toFinsupp_eq_iff,
    ← Multiset.toFinsupp_eq_iff (f := f)]

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

Goal state before:
pp: case step
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∀ (n : ℕ), (∀ m > n, P.coeff m • Q = 0) → P.coeff n • Q = 0

Tactic:
intro l

Goal state after:
case step
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 : ℕ
⊢ (∀ m > l, P.coeff m • Q = 0) → P.coeff l • Q = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ C a * (monomial s) a' = (monomial s) (a * a')

Tactic:
by
  have := single_mul_single 0 s a a'
  rw [zero_add] at this
  exact this

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial s) a = C a * s.prod fun n e ↦ X n ^ e

Tactic:
by
  simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, Finsupp.sum_single]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (C a * p) = a * coeff m p

Tactic:
rw [mul_def, sum_C]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (p.coeff.sum fun n b ↦ (monomial (0 + n)) (a * b)) = a * coeff m p

R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ (p.coeff.sum fun n b ↦ (monomial (0 + n)) (0 * b)) = 0
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₁
n : σ
⊢ (map f) (X n) = X n

Tactic:
by simp [X]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ i ∈ s, f i).support.sup fun s ↦ toMultiset s) ≤ s.sup fun i ↦ (f i).support.sup fun s ↦ toMultiset s

Tactic:
exact supDegree_sum_le

Goal state after:
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

Goal state after:
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✝ : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
⊢ (if i✝ ≤ i then coeff (i - i✝) p * 1 else 0) ∈ M
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = (rename Subtype.val) q) → ∃ s q, p * X n = (rename Subtype.val) q

Tactic:
rintro p n ⟨s, p, rfl⟩
    refine ⟨insert n s, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
      simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]
    · simp only [rename_rename, rename_X, map_mul]
      rfl

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

Goal state before:
pp: case refine_1.mem_mul_mem
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
s : σ →₀ ℕ
m : S
hm : m ∈ M
n : S
hn : n ∈ N
⊢ (monomial s) m * (monomial 0) n ∈ coeffsIn σ M * coeffsIn σ N

Tactic:
apply Submodule.mul_mem_mul <;> simpa

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

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ ((monomial s) r).vars = s.support

Tactic:
classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ j ∈ s, f j).support.sup fun m ↦ m i) ≤ s.sup fun j ↦ (f j).support.sup fun m ↦ m i

Tactic:
exact supDegree_sum_le

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p - q).degrees ≤ p.degrees ∪ q.degrees

Tactic:
by
  simpa [degrees_def] using! AddMonoidAlgebra.supDegree_sub_le

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: n : Fin 2 →₀ ℕ
⊢ ofSupportFinite ![n 0, n 1] ⋯ = n

Tactic:
Finsupp.ext_iff,

Goal state after:
n : Fin 2 →₀ ℕ
⊢ ∀ (a : Fin (Nat.succ 0).succ), (ofSupportFinite ![n 0, n 1] ⋯) a = n a
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : R
hs : ∀ (i : σ →₀ ℕ), f (coeff i (C a)) ∈ s
⊢ eval₂ f v (C a) ∈ s

Tactic:
simpa using hs 0

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ((X s).support.sup fun s ↦ s.sum fun x e ↦ e) = 1

Tactic:
support_X

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ ({Finsupp.single s 1}.sup fun s ↦ s.sum fun x e ↦ e) = 1
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
h' : ∃ a ∈ p.coeff.support, (mapDomain.addMonoidHom f) a = b
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
rcases h' with ⟨s, hs, rfl⟩

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.coeff.support
h : (mapDomain.addMonoidHom f) s ∈ ((rename f) p).support
⊢ (((mapDomain.addMonoidHom f) s).sum fun x e ↦ e) ≤ p.totalDegree
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:
by
  rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
⊢ (∃ x, ¬coeff x (((optionEquivLeft R σ) p).coeff i) = 0) →
    ∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i

Tactic:
rintro ⟨m, hm⟩
    exact ⟨optionElim i m, by simpa using! hm, optionElim_apply_none _ _⟩

Goal state after: