mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
⊢ (x - y).map f = x.map f - y.map f

Tactic:
ext; simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
⊢ (r • x).map f = r • x.map f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
⊢ 0 ∈ Icc 0 a

Tactic:
by simpa using! ha.le

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
H : IsMax ⟨0, ⋯⟩
⊢ a ∈ Icc 0 a

Tactic:
by simpa using! ha.le

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
α : Type u_2
inst✝ : Add α
f : α → R
hf : ∀ (x : α), 0 ≤ f x
hna : IsNonarchimedean f
a b : α
⊢ f (a + b) ≤ f a + f b

Tactic:
by
  apply le_trans (hna _ _)
  rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]
  exact ⟨hf _, hf _⟩

Goal state after:
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✝⁴ : AddMonoidWithOne α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
⊢ f ↑n ≤ 1

Tactic:
← nsmul_one n,

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : AddMonoidWithOne α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
⊢ f (n • 1) ≤ 1
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✝⁴ : AddMonoidWithOne α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
⊢ f ↑n ≤ 1

Tactic:
rw [← nsmul_one n, ← map_one f]

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝⁴ : AddMonoidWithOne α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
⊢ f (n • 1) ≤ f 1
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
hxy : (of R).symm (x • y) = 0
⊢ ↑(⋯.min ⋯) ≤ ((of R).symm (x • y)).orderTop

Tactic:
rw [hxy, HahnSeries.orderTop_zero]

Goal state after:
case pos
R : Type u_3
V : Type u_5
inst✝⁷ : AddCommMonoid V
Γ : Type u_6
Γ' : Type u_7
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : MulZeroClass R
inst✝¹ : SMulWithZero R V
x : R⟦Γ⟧
inst✝ : VAdd (WithTop Γ) (WithTop Γ')
y : HahnModule Γ' R V
h : ∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ'
hx : ¬x = 0
hy : ¬y = 0
hhy : (of R).symm y ≠ 0
hxy : (of R).symm (x • y) = 0
⊢ ↑(⋯.min ⋯) ≤ ⊤
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
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
hferase :
  (f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)) = ∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x)
hmono : StrictMonoOn (fun x ↦ ArchimedeanClass.mk ↑(f x)) ↑f.support
hsupport' : (f.support.erase (f.support.min' hsupport)).Nonempty
⊢ ↑(f ((f.support.erase (f.support.min' hsupport)).min' hsupport')) ≠ 0

Tactic:
simpa using! (Finset.mem_erase.mp <| (f.support.erase _).min'_mem hsupport').2

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
⊢ -⊤ = ⊤

Tactic:
by simp [← mk_zero, ← mk_inv]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
⊢ Injective ⇑C

Tactic:
intro r s rs
  rw [HahnSeries.ext_iff, funext_iff] at rs
  have h := rs 0
  rwa [C_apply, coeff_single_same, C_apply, coeff_single_same] at h

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ conjneg (conjneg f) = f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
⊢ conjneg 0 = 0

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
⊢ conjneg 1 = 1

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
⊢ conjneg (f + g) = conjneg f + conjneg g

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f g : G → R
⊢ conjneg (f * g) = conjneg f * conjneg g

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
⊢ conjneg (∑ i ∈ s, f i) = ∑ i ∈ s, conjneg (f i)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
⊢ conjneg (∏ i ∈ s, f i) = ∏ i ∈ s, conjneg (f i)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ conjneg f = 1 ↔ f = 1

Tactic:
rw [← conjneg_inj, conjneg_conjneg, conjneg_one]

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f g : G → R
⊢ conjneg (f - g) = conjneg f - conjneg g

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f : G → R
⊢ conjneg (-f) = -conjneg f

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : NonUnitalSemiring α
inst✝⁶ : NonUnitalSemiring β
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : StarRing α
inst✝² : StarRing β
inst✝¹ : StarOrderedRing α
inst✝ : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
this :
  closure (Set.range fun s ↦ star s * s) =
    (closure (Set.range fun s ↦ star s * s)).prod (closure (Set.range fun s ↦ star s * s))
⊢ (xa, xy) ≤ (ya, yb) ↔ ∃ p ∈ closure (Set.range fun s ↦ star s * s), (ya, yb) = (xa, xy) + p

Tactic:
simp only [mk_le_mk, Prod.exists, mk_add_mk, mk.injEq, StarOrderedRing.le_iff, this,
      AddSubmonoid.mem_prod, exists_and_exists_comm, and_and_and_comm]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ (OrderDual.ofDual.trans A.primeSpectrumEquiv) a ≤ (OrderDual.ofDual.trans A.primeSpectrumEquiv) b

Tactic:
by apply ofPrime_le_of_le; exact h

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x y : FiniteElement K
⊢ mk x = mk y ↔ 0 < ArchimedeanClass.mk (↑x - ↑y)

Tactic:
apply Quotient.eq.trans
  rw [Submodule.quotientRel_def, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
    FiniteElement.not_isUnit_iff_mk_pos, AddSubgroupClass.coe_sub]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure s * upperClosure t)

Tactic:
UpperSet.coe_mul,

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure s) * ↑(upperClosure t)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
b : α
⊢ stabilizer G {b} = stabilizer G b

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : DecidableEq α
b : α
⊢ stabilizer G {b} = stabilizer G b

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
a : G
inst✝ : DecidableEq α
s : Finset α
⊢ a ∈ stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s

Tactic:
simp_rw [← stabilizer_coe_finset, mem_stabilizer_set, Finset.mem_coe]

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
h✝ : mk x ≠ 0
h : mk x < 0
⊢ stdPart x = 0

Tactic:
exact dif_neg h.not_ge

Goal state after:
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
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
this : FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯ = 1
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) 1 = 1

Tactic:
map_one

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
hx' : 0 ≤ mk x⁻¹
this : FiniteElement.mk x⁻¹ hx' * FiniteElement.mk x ⋯ = 1
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse)[k]?

