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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * ↑y₂ - x₂ * ↑y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * ↑y₂ + -(x₂ * ↑y₁)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * ↑y₂ + -(x₂ * ↑y₁)) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * ↑y₂ + -(x₂ * ↑y₁)) (y₁ * y₂) = mk' S x₁ y₁ + -mk' S x₂ y₂
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x✝ y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x✝ = (lift (LinearMap.mul R A)) y
x : A ⊗[R] A
⊢ ∃ a, x = a ⊗ₜ[R] 1

Tactic:
induction x using TensorProduct.induction_on with
    | zero => exact ⟨0, by simp⟩
    | tmul u v =>
      use u * v
      calc u ⊗ₜ[R] v = u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v := by simp
                   _ = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1 := by rw [h]
                   _ = (u * v) ⊗ₜ[R] 1 := by simp
    | add u v hu hv =>
      obtain ⟨u, rfl⟩ := hu
      obtain ⟨v, rfl⟩ := hv
      exact ⟨u  + v, by simp [add_tmul]⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).Finite

Tactic:
have : Module.Finite S S' := finite_algebraMap.mp Hf

Goal state after:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).Finite
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ x ∈ σ (r • a) ↔ x ∈ r • σ a

Tactic:
x_eq

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r • r⁻¹ • x ∈ σ (r • a) ↔ x ∈ r • σ a
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
r : R
⊢ {r} - σ a = σ (↑ₐ r - a)

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ {r} + -σ a = σ (↑ₐ r - a)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) ↔ ¬IsUnit ((algebraMap R A) r - a)

Tactic:
rw [not_iff_not, isQuasiregular_iff_isUnit, ← sub_eq_add_neg, Algebra.algebraMap_eq_smul_one]

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
hr : IsUnit r
⊢ IsUnit (1 - hr.unit⁻¹ • a) ↔ IsUnit (r • 1 - a)
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹

Tactic:
← Units.inv_eq_val_inv,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ hx.unit.inv i = ↑⋯.unit⁻¹
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Injective ⇑φ
x y : Unitization R A
h : (starMap φ) x = (starMap φ) y
⊢ φ x.toProd.2 = φ y.toProd.2

Tactic:
simpa [algebraMap_eq_inl] using! congr($(h).snd)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : (c.sum fun a b ↦ b • M'.mkQ (g a)) = 0
⊢ (c.sum fun i a ↦ a • g i) = 0

Tactic:
mkQ_apply

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : (c.sum fun a b ↦ b • Submodule.Quotient.mk (g a)) = 0
⊢ (c.sum fun i a ↦ a • g i) = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: 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
inst✝ : Module.Free R B
⊢ centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = centralizer R ↑includeLeft.range

Tactic:
simp [Algebra.TensorProduct.map_range]

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

Goal state before:
pp: 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
inst✝ : Module.Free R A
⊢ centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    centralizer R ↑includeRight.range

Tactic:
simp [Algebra.TensorProduct.map_range]

Goal state after:
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✝ : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
⊢ False

Tactic:
by rw [eq, rank_bot] at h; exact lt_irrefl _ h

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

Goal state before:
pp: R : Type u
ι : Type w
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
inst✝¹ : Finite ι
inst✝ : Nontrivial R
s : Set ι
this : Fintype ι
⊢ (⇑(basisFun R ι) '' s).toFinset.card = s.ncard

Tactic:
Set.toFinset_card,

Goal state after:
R : Type u
ι : Type w
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
inst✝¹ : Finite ι
inst✝ : Nontrivial R
s : Set ι
this : Fintype ι
⊢ Fintype.card ↑(⇑(basisFun R ι) '' s) = s.ncard
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∃ s, W = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
by
    refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩
    rintro _ ⟨w, ⟨_, ⟨hw, rfl⟩⟩⟩
    exact nonzero_span_atom w hw

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case hs.hs
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := ⋯
s : Set V := ⋯
hs : span K s = f.ker
n : Set V := ⋯
⊢ LinearIndepOn K _root_.id (Set.range ⇑b₁)

pp: case hs.hf_inj
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := ⋯
s : Set V := ⋯
hs : span K s = f.ker
n : Set V := ⋯
⊢ Disjoint (span K (Set.range ⇑b₁)) f.ker.subtype.ker

Tactic:
· exact b₁.linearIndependent.linearIndepOn_id

Goal state after:
case hs.hf_inj
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := ⋯
s : Set V := ⋯
hs : span K s = f.ker
n : Set V := ⋯
⊢ Disjoint (span K (Set.range ⇑b₁)) f.ker.subtype.ker
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case hs.hs
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 := ⋯
w : V
hw : f w = 1
s : Set V := ⋯
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := ⋯
⊢ LinearIndepOn K _root_.id (Set.range ⇑b₁)

pp: case hs.hf_inj
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 := ⋯
w : V
hw : f w = 1
s : Set V := ⋯
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := ⋯
⊢ Disjoint (span K (Set.range ⇑b₁)) f.ker.subtype.ker

Tactic:
· exact b₁.linearIndependent.linearIndepOn_id

Goal state after:
case hs.hf_inj
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 := ⋯
w : V
hw : f w = 1
s : Set V := ⋯
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := ⋯
⊢ Disjoint (span K (Set.range ⇑b₁)) f.ker.subtype.ker
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
← t.mk_eq_rank'',

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
h : c ≤ #↑(range ⇑t')
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.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
c✝ : 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✝² * Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝

Tactic:
exact Quot.sound Rel.left_distrib

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

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

Tactic:
exact Quot.sound Rel.add_comm

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p q : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
p q : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (p + -q) = eval₂ f x p - eval₂ f x q
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ ↑1 * r = 0 * r

Tactic:
by rw [CharP.cast_eq_zero]

Goal state after:
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
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g

Tactic:
rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧
    x * 0 + y + z * 0 ≠ 0 ∧ ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0

Tactic:
if_neg hmn.ne',

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧ x * 0 + y + z * 0 ≠ 0 ∧ (x * if n = k then 1 else 0) + y * 0 + z ≠ 0
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

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

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
sub_eq_add_neg,

Goal state after:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D g
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ natDegree 0 = 0

Tactic:
natDegree_zero

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : Subsingleton R
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)

