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

Goal state before:
pp: case e'_3
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : 0 < mk x
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of ↑x)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of ↑y)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of ↑x)| = ↑x

pp: case e'_4
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : 0 < mk x
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of ↑x)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of ↑y)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of ↑y)| = ↑y

Tactic:
· exact abs_of_pos <| lt_of_mk_lt_mk hx

Goal state after:
case e'_4
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk y
hx : 0 < mk x
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of ↑x)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of ↑y)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of ↑y)| = ↑y
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
h : 0 ≤ x
hx : mk x = 0
⊢ 0 ≤ stdPart x

Tactic:
rw [stdPart, dif_pos hx.ge]

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : 0 ≤ x
hx : mk x = 0
⊢ 0 ≤ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk x ⋯)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h : 0 ≤ x
⊢ 0 ≤ stdPart x

Tactic:
by
  obtain hx | hx := eq_or_ne (ArchimedeanClass.mk x) 0
  · rw [stdPart, dif_pos hx.ge]
    exact map_nonneg _ h
  · rw [stdPart_of_mk_ne_zero hx]

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

Goal state before:
pp: case a
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
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
⊢ f ≤ f.extend hx

Tactic:
change f.val ≤ (f.extend hx).val

Goal state after:
case a
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
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
⊢ ↑f ≤ ↑(f.extend hx)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v)

Tactic:
by
  rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (f a :: f b :: map f l)

Tactic:
destutter_cons_cons,

Goal state after:
α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
this : R a b ↔ R₂ (f a) (f b)
⊢ map f (if R a b then a :: destutter' R b l else destutter' R a l) =
    if R₂ (f a) (f b) then f a :: destutter' R₂ (f b) (map f l) else destutter' R₂ (f a) (map f l)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case ha
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 1 ≠ 0

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ k ≤ n

pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 1 ^ 0 = 1

pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 0 ^ 0 = 1

pp: case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

pp: case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0

Tactic:
all_goals simp_all [pow_add]

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

pp: case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
· have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
      simp [destutter', if_pos hac, if_pos (not_not.1 hbc), if_neg hab]

Goal state after:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup

Tactic:
destutter_cons_cons,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
⊢ (if x ≠ y then x :: destutter' (fun x1 x2 ↦ x1 ≠ x2) y xs else destutter' (fun x1 x2 ↦ x1 ≠ x2) x xs) =
    (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑i ≤ ↑n

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at h

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑i ≤ ↑n
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑k ≤ ↑i

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at h

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑k ≤ ↑i
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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval₂ (algebraMap R A) r ((⇑derivative)^[k] p) = 0

Tactic:
eval₂_eq_eval_map,

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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r (map (algebraMap R A) ((⇑derivative)^[k] p)) = 0
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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval₂ (algebraMap R A) r ((⇑derivative)^[q] p) = q ! • eval r p'

Tactic:
eval₂_eq_eval_map,

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 : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r (map (algebraMap R A) ((⇑derivative)^[q] p)) = q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
⊢ ((monomial d) c).signVariations = 0

Tactic:
by_cases hcz : c = 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : c = 0
⊢ ((monomial d) c).signVariations = 0

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (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 * p'
⊢ (aeval r) (sumIDeriv p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)

Tactic:
rw [sumIDeriv_apply, map_sum]

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (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 * p'
⊢ ∑ x ∈ range (p.natDegree + 1), (aeval r) ((⇑derivative)^[x] p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)
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 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * P.eraseLead - (monomial P.natDegree) P.eraseLead.leadingCoeff

Tactic:
leadingCoeff_eraseLead_eq_nextCoeff hc.ne,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : eval 1 (p * p.mirror) = eval 1 (q * q.mirror)
⊢ q = p ∨ q = p.mirror

Tactic:
rw [eval_mul, eval_mul, mirror_eval_one, mirror_eval_one, ← sq, ← sq, hp, hq] at hadd

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : eval 1 (trinomial k m n ↑u ↑v ↑w) ^ 2 = eval 1 (trinomial k m' n ↑x ↑v ↑z) ^ 2
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl.inl
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
h2 : q = p
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
exact Or.inl h2

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

Goal state before:
pp: case h.right
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)
⊢ P.eraseLead.leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)

Tactic:
h₂

Goal state after:
case h.right
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)
⊢ P.nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList) =
    P.nextCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ AddGroup (QuadraticAlgebra R a b)

Tactic:
refine (equivProd a b).injective.addGroup _ rfl ?_ ?_ ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x + y) = (equivProd a b) x + (equivProd a b) y

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b), (equivProd a b) (-x) = -(equivProd a b) x

case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x y : QuadraticAlgebra R a b), (equivProd a b) (x - y) = (equivProd a b) x - (equivProd a b) y

case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℕ), (equivProd a b) (n • x) = n • (equivProd a b) x

case refine_5
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddGroup R
⊢ ∀ (x : QuadraticAlgebra R a b) (n : ℤ), (equivProd a b) (n • x) = n • (equivProd a b) x
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a✝ b✝ : R
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
q : ℚ
x : QuadraticAlgebra K a b
⊢ q • x = ↑q * x

