mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : SubmultiplicativeHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a b : α
⊢ ∀ (x : α), 0 ≤ f x

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
⊢ ∃ n, ↑n < x

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg (mk_neg x ▸ hx)
  use -n
  simpa [neg_lt]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ x * x ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ x ^ 2 ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
a✝ b✝ : R
ha : a✝ ∈ S
hb : b✝ ∈ S
⊢ a✝ * b✝ ∈ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
⊢ 1 ∈ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
a✝ b✝ : R
ha : a✝ ∈ S
hb : b✝ ∈ S
⊢ a✝ + b✝ ∈ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
S : Set R
hS : S = ↑P
⊢ 0 ∈ S

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ ∀ {a b : R}, a ∈ ↑P ∩ -↑P → b ∈ ↑P ∩ -↑P → a + b ∈ ↑P ∩ -↑P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ 0 ∈ ↑P ∩ -↑P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
⊢ ∀ {x : R}, x ∈ ↑P ∩ -↑P → -x ∈ ↑P ∩ -↑P

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ x.leadingCoeff ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
⊢ y.leadingCoeff ≠ 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
hdc : d < c
hcd : ¬↑c ≤ ↑d
⊢ (if h : d ∈ f.support then f d else 0) = f d

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: F : Type u_2
inst✝ : Field F
P : RingPreordering F
a : F
ha : a ∈ P
⊢ a * (a⁻¹ * a⁻¹) ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ 0 ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case sq_add
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x x✝ s✝ : R
hx✝ : IsSquare x✝
hs✝ : IsSumSq s✝
a✝ : s✝ ∈ P
⊢ x✝ + s✝ ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
s : Setoid α
inst✝ : Preorder β
f : α → β
hf : Monotone f
H : ∀ (x₁ x₂ : α), x₁ ≈ x₂ → f x₁ = f x₂
⊢ Monotone (Quotient.lift f H)

Tactic:
intro x y h
  induction x using Quotient.inductionOn with | h x
  induction y using Quotient.inductionOn with | h y
  induction h
  on_goal 2 => rename_i IH; apply IH.trans
  all_goals
    rename_i h
    cases h with
    | inl h => exact hf h
    | inr h => exact (H _ _ h).le

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this : ¬(a ∈ P ∨ b ∈ P)
⊢ -a ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this : ¬(a ∈ P ∨ b ∈ P)
⊢ -b ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
⊢ x ∈ P ∨ -x ∈ P

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
f : Partial seed
inst✝ : IsOrderedAddMonoid R
x y : ↥(↑f).domain
⊢ ((∃ m, |y| ≤ m • |x|) ∧ ∃ n, |x| ≤ n • |y|) ↔ (∃ m, |↑y| ≤ m • |↑x|) ∧ ∃ n, |↑x| ≤ n • |↑y|

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ a ∈ IsLocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1

Tactic:
IsLocalRing.mem_maximalIdeal

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ a ∈ nonunits ↥A ↔ A.valuation ↑a < 1
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
f : R →+*o K
r : R
hr : r ≠ 0
⊢ ArchimedeanClass.mk ↑(FiniteElement.mk (f r) ⋯) = 0

Tactic:
exact mk_map_of_archimedean' f hr

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
⊢ x ≠ 0

Tactic:
aesop

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

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧ (0, p).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
simpa using H₀ _

Goal state after:
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: case h
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := ⋯
⊢ (aeval (f x)) (derivative p) * f x′ = (aeval (f x)) (derivative p) * (f x)′

Tactic:
conv => lhs; rw [Polynomial.aeval_algHom]

Goal state after:
case h
A : Type u_1
inst✝¹¹ : CommRing A
inst✝¹⁰ : Differential A
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Differential R
inst✝⁷ : Algebra A R
inst✝⁶ : DifferentialAlgebra A R
R' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : Differential R'
inst✝³ : Algebra A R'
inst✝² : DifferentialAlgebra A R'
inst✝¹ : IsDomain R'
inst✝ : Nontrivial R
f : R →ₐ[A] R'
hf : Function.Injective ⇑f
x : R
h : IsSeparable A x
p : A[X] := minpoly A x
⊢ (f.comp (aeval x)) (derivative p) * f x′ = (aeval (f x)) (derivative p) * (f x)′
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommSemiring R
p✝ q✝ : R[X]
a✝¹ : swap (map C p✝) = C p✝
a✝ : swap (map C q✝) = C q✝
⊢ swap (map C (p✝ + q✝)) = C (p✝ + q✝)

