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

Goal state before:
pp: R : Type u_4
inst✝⁷ : CommSemiring R
S : Submonoid R
R' : Type u_5
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
inst✝⁴ : IsLocalization S R'
M' : Type u_6
inst✝³ : AddCommMonoid M'
inst✝² : Module R' M'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
⊢ x ∈ N'

Tactic:
← Submodule.smul_mem_iff_of_isUnit (r := algebraMap R R' s) N' (map_units R' s),

Goal state after:
R : Type u_4
inst✝⁷ : CommSemiring R
S : Submonoid R
R' : Type u_5
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
inst✝⁴ : IsLocalization S R'
M' : Type u_6
inst✝³ : AddCommMonoid M'
inst✝² : Module R' M'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
⊢ (algebraMap R R') ↑s • x ∈ N'
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
K : Type u_5
inst✝⁴ : Field K
L : Type u_7
inst✝³ : Field L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : Algebra A L
f : L →ₐ[A] K
x : K
⊢ ∃ a, f a = x

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A x

Goal state after:
A : Type u_4
inst✝⁵ : CommRing A
K : Type u_5
inst✝⁴ : Field K
L : Type u_7
inst✝³ : Field L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : Algebra A L
f : L →ₐ[A] K
x y : A
hy : y ∈ A⁰
⊢ ∃ a, f a = (algebraMap A K) x / (algebraMap A K) y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e'_3
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ M = Submonoid.map (↑h).symm (Submonoid.map (↑h) M)

Tactic:
←
      Submonoid.comap_equiv_eq_map_symm,

Goal state after:
case e'_3
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ M = Submonoid.comap (↑h) (Submonoid.map (↑h) M)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
⊢ (algebraMap R S) x = 0 ↔ x = 0

Tactic:
by
  constructor <;> intro h
  · obtain ⟨c, hc⟩ := (map_eq_zero_iff M _ _).mp h
    exact (hM c.2).1 x hc
  · rw [h, map_zero]

Goal state after:
Module: Mathlib.Tactic.NoncommRing

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ r * OfNat.ofNat n = OfNat.ofNat n • r

Tactic:
by
  simp only [nsmul_eq_mul', Nat.cast_ofNat]

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
⊢ NonUnitalNonAssocRing α

Tactic:
let sub := e.sub

Goal state after:
α : 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
⊢ NonUnitalNonAssocRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
⊢ NonUnitalRing α

Tactic:
let sub := e.sub

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
⊢ NonUnitalRing α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
⊢ NonUnitalCommRing α

Tactic:
let sub := e.sub

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
⊢ NonUnitalCommRing α
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 b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit ha) * (↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb) - ↑(IsUnit.unit hb)⁻¹ * ↑(IsUnit.unit hb)) = a - b

Tactic:
Units.inv_mul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit ha) * (↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb) - 1) = a - b
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : ↥(unitsFstOne R A)
⊢ PreQuasiregular.equiv.symm (PreQuasiregular.equiv (↑↑x).toProd.2 * PreQuasiregular.equiv (↑↑x⁻¹).toProd.2) =
    PreQuasiregular.equiv.symm 1

Tactic:
simpa [-Units.mul_inv] using congr($(x.val.mul_inv).snd)

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ quasispectrum R a = spectrum R ↑a

Tactic:
ext r
  have : { r | ¬ IsUnit r} ⊆ spectrum R _ := mem_spectrum_inr_of_not_isUnit a
  rw [← Set.union_eq_left.mpr this, ← quasispectrum_eq_spectrum_union]
  apply forall_congr' fun hr ↦ ?_
  rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

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

Goal state before:
pp: case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (b * a)

Tactic:
exact fun _ ↦ quasispectrum.not_isUnit_mem _

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

Goal state before:
pp: case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)

Tactic:
exact fun _ ↦ quasispectrum.not_isUnit_mem _

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ f '' quasispectrum S a = quasispectrum R a

Tactic:
by
  simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ f '' spectrum S a = spectrum R a

Tactic:
by
  simp only [← h.algebraMap_image, Set.image_image, h.left_inv _, Set.image_id']

Goal state after:
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
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case inl.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
refine ⟨s.toFinset, by simpa using hs', by simpa⟩

Goal state after:
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
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
v : V
hv : v ≠ 0
w : V'
hw : w ≠ 0
⊢ v ∉ ⊥

Tactic:
simp only [mem_bot, hv, not_false_eq_true]

Goal state after:
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
κ : Type v
b : Basis κ K V
⊢ Module.rank K V ≤ 1 → ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v

Tactic:
intro hd
    rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd
    rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩
    · use 0
      have h' : ∀ v : V, v = 0 := by
        simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.symm
      intro v
      simp [h' v]
    · use b i
      have h' : K ∙ b i = ⊤ :=
        (subsingleton_range b).eq_singleton_of_mem (mem_range_self i) ▸ b.span_eq
      intro v
      have hv : v ∈ (⊤ : Submodule K V) := mem_top
      rwa [← h', mem_span_singleton] at hv

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ ≤ 1

case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥
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:
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)

Goal state after:
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
this : Surjective ⇑(LinearMap.mulLeft F x)
⊢ ∃ y, x * y = 1
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_assoc
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✝ * c✝))