Tactic:
rw [List.getElem?_append_right (List.length_replicate ▸ hkn),
      List.length_replicate, List.getElem?_reverse, List.getElem?_map]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    Option.map P.eraseLead.coeff
      (List.range
          P.eraseLead.degree.succ)[(List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length - 1 -
          (k - n)]?

case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
P : R[X]
hp : P = 0
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList

pp: case neg
R : Type u_1
inst✝ : Ring R
P : R[X]
hp : ¬P = 0
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList

Tactic:
· rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
P : R[X]
hp : ¬P = 0
⊢ (-P).coeffList = List.map (fun x ↦ -x) P.coeffList
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
l : Multiset R[X][Y]
⊢ evalEval x y l.prod = (Multiset.map (evalEval x y) l).prod

Tactic:
by
  simp [evalEval, eval_multiset_prod, Multiset.map_map]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : R[X][Y] →ₐ[R] A
⊢ ((fun xy ↦
            (AlgHom.restrictScalars R (aeval xy.1)).comp
              (let this := algebra;
              AlgHom.restrictScalars R (aeval (C xy.2))))
          ((fun f ↦ (f (C X), f Y)) f)).comp
      CAlgHom =
    f.comp CAlgHom

Tactic:
ext; simp

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
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
⊢ seed.baseEmbedding ≤ sSupFun hc

Tactic:
by
  obtain ⟨f, hf⟩ := hnonempty
  exact le_trans f.prop.baseEmbedding_le (le_sSupFun hc hf)

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ (p - X ^ n).natDegree < n

Tactic:
by
  obtain ⟨q, hq₁, hq₂⟩ := hp.exists_natDegree_lt hn
  simpa [hq₁]

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))
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))

Tactic:
have := hl a (by simp) b (by simp)

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 (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p.Monic
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
hp1 : p ≠ 1
⊢ 3 / 2 ≤ p.natDegree / 2

Tactic:
apply Nat.div_le_div_right (c := 2) hp2

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (SignType.sign P.leadingCoeff ::
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
if_pos ?_

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ (SignType.sign P.leadingCoeff ::
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.eraseLead.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      1

R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
cs : List R
h_eL : P.eraseLead.coeffList = P.eraseLead.leadingCoeff :: cs
h₁ : SignType.sign P.eraseLead.leadingCoeff ≠ 0
h₄ : ¬SignType.sign P.leadingCoeff = SignType.sign P.eraseLead.leadingCoeff
⊢ SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.map (fun x ↦ -x)
          (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (List.map (⇑SignType.sign)
              (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
List.length_map

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (List.map (⇑SignType.sign)
            (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case e_a.e_a.e_l.e_f
R✝ : Type u_1
inst✝⁴ : Ring R✝
inst✝³ : LinearOrder R✝
η✝ : R✝
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
P : R[X]
hx : η ≠ 0
hx2 : 0 < η
x✝ : R
⊢ (⇑SignType.sign ∘ fun x ↦ η * x) x✝ = SignType.sign x✝

Tactic:
simp [hx2, sign_mul]

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

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

Tactic:
trinomial_mirror hkm' hmn' w.ne_zero u.ne_zero

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x = (0 - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1

Tactic:
hp0,

Goal state after:
case cons
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
q₁ q₂ : R[X]
r₁ r₂ : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      (∀ i ∈ s, (r₁ i).degree < (g i).degree) →
        (∀ i ∈ s, (r₂ i).degree < (g i).degree) →
          q₁ * ∏ i ∈ s, g i + ∑ i ∈ s, r₁ i * ∏ k ∈ s.erase i, g k =
              q₂ * ∏ i ∈ s, g i + ∑ i ∈ s, r₂ i * ∏ k ∈ s.erase i, g k →
            q₁ = q₂ ∧ ∀ i ∈ s, r₁ i = r₂ i
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
hr₁ : (r₁ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₁ x).degree < (g x).degree
hr₂ : (r₂ i).degree < (g i).degree ∧ ∀ x ∈ s, (r₂ x).degree < (g x).degree
cop : IsCoprime (g i) (∏ i ∈ s, g i)
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
hgid : g i ∣ r₂ i - r₁ i
hf : g i * 0 = (0 - g i * (q₁ - q₂)) * ∏ x ∈ s, g x
hpgd : ∏ i ∈ s, g i ∣ ∑ x ∈ s, (r₁ x - r₂ x) * ∏ x ∈ s.erase x, g x
hdr : (r₂ i - r₁ i).degree < (g i).degree
hr0 : r₂ i - r₁ i = 0
hpm : (∏ i ∈ s, g i).Monic
hdp : (∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k).degree < (∏ i ∈ s, g i).degree
hp0 : ∑ i ∈ s, (r₁ i - r₂ i) * ∏ k ∈ s.erase i, g k = 0
⊢ q₁ = q₂ ∧ ∀ i_1 ∈ Finset.cons i s hi, r₁ i_1 = r₂ i_1