Tactic:
rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.degree < ↑(n + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.degree = ↑p.natDegree

pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.coeff.support.Nonempty

Tactic:
degree_eq_natDegree h,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ↑p.natDegree = ↑p.natDegree

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.coeff.support.Nonempty
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ p.natDegree + 1

Tactic:
rw [← Finset.card_range (p.natDegree + 1)]
  exact Finset.card_le_card supp_subset_range_natDegree_succ

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

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

Tactic:
by
  rw [← WithBot.coe_zero, cast_withBot, WithBot.coe_le_coe]
  exact n.zero_le

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.degree < 0 ↔ p ≠ 0

Tactic:
Nat.WithBot.lt_zero_iff,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬p.degree = ⊥ ↔ p ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p + -C a).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (p - C a).natDegree = p.natDegree

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (p + -C a).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
sub_eq_add_neg,

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

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

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p + -q).leadingCoeff = -q.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
x : R
⊢ eval₂ C X ((monomial n) x) = (monomial n) x

Tactic:
rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']

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

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

Tactic:
sub_eq_add_neg,

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

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

Tactic:
sub_eq_add_neg,

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p + -q).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p + -q).degree = q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n - C r).leadingCoeff = 1

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n + -C r).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ (X - C a).degree = 1

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ (X + -C a).degree = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Ring S
c : S
⊢ (X - C c).nextCoeff = -c

Tactic:
sub_eq_add_neg,

Goal state after:
S : Type v
inst✝ : Ring S
c : S
⊢ (X + -C c).nextCoeff = -c
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n - C a).degree = ↑n

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n + -C a).degree = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n - C a ≠ 0

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ X ^ n + -C a ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ (X ^ n - C r).natDegree = n

Tactic:
sub_eq_add_neg,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ (X ^ n + -C r).natDegree = n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Ring S
r : S
⊢ (X - C r).leadingCoeff = 1

Tactic:
sub_eq_add_neg,

Goal state after:
S : Type v
inst✝ : Ring S
r : S
⊢ (X + -C r).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
coeff_eq_zero_of_natDegree_lt,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ 0 * (r ^ n * if n = n then 1 else 0) = 0

R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : map f p = 0
⊢ natDegree 0 < p.natDegree

Tactic:
natDegree_zero

Goal state after:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : map f p = 0
⊢ 0 < p.natDegree
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → a ∈ f.neLocus g

Tactic:
by
  simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg (F a)

Goal state after:
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.neLocus (f - g) = g.support

Tactic:
sub_eq_add_neg,

Goal state after:
α : 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.neLocus (f + -g) = g.support
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case pos
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ↑u.support ⊆ range f
⊢ coeff s ((monomial (Finsupp.comapDomain f u ⋯)) r) = coeff (Finsupp.mapDomain f s) ((monomial u) r)

Tactic:
simp [← (Finsupp.mapDomain_injective hf).eq_iff, u.mapDomain_comapDomain _ hf h]

Goal state after:
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₁
hf : Surjective ⇑f
p : MvPolynomial σ S₁
⊢ ∃ a, (map f) a = p

Tactic:
induction p using MvPolynomial.induction_on' with
  | monomial i fr =>
    obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  | add a b ha hb =>
    obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, map_add _ _ _⟩

Goal state after: