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

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
⊢ AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f) = algEquivOfAlgEquiv f

Tactic:
by
  ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
m : ℤ
⊢ mk (↑m) 1 = ↑m

Tactic:
simpa using mk_algebraMap (R := R) (A := ℤ) _

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionSemiring R
inst✝⁴ : CharZero R
inst✝³ : DivisionSemiring S
inst✝² : CharZero S
inst✝¹ : SMul R S
inst✝ : SMulCommClass R S S
q : ℚ≥0
a : R
b : S
⊢ q • a • b = a • q • b

Tactic:
by simp [smul_def, mul_smul_comm]

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionRing R
inst✝⁴ : CharZero R
inst✝³ : DivisionRing S
inst✝² : CharZero S
inst✝¹ : SMul R S
inst✝ : SMulCommClass R S S
q : ℚ
a : R
b : S
⊢ q • a • b = a • q • b

Tactic:
by simp [smul_def, mul_smul_comm]

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
⊢ NonUnitalNonAssocRing α

Tactic:
apply e.injective.nonUnitalNonAssocRing _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ (-resolventSet R a)ᶜ = (resolventSet R (-a))ᶜ

Tactic:
resolventSet_neg

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ (-resolventSet R a)ᶜ = (-resolventSet R a)ᶜ
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Tactic:
by
  ext; rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ lmul'' R = (↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul S R S S S)

Tactic:
by
  ext; rfl

Goal state after:
Module: Mathlib.Algebra.Algebra.StrictPositivity

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 < x

Tactic:
have h₁ : 0 ≤ x := by grind
  have h₂ : x ≠ 0 := by grind [= spectrum.zero_notMem_iff]
  exact lt_of_le_of_ne h₁ h₂.symm

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
by
  dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_mk]

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)

Tactic:
rank_matrix,

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max v u, v} #m * lift.{max v u, v} #n = lift.{u, v} (#m * #n)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝ : Type v
bM : Basis fst✝ R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')

Goal state after:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type v'
bN : Basis fst✝ S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
h : K ∙ v < W → K ∙ v = ⊥
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False

Tactic:
span_singleton_eq_bot,

Goal state after:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
v : V
h : K ∙ v < W → v = 0
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = K ∙ v
⊢ False
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✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ S = ⊥

Tactic:
← Submodule.rank_eq_zero,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ Module.rank R ↥S = 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ ⟨↑v, ⋯⟩ ≠ ⟨w, ⋯⟩

pp: case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ f = b.coord ⟨w, ⋯⟩

Tactic:
· apply_fun (f ∘ (↑))
    simp [hw]

Goal state after:
case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ f = b.coord ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
⊢ False

Tactic:
have : Subsingleton V := .intro fun _ _ ↦ by simp_rw [← hv]

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this✝ : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
this : Subsingleton V
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this✝¹ : Nontrivial K
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ r, r • v₀ = v
H : Module.rank K V = 0
κ : Type v
b : Basis κ K V
this✝ : IsEmpty κ
this : Subsingleton V
⊢ False

Tactic:
exact h (Subsingleton.elim _ _)

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

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

Tactic:
rintro ⟨⟩ ⟨⟩

Goal state after:
case mk.mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝² : FreeAlgebra R X
a✝¹ : Pre R X
b✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝ + Quot.mk (Rel R X) a✝¹
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = p.sum fun e a ↦ f a * x ^ e

Tactic:
by
  rw [eval₂_def]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case left_distrib
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
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ * (b✝ + c✝)) = liftFun R X f (a✝ * b✝ + a✝ * c✝)

Tactic:
change _ * (_ + _) = _ * _ + _ * _
        rw [left_distrib]

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 y : FreeAlgebra R X),
    Quot.liftOn (x * y) (liftFun R X f) ⋯ = Quot.liftOn x (liftFun R X f) ⋯ * Quot.liftOn y (liftFun R X f) ⋯

Tactic:
rintro ⟨⟩ ⟨⟩

Goal state after:
case mk.mk
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✝ : FreeAlgebra R X
a✝¹ : Pre R X
y✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.liftOn (Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝) (liftFun R X f) ⋯ =
    (Quot.mk (Rel R X) a✝¹).liftOn (liftFun R X f) ⋯ * (Quot.mk (Rel R X) a✝).liftOn (liftFun R X f) ⋯
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 y : FreeAlgebra R X),
    Quot.liftOn (x + y) (liftFun R X f) ⋯ = Quot.liftOn x (liftFun R X f) ⋯ + Quot.liftOn y (liftFun R X f) ⋯

Tactic:
rintro ⟨⟩ ⟨⟩

Goal state after:
case mk.mk
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✝ : FreeAlgebra R X
a✝¹ : Pre R X
y✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.liftOn (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝) (liftFun R X f) ⋯ =
    (Quot.mk (Rel R X) a✝¹).liftOn (liftFun R X f) ⋯ + (Quot.mk (Rel R X) a✝).liftOn (liftFun R X f) ⋯
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ n.sqrt + 2 - (a✝ + 2) < n.sqrt + 2 - a✝

Tactic:
simp_wf; apply minFac_lemma n k; assumption

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

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Nontrivial R
p : ℕ
inst✝¹ : CharP R p
inst✝ : ExpChar R 1
⊢ p = 0

Tactic:
exact char_zero_of_expChar_one R p

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Monoid M
inst✝ : Subsingleton M
a : A
a✝ : M
⊢ ((uniqueAlgEquiv R M).symm a).coeff a✝ = (single 1 a).coeff a✝

Tactic:
simp [uniqueAlgEquiv]

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
x : A[M]
m : M
⊢ ((mapAlgHom M f) x).coeff m = f (x.coeff m)

Tactic:
by simp [mapAlgHom]

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

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
exact h₁ (left_mem_Ico.2 (g₀.trans hx)) ⟨g₀.le, hx⟩ g₀.le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (C c).nextCoeff = 0

Tactic:
rw [nextCoeff]

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
⊢ (if (C c).natDegree = 0 then 0 else (C c).coeff ((C c).natDegree - 1)) = 0
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 ↔ p ∣ n

Tactic:
← CharP.cast_eq_zero_iff R,

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.Operations

Goal state before:
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
⊢ q.natDegree < j

Tactic:
by_contra! H'

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
H' : j ≤ q.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p - q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
simpa only [← natDegree_neg q] using! natDegree_add_le p (-q)

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

Goal state before:
pp: case neg
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).natDegree = p.natDegree

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero

Goal state after:
case neg.pn
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).natDegree ≤ p.natDegree

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
Module: Mathlib.Algebra.Polynomial.Degree.Domain

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

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n : ℕ
⊢ 0 ≤ ↑n

Tactic:
rw [← WithBot.coe_zero, cast_withBot, WithBot.coe_le_coe]

Goal state after:
n : ℕ
⊢ 0 ≤ n
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
hp : p ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R; · exact (hp (Subsingleton.elim _ _)).elim
  apply supDegree_mul hD hadd ?_ hp hq.ne_zero
  simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ 0 ≤ single i a ↔ 0 ≤ a

Tactic:
by classical exact Pi.single_nonneg

Goal state after:
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 = ∑ i ∈ range (p.natDegree + 1), p.coeff i • x ^ i

Tactic:
Algebra.smul_def

Goal state after:
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
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]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ i ∈ range n, p.coeff i • x ^ i

Tactic:
Algebra.smul_def

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range n, (algebraMap R S) (p.coeff x_1) * x ^ x_1
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case neg
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
convert! dvd_zero p

Goal state after:
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ f.coeff i * z ^ i = 0
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f + g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_add_right]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
ha : IsRegular a
p q : MvPolynomial σ R
h : (fun x ↦ (MvPolynomial.monomial m) a * x) p = (fun x ↦ (MvPolynomial.monomial m) a * x) q
d : σ →₀ ℕ
h' : a * coeff d p = a * coeff d q
⊢ coeff d p = coeff d q

Tactic:
rw [← ha.left.eq_iff, h']

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ (algebraMap R (MvPolynomial σ R)) c *
      ∏ a ∈ s.support, (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a =
    0

Tactic:
apply mul_eq_zero_of_right

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ ∏ a ∈ s.support, (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a = 0
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.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.degrees.toFinset = ∅
⊢ p.degrees.card = 0

Tactic:
Multiset.toFinset_eq_empty

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.degrees = 0
⊢ p.degrees.card = 0
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]
  ext
  erw [mem_range_map_iff_coeffs_subset, mem_coeffsIn_iff_coeffs_subset]
  simp [Set.subset_def]

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

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update i.succ y).tail = t.tail.update i y

Tactic:
by ext; simp [tail]

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

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
⊢ cons 0 0 = 0

Tactic:
by simp [cons_zero_eq_single_zero]

Goal state after:
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:
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: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) p = (RingHom.id (MvPolynomial σ R)) p

Tactic:
refine hom_congr_vars ?_ ?_ ?_

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

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 ∈ p.vars,
    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)

case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
| C r * X ^ (revAt N) 0

Tactic:
revAt_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
| C r * X ^ N