Tactic:
aesop

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

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x y : A
p✝ q✝ : R[X][Y]
a✝¹ : (aevalAeval x y) (swap p✝) = (aevalAeval y x) p✝
a✝ : (aevalAeval x y) (swap q✝) = (aevalAeval y x) q✝
⊢ (aevalAeval x y) (swap (p✝ + q✝)) = (aevalAeval y x) (p✝ + q✝)

Tactic:
aesop

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

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
p✝ q✝ : R[X][Y]
a✝¹ : (aeval (C x)) p✝ = (mapAlgHom (aeval x)) (swap p✝)
a✝ : (aeval (C x)) q✝ = (mapAlgHom (aeval x)) (swap q✝)
⊢ (aeval (C x)) (p✝ + q✝) = (mapAlgHom (aeval x)) (swap (p✝ + q✝))

Tactic:
aesop

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

Goal state before:
pp: case add
R : Type u_2
inst✝ : CommRing R
p q : R[X][Y]
a✝¹ :
  (MvPolynomial.pderiv 0) ((equivMvPolynomial R) p) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs p))
a✝ :
  (MvPolynomial.pderiv 0) ((equivMvPolynomial R) q) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs q))
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) (p + q)) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs (p + q)))

Tactic:
aesop

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

Goal state before:
pp: case monomial.add
R : Type u_2
inst✝ : CommRing R
n : ℕ
p q : R[X]
a✝¹ :
  (MvPolynomial.pderiv 0) ((equivMvPolynomial R) ((monomial n) p)) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs ((monomial n) p)))
a✝ :
  (MvPolynomial.pderiv 0) ((equivMvPolynomial R) ((monomial n) q)) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs ((monomial n) q)))
⊢ (MvPolynomial.pderiv 0) ((equivMvPolynomial R) ((monomial n) (p + q))) =
    (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs ((monomial n) (p + q))))

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
by
  rcases subsingleton_or_nontrivial R with H | H
  · simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hp hq ⊢
    exact ⟨hp, hq⟩
  refine ⟨?_, hp.monic.mul hq.monic⟩
  have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, hq.leadingCoeff_eq, one_mul]
    exact one_ne_zero
  rw [natDegree_mul' this, hp.natDegree_eq, hq.natDegree_eq]

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

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommSemiring R
p q : R[X][Y]
a✝¹ : (MvPolynomial.pderiv 1) ((equivMvPolynomial R) p) = (equivMvPolynomial R) (derivative p)
a✝ : (MvPolynomial.pderiv 1) ((equivMvPolynomial R) q) = (equivMvPolynomial R) (derivative q)
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) (p + q)) = (equivMvPolynomial R) (derivative (p + q))

Tactic:
aesop

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

Goal state before:
pp: case monomial.add
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p q : R[X]
a✝¹ :
  (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) p)) = (equivMvPolynomial R) (derivative ((monomial n) p))
a✝ :
  (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) q)) = (equivMvPolynomial R) (derivative ((monomial n) q))
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) (p + q))) =
    (equivMvPolynomial R) (derivative ((monomial n) (p + q)))

Tactic:
aesop

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : p.natTrailingDegree ≤ n
⊢ p.reverse.coeff (n - p.natTrailingDegree) = p.coeff (p.natDegree - (n - p.natTrailingDegree))

Tactic:
coeff_reverse,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : p.natTrailingDegree ≤ n
⊢ p.coeff ((revAt p.natDegree) (n - p.natTrailingDegree)) = p.coeff (p.natDegree - (n - p.natTrailingDegree))
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ f

Tactic:
rw [fgh]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ g * h
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ f

Tactic:
rw [fgh]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ g * h
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
this : (fun₀ | 0 => m 0 | 1 => m 1) = m
⊢ (if (fun₀ | 0 => k | 1 => n - k) = m then c else 0) = if m 0 + m 1 = n then if k = m 0 then c else 0 else 0

Tactic:
aesop

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

Goal state before:
pp: case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (p i * ∏ i ∈ s, p i).homogenize (n i + ∑ i ∈ s, n i) = (p i).homogenize (n i) * ∏ i ∈ s, (p i).homogenize (n i)

Tactic:
rw [homogenize_mul _ _ h.1, ihs h.2]

Goal state after:
case cons
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
p : ι → R[X]
n : ι → ℕ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ i ∈ s, (p i).natDegree ≤ n i) → (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)
h : (p i).natDegree ≤ n i ∧ ∀ x ∈ s, (p x).natDegree ≤ n x
⊢ (∏ i ∈ s, p i).natDegree ≤ ∑ i ∈ s, n i
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 0) = p * (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 1)

Tactic:
by
  simp [toTupleMvPolynomial]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
⊢ p.smeval 0 = p.coeff 0 • 1

Tactic:
induction p using Polynomial.induction_on' with
  | add p q ph qh => simp_all only [smeval_add, coeff_add, add_smul]
  | monomial n a =>
    cases n with
    | zero => simp only [monomial_zero_left, smeval_C, npow_zero, coeff_C_zero]
    | succ n => rw [coeff_monomial_succ, smeval_monomial, npow_add, npow_one, mul_zero, zero_smul,
        smul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
⊢ (p * X ^ 0).smeval x = p.smeval x * x ^ 0

Tactic:
simp only [npow_zero, mul_one]

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

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
⊢ ¬IsUnit p

Tactic:
obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
  exact fun h =>
    ne_zero_of_lt hmn
      ((trinomial_natDegree hkm hmn w.ne_zero).symm.trans
        (natDegree_eq_of_degree_eq_some (degree_eq_zero_of_isUnit h)))

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
obtain ⟨p', p'_le, hp'⟩ := exists_iterate_derivative_eq_factorial_smul p k

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q k : ℕ
hk : q ≤ k
p' : R[X]
p'_le : p'.natDegree ≤ p.natDegree - k
hp' : (⇑derivative)^[k] p = k ! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ ((X - C η) * P).natDegree = P.natDegree + 1

Tactic:
natDegree_mul h₅ h₃,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
⊢ (X - C η).natDegree + P.natDegree = P.natDegree + 1
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ x ∈ Ico q (p.natDegree + 1)
⊢ False

Tactic:
mem_Ico

Goal state after:
case inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1
⊢ False
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: case h
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
⊢ (mk rels) a ∈ closure (range (of rels))

Tactic:
induction a with

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

Goal state before:
pp: case isTrue.isTrue.cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs✝ : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
r : SignType
rs : List SignType
hcs : List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs) = r :: rs
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2) (1 :: r :: rs)).length ≤
    (1 :: List.destutter' (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀) (r :: rs)).length

Tactic:
← List.destutter_cons'

Goal state after:
case isTrue.isTrue.cons
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h : 0 < P.leadingCoeff
h₂ : 0 < P.nextCoeff
c₀ : R
cs : List R
hcs✝ : ((X - C η) * P).coeffList = P.leadingCoeff :: c₀ :: cs
hecs : ((X - C η) * P.eraseLead).coeffList = P.nextCoeff :: cs
h✝¹ : decide (SignType.sign c₀ ≠ 0) = true
h✝ : 1 ≠ SignType.sign c₀
r : SignType
rs : List SignType
hcs : List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs) = r :: rs
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2) (1 :: r :: rs)).length ≤
    (1 :: List.destutter (fun x1 x2 ↦ x1 ≠ x2) (SignType.sign c₀ :: r :: rs)).length
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
h : z.im = 0
hz : z.re = 0
⊢ z = 0

Tactic:
aesop

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re ^ 2 + b * z.re * z.im = a * z.im * z.im
h : ¬z.im = 0
⊢ False

Tactic:
← eq_sub_iff_add_eq

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re ^ 2 = a * z.im * z.im - b * z.re * z.im
h : ¬z.im = 0
⊢ False