Tactic:
change _ * _ * _ = _ * (_ * _)

Goal state after:
case mul_assoc
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✝ * liftFun R X f b✝ * liftFun R X f c✝ = liftFun R X f a✝ * (liftFun R X f b✝ * liftFun R X f c✝)
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
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R) ((lift R).symm g) = g

Tactic:
exact (lift R).apply_symm_apply g

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.comp 0 = C (eval 0 p)

Tactic:
by rw [← C_0, comp_C]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ map f (p * q) = map f p * map f q

Tactic:
map,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ eval₂ (C.comp f) X (p * q) = eval₂ (C.comp f) X p * eval₂ (C.comp f) X q
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ ¬True
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
_root_.not_true,

Goal state after:
n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ False
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * (C r * X ^ n)).coeff (d + n) = p.coeff d * r

Tactic:
← X_pow_mul,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * (X ^ n * C r)).coeff (d + n) = p.coeff d * r
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
n : ℕ
f : R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
exact degtm _ _

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
exact degtm _ _

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ (∑ i ∈ cons a s has, f i).degree ≤ max (f a).degree (∑ i ∈ s, f i).degree

Tactic:
rw [Finset.sum_cons]; exact degree_add_le _ _

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
leadingCoeff_monomial

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ a = a
Module: Mathlib.Algebra.MonoidAlgebra.Degree

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

Tactic:
intro h; rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ antidiagonal (p.natDegree + q.natDegree)
⊢ (p.natDegree, q.natDegree) ∈ antidiagonal (p.natDegree + q.natDegree)

Tactic:
rw [mem_antidiagonal]

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).leadingCoeff = a

Tactic:
rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]

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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg) ∈ antidiagonal (df + dg)

Tactic:
rw [mem_antidiagonal]

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 : ℕ
⊢ (map f p).coeff n = f (p.coeff n)

Tactic:
map,

Goal state after:
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)
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
h✝ : Nontrivial R
⊢ ¬leadingCoeff D p = 0

Tactic:
leadingCoeff_eq_zero hD,

Goal state after:
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
h✝ : Nontrivial R
⊢ ¬p = 0
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
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ ¬leadingCoeff D q = 0

Tactic:
leadingCoeff_eq_zero hD,

Goal state after:
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
hp : Monic D p
hq : q ≠ 0
h✝ : Nontrivial R
⊢ ¬q = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i

Tactic:
rw [eval_eq_sum, sum_over_range]; simp

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

Goal state before:
pp: case zero
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 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D (single 0 1) = 0

Tactic:
supDegree_single 0 1,

Goal state after:
case zero
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 : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ (if 1 = 0 then ⊥ else D 0) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_map]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
hp0 : p ≠ 0
⊢ f (p.coeff p.natDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p

Tactic:
rw [comp, p.as_sum_range]

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))) =
    eval₂ f (eval₂ f x q) (∑ i ∈ range (p.natDegree + 1), (monomial i) (p.coeff i))
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
⊢ ¬∀ (x : A[X]), x ∈ ⊥ ↔ x ∈ ⊤

Tactic:
not_forall

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
⊢ ∃ x, ¬(x ∈ ⊥ ↔ x ∈ ⊤)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
x : R
⊢ ¬∀ (n : ℕ), (C ((algebraMap R A) x)).coeff n = X.coeff n

Tactic:
not_forall

Goal state after:
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
x : R
⊢ ∃ x_1, ¬(C ((algebraMap R A) x)).coeff x_1 = X.coeff x_1
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
⊢ IsLowerSet (Set.range (embDomain f))

Tactic:
by
  rintro _ y h ⟨z, rfl⟩
  obtain ⟨w, hw⟩ := exists_add_of_le h
  rw [mem_range_embDomain_iff]
  trans ↑(y + w).support
  · exact fun _ ↦ by simp; grind
  · simp [← hw]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h : a ≠ b
⊢ False

Tactic:
Function.ne_iff

Goal state after:
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h : ∃ a_1, a a_1 ≠ b a_1
⊢ False
Module: Mathlib.Order.PiLex

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

Tactic:
ofColex_apply

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

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

Tactic:
rw [← leadingCoeff_eq_zero]

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q.leadingCoeff = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
r : R
⊢ (C r).coeffs = if r = 0 then ∅ else {r}

Tactic:
by
  classical
  aesop (add simp mem_coeffs_iff)

Goal state after: