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

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2).IsPWO

Tactic:
refine Set.IsPWO.mono x.isPWO_support' ?_

Goal state after:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2) ⊆ Function.support x.coeff
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ x.orderTop ≤ ↑g

Tactic:
rw [orderTop_of_ne_zero (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]

Goal state after:
R : Type u_3
inst✝¹ : Zero R
Γ : Type u_5
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ ⋯.min ⋯ ≤ g
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s✝ : Finset α
x : α → R⟦Γ⟧
g : Γ
i : α
s : Finset α
his : i ∉ s
hsum : (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g
⊢ (x i).coeff g + (∑ x_1 ∈ s, x x_1).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g

Tactic:
hsum

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s✝ : Finset α
x : α → R⟦Γ⟧
g : Γ
i : α
s : Finset α
his : i ∉ s
hsum : (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g
⊢ (x i).coeff g + ∑ i ∈ s, (x i).coeff g = (x i).coeff g + ∑ x_1 ∈ s, (x x_1).coeff g
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 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))

Tactic:
obtain hb' | hb' := le_total 0 b

Goal state after:
case inr.inl.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
hb' : 0 ≤ b
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))

case inr.inl.inr
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
hb' : b ≤ 0
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * (y ⊔ z) = x * y ⊔ x * z

Tactic:
← iSup_pair,

Goal state after:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * (y ⊔ z) = ⨆ x_1 ∈ {y, z}, x * x_1
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x✝¹ x✝ : { a // a ≠ 0 }
a : Lex R⟦Γ⟧
ha : a ≠ 0
b : Lex R⟦Γ⟧
hb : b ≠ 0
h : ArchimedeanClass.mk ↑⟨a, ha⟩ ≤ ArchimedeanClass.mk ↑⟨b, hb⟩
⊢ (ofLex a).orderTop.untop ⋯ < (ofLex b).orderTop.untop ⋯ ∨
    (ofLex a).orderTop = ↑((ofLex b).orderTop.untop ⋯) ∧
      ArchimedeanClass.mk (ofLex a).leadingCoeff ≤ ArchimedeanClass.mk (ofLex b).leadingCoeff

Tactic:
simpa using archimedeanClassMk_le_archimedeanClassMk_iff.mp h

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

Goal state before:
pp: case mpr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
⊢ (∃ i,
      (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j) ∧
        (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i) ∨
    embDomain f (ofLex a) = embDomain f (ofLex b)

pp: case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a : Lex R⟦Γ⟧
⊢ (∃ i,
      (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex a)).coeff j) ∧
        (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex a)).coeff i) ∨
    embDomain f (ofLex a) = embDomain f (ofLex a)

Tactic:
· refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩
        by_cases hkmem : k ∈ Set.range f
        · obtain ⟨j', rfl⟩ := hkmem
          simpa using hj _ <| f.lt_iff_lt.mp hki
        · simp_rw [embDomain_of_notMem_range hkmem]

Goal state after:
case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a : Lex R⟦Γ⟧
⊢ (∃ i,
      (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex a)).coeff j) ∧
        (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex a)).coeff i) ∨
    embDomain f (ofLex a) = embDomain f (ofLex a)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case mpr
Γ : 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✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
b : Γ
hr : ¬r = 0
hx : ¬((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
⊢ a1 = b ∧ a2 = a → a1 = b ∧ a2 ∈ ((of R).symm x).support ∧ a1 +ᵥ a2 = b +ᵥ a

Tactic:
rintro ⟨rfl, rfl⟩
      exact ⟨rfl, by exact hx, rfl⟩

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
⊢ ⊤ ≠ 0

Tactic:
simp [← mk_one]

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 : x ≠ 0
⊢ IsAddRegular (mk x)

Tactic:
rw [← isAddLeftRegular_iff_isAddRegular]

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ 0
⊢ IsAddLeftRegular (mk x)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y z : R⟦Γ⟧
⊢ (HahnModule.of R).symm (x • (HahnModule.of R) (y + z)) =
    (HahnModule.of R).symm (x • (HahnModule.of R) y) + (HahnModule.of R).symm (x • (HahnModule.of R) z)

Tactic:
exact HahnModule.smul_add x y z

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

Goal state before:
pp: case neg
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) = ∅
⊢ ↑(f.support.min' hsupport) < ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
simpa [hsupport'] using! (f.support.min' hsupport).2.lt_top

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

Goal state before:
pp: case inr.refine_2
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
nz : (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0
⊢ y.inv.leadingCoeff = 1

Tactic:
· simpa [this.2, y.val_inv] using (leadingCoeff_mul_of_ne_zero nz).symm

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Tactic:
rw [coeff_single_of_ne h, coeff_mul, sum_eq_zero]
    simp_rw [mem_antidiagonal]
    rintro ⟨y, z⟩ ⟨hy, hz, rfl⟩
    rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h
    exact (h rfl).elim

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ (posSubgroup R).index = 2

Tactic:
by
  rw [Subgroup.index_eq_two_iff]
  refine ⟨-1, fun a ↦ ?_⟩
  obtain h | h := lt_or_gt_of_ne a.ne_zero
  · simp [h, h.le]
  · simp [h, xor_comm, h.le]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ ⇑(R.mapOfLE S h) ∘ ⇑R.valuation = ⇑S.valuation

Tactic:
by ext; rfl

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

Goal state before:
pp: case mpr
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
⊢ v₁ x ≤ 1 ↔ v₂ x ≤ 1

Tactic:
have : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring := by rw [h]

Goal state after:
case mpr
K : Type u
inst✝² : Field K
Γ₁ : Type u_2
Γ₂ : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero Γ₁
inst✝ : LinearOrderedCommGroupWithZero Γ₂
v₁ : Valuation K Γ₁
v₂ : Valuation K Γ₂
h : v₁.valuationSubring = v₂.valuationSubring
x : K
this : x ∈ v₁.valuationSubring ↔ x ∈ v₂.valuationSubring
⊢ v₁ x ≤ 1 ↔ v₂ x ≤ 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A.unitGroup
⊢ { val := ⟨↑↑(a * b), ⋯⟩, inv := ⟨↑↑(a * b)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } =
    { val := ⟨↑↑a, ⋯⟩, inv := ⟨↑↑a⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } *
      { val := ⟨↑↑b, ⋯⟩, inv := ⟨↑↑b⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ }

Tactic:
by ext; rfl

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
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ f.eval x = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))

Tactic:
unfold eval
  rw [toLex.injective.eq_iff]
  ext d
  simp only
  obtain hd | hd := lt_or_ge d c
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hd]
    exact evalCoeff_eq _ fun _ ↦ by simpa [hy]
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hd]
    apply evalCoeff_eq_zero
    contrapose! h
    obtain ⟨z, hz⟩ := h
    exact ⟨z, (ball_strictAnti K).antitone (by simpa using hd) hz⟩

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✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : y ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {⟦x⟧}
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ z ∈ Quotient.mk (Submodule.quotientRel (IsLocalRing.maximalIdeal (FiniteElement K))) ⁻¹' {⟦x⟧}

Tactic:
rw [Set.mem_preimage, Set.mem_singleton_iff, Quotient.eq, Submodule.quotientRel_def,
    IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, FiniteElement.not_isUnit_iff_mk_pos] at hy ⊢

Goal state after:
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 - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ 0 < mk ↑(z - x)
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
inst✝ : Archimedean R
x : M
c : K
hc : c ≠ 0
hx : -c • x ∈ (↑f).domain
⊢ x ∈ (↑f).domain

Tactic:
neg_smul,

Goal state after:
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
c : K
hc : c ≠ 0
hx : -(c • x) ∈ (↑f).domain
⊢ x ∈ (↑f).domain
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s / t)

Tactic:
rw [div_eq_mul_inv]
  exact hs.mul_right

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Subgroup Gᵐᵒᵖ
a : G
h : ∀ (b : Gᵐᵒᵖ), a • b ∈ ↑s ↔ b ∈ ↑s
this : 1 * op a ∈ s
⊢ a ∈ s.unop

Tactic:
simpa only [op_smul_eq_mul, SetLike.mem_coe, one_mul] using! this

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
hx : mk x ≠ 0
⊢ mk x⁻¹ ≠ 0

Tactic:
rwa [mk_inv, neg_ne_zero]

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

Goal state before:
pp: case pos.inr
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
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : c ≤ d
⊢ ((truncLTLinearMap K c) (ofLex (↑↑f y))).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d

Tactic:
· simp_rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
by_cases hdp : P.natDegree = 0
  · rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢
    simp [coeffList_C (C_ne_zero.mp h)]
  by_cases hep : P.eraseLead = 0
  · have h₂ : .monomial P.natDegree P.leadingCoeff = P := by
      simpa [hep] using P.eraseLead_add_monomial_natDegree_leadingCoeff
    nth_rewrite 1 [← h₂]
    simp [coeffList_monomial (Polynomial.leadingCoeff_ne_zero.mpr h), hep]
  have h₁ := withBotSucc_degree_eq_natDegree_add_one h
  have h₂ := withBotSucc_degree_eq_natDegree_add_one hep
  obtain ⟨n, hn, hn2⟩ : ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧
      d = P.natDegree - P.eraseLead.degree.succ := by
    use P.natDegree - P.eraseLead.natDegree - 1
    have := eraseLead_natDegree_le P
    lia
  rw [← hn2]; clear hn2
  apply List.ext_getElem?
  rintro (_ | k)
  · obtain ⟨w, h⟩ := (coeffList_eq_cons_leadingCoeff h)
    simp_all
  simp only [coeffList, List.map_reverse]
  by_cases! hkd : P.natDegree + 1 ≤ k + 1
  · rw [List.getElem?_eq_none]
      <;> simp <;> lia
  obtain ⟨dk, hdk⟩ := exists_add_of_le (Nat.le_of_lt_succ hkd)
  rw [List.getElem?_reverse (by simpa [withBotSucc_degree_eq_natDegree_add_one h] using hkd),
    List.getElem?_cons_succ, List.length_map, List.length_range, List.getElem?_map,
    List.getElem?_range (by lia), Option.map_some]
  conv_lhs => arg 1; equals P.eraseLead.coeff dk =>
    rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]
    congr
    lia
  by_cases! hkn : k < n
  · simpa [List.getElem?_append, hkn] using coeff_eq_zero_of_natDegree_lt (by lia)
  · rw [List.getElem?_append_right (List.length_replicate ▸ hkn),
      List.length_replicate, List.getElem?_reverse, List.getElem?_map]
    · rw [List.length_map, List.length_range,
        List.getElem?_range (by lia), Option.map_some]
      congr 2
      lia
    · simp
      lia

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

Goal state before:
pp: case refine_1
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
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
a' : M
ha'mem : a' ∈ (↑f).domain
ha' : (↑f).toFun ⟨a', ha'mem⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))
⊢ ((↑f).supSpanSingleton x (f.eval x) hx).toFun ⟨a', ⋯⟩ = (↑f).toFun ⟨a', ha'mem⟩

Tactic:
exact LinearPMap.supSpanSingleton_apply_mk_of_mem f.val _ hx ha'mem

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
n : ℤ
⊢ evalEval x y ↑n = ↑n

Tactic:
by
  simp only [evalEval, eval_intCast]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
x✝ : IsMonicOfDegree 1 n
H : natDegree 1 = n
monic✝ : Monic 1
⊢ n = 0

pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
⊢ IsMonicOfDegree 1 n

Tactic:
· rwa [natDegree_one, eq_comm] at H

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
⊢ IsMonicOfDegree 1 n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
⊢ q.natDegree = n

Tactic:
have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [hp.leadingCoeff_eq, h₂.leadingCoeff, one_mul]
    exact one_ne_zero

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : q.Monic
this : (p * q).natDegree = m + n
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ q.natDegree = n
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i (r * a ^ n * b ^ (N - n)) = i b ^ N * eval (i a * bi) (Polynomial.map i (C r * X ^ n))

Tactic:
C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
⊢ i (r * a ^ n * b ^ (N - n)) = i b ^ N * eval (i a * bi) (Polynomial.map i ((monomial n) r))
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
| i b ^ (N - n + n - n) * (i r * (i a * 1) ^ n)

Tactic:
← bu

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
n : ℕ
r : R
nN : n ≤ N
| i b ^ (N - n + n - n) * (i r * (i a * (bi * i b)) ^ n)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (if R b c then b :: destutter' R c l else destutter' R b l).length ≤
    (if R a c then a :: destutter' R c l else destutter' R a l).length

Tactic:
if_pos (not_not.1 hac),

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (if R b c then b :: destutter' R c l else destutter' R b l).length ≤ (a :: destutter' R c l).length
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p

Tactic:
apply Polynomial.irreducible_of_degree_eq_one

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ p.degree = 1
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p : R[X]
⊢ (aeval x) p = p.smeval x

Tactic:
rw [aeval_def, eval₂_def, Algebra.algebraMap_eq_smul_one', smeval_def]
  simp only [Algebra.smul_mul_assoc, one_mul]
  exact rfl

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
⊢ (((if m = k then u else 0) + if m = m then v else 0) + if m = n then w else 0) = v

Tactic:
if_neg hkm.ne',

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ ((0 + if m = m then v else 0) + if m = n then w else 0) = v
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 + k) + C v * X ^ (n - m + k) + C w * X ^ (n - n + k) = trinomial k (n - m + k) n w v u

Tactic:
Nat.sub_add_cancel (hkm.trans hmn).le,

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 + C v * X ^ (n - m + k) + C w * X ^ (n - n + k) = trinomial k (n - m + k) n w v u