Tactic:
ext <;> simp [Rat.smul_def]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
⊢ Multiset.countP (fun x ↦ 0 < x) P.roots ≤ P.signVariations

Tactic:
generalize h : P.roots.countP (0 < ·) = num_pos_roots
  induction num_pos_roots generalizing P -- Induct on number of roots.
  · exact zero_le
  rename_i ih
  have hp : P ≠ 0 := by grind [roots_zero, Multiset.countP_zero]
  -- we can take a positive root, η, because the number of roots is positive
  obtain ⟨η, η_root, η_pos⟩ : ∃ x, x ∈ P.roots ∧ 0 < x := by grind [Multiset.countP_pos]
  -- (X - η) divides P(X), so write P(X) = (X - η) * Q(X)
  obtain ⟨Q, rfl⟩ := dvd_iff_isRoot.mpr (isRoot_of_mem_roots η_root)
  -- P has at least num_roots sign variations
  grw [ih Q, succ_signVariations_le_X_sub_C_mul η_pos]
  · exact right_ne_zero_of_mul hp
  · simp [← h, roots_mul (ne_zero_of_mem_roots η_root), η_pos, ← Nat.succ.injEq]

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

Goal state before:
pp: R : Type u
inst₁ inst₂ : NonAssocRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
    ext : 1 <;> assumption
  have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
    ext : 1 <;> assumption
  -- Mathematically non-trivial fact: `intCast` is determined by the rest.
  have h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne :=
    AddCommGroupWithOne.ext h_add (congrArg (·.toOne.one) h₂)
  cases inst₁; cases inst₂
  congr <;> solve | injection h₁ | injection h₂ | injection h₃

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsFormallyReal R
⊢ IsReduced R

Tactic:
by
  rw [isReduced_iff_pow_one_lt 2 (by lia)]
  intro x hx
  by_contra! hc
  exact not_isSumNonzeroSq_zero <| by simpa [← pow_two, hx] using IsSumNonzeroSq.sq hc

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁸ : CommSemiring k
inst✝⁷ : Monoid G
inst✝⁶ : Monoid H
A : Type u_4
B : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : Algebra k A
inst✝³ : Semiring B
inst✝² : Algebra k B
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
⊢ SkewMonoidAlgebra k G →ₐ[k] A

Tactic:
by
    apply liftNCAlgHom (Algebra.ofId k A) F
    simp_rw [show ∀ (g : G) (r : k), g • r = r by
        exact fun _ _ ↦ smul_algebraMap _ (algebraMap k k _)]
    exact Algebra.commutes _ _

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.symm
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x✝¹ y✝¹ : R
hab : Rel r x✝¹ y✝¹
c d x✝ y✝ : R
a✝ : Relation.EqvGen (Rel r) x✝ y✝
h : Relation.EqvGen (Rel r) (y✝¹ * x✝) (y✝¹ * y✝)
⊢ Relation.EqvGen (Rel r) (y✝¹ * y✝) (y✝¹ * x✝)

Tactic:
| symm _ _ _ h =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.symm
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x✝¹ c d x✝ y✝ : R
a✝ : Relation.EqvGen (Rel r) x✝ y✝
h : Relation.EqvGen (Rel r) (x✝¹ * x✝) (x✝¹ * y✝)
⊢ Relation.EqvGen (Rel r) (x✝¹ * y✝) (x✝¹ * x✝)

Tactic:
| symm _ _ _ h =>

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case rel.symm
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x✝¹ y✝¹ : R
hab : Rel r x✝¹ y✝¹
c d x✝ y✝ : R
a✝ : Relation.EqvGen (Rel r) x✝ y✝
h : Relation.EqvGen (Rel r) (y✝¹ + x✝) (y✝¹ + y✝)
⊢ Relation.EqvGen (Rel r) (y✝¹ + y✝) (y✝¹ + x✝)

Tactic:
| symm _ _ _ h =>

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x * x_1) f.support
⊢ ∃ a ∈ f.support, x * a = y

Tactic:
by
    simpa only [Finset.mem_image, exists_prop] using hy

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case refl.symm
R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : R → R → Prop
a b x✝¹ c d x✝ y✝ : R
a✝ : Relation.EqvGen (Rel r) x✝ y✝
h : Relation.EqvGen (Rel r) (x✝¹ + x✝) (x✝¹ + y✝)
⊢ Relation.EqvGen (Rel r) (x✝¹ + y✝) (x✝¹ + x✝)

Tactic:
| symm _ _ _ h =>

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.support
⊢ ∃ a ∈ f.support, a * x = y

Tactic:
by
    simpa only [Finset.mem_image, exists_prop] using hy

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
ext a
  simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Semiring k
inst✝¹ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst✝ : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
by
  classical
  ext a
  simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (monomial 0) 1 = X ^ 0

Tactic:
simp only [monomial_zero_left, ← CRingHom_eq_C, map_one, pow_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
a b : Tropical (WithTop R)
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
by
  simp [← untrop_inj_iff, WithTop.add_eq_top]

Goal state after:
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)
  · simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]
  · rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']

Goal state after: