mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2).gcd (a1 * b1) = ((c1, c2), d1, d2).2.1

Tactic:
h.1,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
cop : (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2).Coprime (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2)
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ (((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2).gcd (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1) =
    ((c1, c2), d1, d2).2.1
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ (1 - x ^ n) / (1 - x) < (1 - x)⁻¹

Tactic:
div_lt_iff₀,

Goal state after:
K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ^ n < (1 - x)⁻¹ * (1 - x)

K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 0 < 1 - x
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁹ : Semiring α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : ExistsAddOfLE α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Monovary (f ∘ ⇑σ) g

Tactic:
by
  simp [(hfg.monovaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ (∃ m, |a| ≤ m • |k| • |a|) ∧ ∃ n, |k| • |a| ≤ n • |a|

Tactic:
refine ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩

Goal state after:
case refine_1
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ |a| ≤ m • |k| • |a|

case refine_2
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ |k| • |a| ≤ n • |a|
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = f g
hr : ¬r = 0
⊢ g' ∉ ⇑f '' ((single g) r).support

Tactic:
rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]

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

Goal state before:
pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g
⊢ g ∈ x.support

Tactic:
rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this

Goal state after:
case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = y.coeff g
⊢ g ∈ x.support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : (ofLex a).coeff i = 0 ∧ (ofLex b).coeff i = 0
⊢ (ofLex a).coeff i = (ofLex b).coeff i

Tactic:
h.1,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : (ofLex a).coeff i = 0 ∧ (ofLex b).coeff i = 0
⊢ 0 = (ofLex b).coeff i
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.inl
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
⊢ ↑(#(Ico 0 (a + (b - a)))) - ↑(#(Ico 0 (-(b - a) + -a))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))

Tactic:
simp only [add_sub_cancel, neg_sub, sub_add_eq_add_sub, add_neg_cancel, zero_sub]

Goal state after:
case inr.inl
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ ((of R).symm y).coeff b + ((of R).symm z).coeff b = 0

Tactic:
h.1,

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Zero R
inst✝ : DistribSMul R V
x : R⟦Γ⟧
y z : HahnModule Γ' R V
k b : Γ'
h : ((of R).symm y).coeff b = 0 ∧ ((of R).symm z).coeff b = 0
⊢ 0 + ((of R).symm z).coeff b = 0
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
IH : mk (x ^ n) = mk (y ^ n)
⊢ mk (x ^ (n + 1)) = mk (y ^ (n + 1))

Tactic:
| succ n IH =>

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

Goal state before:
pp: case mp.left
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.orderTop = 0

pp: case mp.right
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.leadingCoeff = 1

Tactic:
· rw [← sub_add_cancel x 1, add_comm, ← orderTop_one (R := R)]
      exact orderTop_add_eq_left (Γ := Γ) (R := R) (orderTop_one (R := R) (Γ := Γ) ▸ hx)

Goal state after:
case mp.right
Γ : Type u_1
R : Type u_3
inst✝³ : LinearOrder Γ
inst✝² : Zero Γ
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
x : R⟦Γ⟧
hx : 0 < (x - 1).orderTop
⊢ x.leadingCoeff = 1
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
a : Rˣ
ha : ↑a ∈ P
⊢ ↑a⁻¹ ∈ P

Tactic:
by
  have : (a * (a⁻¹ * a⁻¹) : R) ∈ P := by aesop (config := { enableSimp := false })
  simp_all

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : RingPreordering R
inst✝ : P.HasIdealSupport
⊢ 1 ∉ P.support

Tactic:
simpa using one_notMem_supportAddSubgroup P

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

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single a) r ^ (n + 1) = (single ((n + 1) • a)) (r ^ (n + 1))

Tactic:
| succ n IH =>

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

Goal state before:
pp: case hfg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
⊢ ∀ (a_1 b : Γ),
    ¬x.coeff a_1 = 0 →
      ¬y.coeff b = 0 ∨ ¬z.coeff b = 0 → a_1 + b = x.order + a → (a_1 = x.order → ¬b = a) → y.coeff b = z.coeff b

Tactic:
rintro b c hxb - hbc hbc'

Goal state after:
case hfg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
this✝ : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
hyz : ∃ x, ¬y.coeff x = z.coeff x
this : {a | y.coeff a ≠ z.coeff a}.IsWF
a : Γ := this.min hyz
ha : y.coeff a ≠ z.coeff a
b c : Γ
hxb : ¬x.coeff b = 0
hbc : b + c = x.order + a
hbc' : b = x.order → ¬c = a
⊢ y.coeff c = z.coeff c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
by_cases h : (b : K) = 0
    · use 0
      left
      ext
      simp [h]
    by_cases h : (a : K) = 0
    · use 0; right
      ext
      simp [h]
    rcases A.mem_or_inv_mem (a / b) with hh | hh
    · use ⟨a / b, hh⟩
      right
      ext
      simp [field]
    · rw [show (a / b : K)⁻¹ = b / a by simp] at hh
      use ⟨b / a, hh⟩
      left
      ext
      simp [field]

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

Goal state before:
pp: case mp.a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ (algebraMap (↥R) K) a ∈ S

Tactic:
exact h a.2

Goal state after:
Module: Mathlib.Algebra.Order.Star.Real

Goal state before:
pp: case refine_1
x d : ℝ≥0
h : x ≤ x + d
⊢ x + d = x + star (sqrt d) * sqrt d

Tactic:
simp only [star_trivial, mul_self_sqrt]

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

Goal state before:
pp: case inr
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_of_mk_ne_zero hx]

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

Goal state before:
pp: 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✝ i : ℕ
⊢ p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
refine SetLike.le_def.mp ?_ <| subset_span <| mem_range_self i

Goal state after:
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✝ i : ℕ
⊢ span R coeffs(p) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Bivariate

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

Tactic:
induction p using Polynomial.induction_on' with
  | add p q _ _ => aesop
  | monomial m a =>
    simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
    simp [map_nsmul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ n < p.mirror.natTrailingDegree

Tactic:
mirror_natTrailingDegree

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ n < p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun₀ | 0 => n | 1 => p.natDegree - n) ∈ (p.homogenize p.natDegree).support

pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun₀ | 0 => s 0 | 1 => p.natDegree - s 0) = s

pp: case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))

Tactic:
· simpa [coeff_homogenize, mem_support_iff.mp hn]
      using Nat.add_sub_of_le <| le_natDegree_of_mem_supp n hn

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun₀ | 0 => s 0 | 1 => p.natDegree - s 0) = s

case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))
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)
⊢ (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

Tactic:
← destutter_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.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)
⊢ (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

Tactic:
← destutter_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.SumIteratedDerivative

Goal state before:
pp: ⊢ ∑ i ∈ range (X.natDegree + 1), (⇑derivative)^[i] X = X + C 1

Tactic:
natDegree_X,

Goal state after:
⊢ ∑ i ∈ range (1 + 1), (⇑derivative)^[i] X = X + C 1
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
⊢ (trinomial k m n u v w).coeff n ≠ 0

Tactic:
by rwa [trinomial_leading_coeff' hkm hmn]

Goal state after:
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
hw : w ≠ 0
⊢ (C u * X ^ (n - k) + C v * X ^ (n - m) + C w * X ^ (revAt n) n) * X ^ k = trinomial k (n - m + k) n w v u

Tactic:
revAt_le le_rfl,

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
hw : w ≠ 0
⊢ (C u * X ^ (n - k) + C v * X ^ (n - m) + C w * X ^ (n - n)) * X ^ k = trinomial k (n - m + k) n w v u
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 : 2 * ↑w * ↑u + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)
⊢ q = p ∨ q = p.mirror

Tactic:
rw [mul_assoc, hmul, ← mul_assoc, add_right_inj,
    mul_right_inj' (show 2 * (v : ℤ) ≠ 0 from mul_ne_zero two_ne_zero v.ne_zero)] 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 : ↑w + ↑u = ↑z + ↑x
⊢ q = p ∨ q = p.mirror
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₂ : 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
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (SignType.sign c₀ :: List.map (⇑SignType.sign) cs))).length

Tactic:
List.filter_cons

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₂ : 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
⊢ (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length ≤
    (List.destutter' (fun x1 x2 ↦ x1 ≠ x2) 1
        (if decide (SignType.sign c₀ ≠ 0) = true then
          SignType.sign c₀ :: List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs)
        else List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) cs))).length
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
ih : ∀ m < 0, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = 0
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
· --P is zero degree, therefore a constant.
    have hcQ : 0 < coeff P 0 := by grind [leadingCoeff]
    have hxcQ : coeff ((X - C η) * P) 1 = coeff P 0 := by
      simp_all [coeff_X_sub_C_mul, coeff_eq_zero_of_natDegree_lt]
    dsimp [signVariations, coeffList]
    rw [withBotSucc_degree_eq_natDegree_add_one hP, withBotSucc_degree_eq_natDegree_add_one h_mul]
    simp [h_deg_mul, hxcQ, hη, hcQ, hd, List.range_succ]

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ QuadraticAlgebra.C r * x = r • x

Tactic:
C_mul_eq_smul r x

Goal state after:
R : Type u_1
a b : R
inst✝ : CommSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ r • x = r • x