mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case hneg
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
ha : 1 < a
hab : mk a < mk (b / a)
⊢ a⁻¹ ≤ 1

Tactic:
· simpa using ha.le

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

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
⊢ Function.Injective ⇑(orderHom f)

Tactic:
intro a b

Goal state after:
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : MulArchimedeanClass M
⊢ (orderHom f) a = (orderHom f) b → a = b
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ≠ ⊤
⊢ ↑(subsemigroup s) = ↑(subgroup s)

Tactic:
simp [subgroup, hs]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
⊢ s ∈ Set.Iio ⊤ → ∀ ⦃b : UpperSet (MulArchimedeanClass M)⦄, b ∈ Set.Iio ⊤ → s < b → subgroup b < subgroup s

Tactic:
hs

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
⊢ ∀ ⦃b : UpperSet (MulArchimedeanClass M)⦄, b ∈ Set.Iio ⊤ → s < b → subgroup b < subgroup s
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋₊

Tactic:
by
  rw [div_eq_inv_mul]; refine mul_lt_floor ?_ ?_ ?_ <;> norm_num; assumption

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: R : Type u_3
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : n / d = res
⊢ IsNat ⌊r⌋₊ res

Tactic:
constructor
  rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
⊢ ↑(↑s ⊓ ↑t) = ↑↑s ∩ ↑↑t

Tactic:
simp only [coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc, inf_coe]
    split_ifs with h
    · simp only [coe_coe, NonemptyInterval.coe_def]
    · refine (Icc_eq_empty <| mt ?_ h).symm
      exact fun h ↦ ⟨le_sup_left.trans <| h.trans inf_le_right,
        le_sup_right.trans <| h.trans inf_le_left⟩

Goal state after:
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
f : (i : ι) → κ i → Interval α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
simp_rw [coe_iInf]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
hg : x.orderTop = ↑g
⊢ x.orderTop ≠ ⊤

Tactic:
simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]

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

Goal state before:
pp: case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
rw [h, orderTop_zero] at ho

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : ⊤ = x.orderTop
h : x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
⊢ (∃ i, (∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j) ∧ (ofLex 0).coeff i < (ofLex x).coeff i) →
    0 < (ofLex x).leadingCoeff

Tactic:
intro ⟨i, hj, hi⟩
    have horder : (ofLex x).orderTop = WithTop.some i := by
      apply orderTop_eq_of_le
      · simpa using hi.ne.symm
      · intro g hg
        contrapose! hg
        simpa using (hj g hg).symm
    have htop : (ofLex x).orderTop ≠ ⊤ := WithTop.ne_top_iff_exists.mpr ⟨i, horder.symm⟩
    have hne : ofLex x ≠ 0 := orderTop_ne_top.1 htop
    have horder' : (ofLex x).orderTop.untop htop = i := (WithTop.untop_eq_iff _).mpr horder
    rw [leadingCoeff_of_ne_zero hne, horder']
    simpa using hi

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
habs : ofLex |x| ≠ 0
⊢ ↑(ofLex |x|).order = ↑(ofLex x).order

Tactic:
rw [order_eq_orderTop_of_ne_zero habs, order_eq_orderTop_of_ne_zero hne']

Goal state after:
case inr
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
habs : ofLex |x| ≠ 0
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: 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✝
G : Type u_3
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : LocallyFiniteOrder Gˣ
a b : G
h : a ≤ b
⊢ (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun a ≤
    (↑((WithZero.map' ↑(orderMonoidHom Gˣ)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom)).toFun b

Tactic:
by have := (orderMonoidHom Gˣ).monotone'; aesop

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

Goal state before:
pp: case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

Tactic:
by_cases hy : (of R).symm y = 0

Goal state after:
case pos
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : (of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff

case neg
R : Type u_3
V : Type u_5
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Zero R
inst✝ : SMulWithZero R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hx : ¬x = 0
hy : ¬(of R).symm y = 0
⊢ ((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ (x * y).order

Tactic:
HahnSeries.order_of_ne hxy,

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ ⋯.min ⋯ + ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inr
Γ✝ : 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
⊢ 0 < (y.inv - 1).orderTop

Tactic:
refine y.inv.orderTop_self_sub_one_pos_iff.mpr ⟨?_, ?_⟩

Goal state after:
case inr.refine_1
Γ✝ : 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.orderTop = 0

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
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
⊢ ∀ {x y : α}, (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)

Tactic:
apply congrFun₂ <| @Relation.transGen_eq_self α _ ⟨fun x y z h₁ h₂ ↦ ?_⟩

Goal state after:
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ z ∨ y ≈ z
⊢ x ≤ z ∨ x ≈ z
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : 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 [h, coeff_mul_single_add]
    simp

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ z ∨ y ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
cases h₁ <;> cases h₂

Goal state after:
case inl.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≤ y
h✝ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≤ y
h✝ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≈ y
h✝ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

case inr.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≈ y
h✝ : y ≈ z
⊢ x ≤ z ∨ x ≈ z
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✝ : NonAssocSemiring R
x y : R
a : Γ
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a

Tactic:
by_cases h : a = 0 <;> simp [h]

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

Goal state before:
pp: K : Type u
inst✝¹ : Field K
A : ValuationSubring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ A.idealOfLE (A.ofPrime P) ⋯ = P

Tactic:
refine Ideal.ext (fun x => ?_)
  apply IsLocalization.AtPrime.to_map_mem_maximal_iff
  exact isLocalRing (ofPrime A P)

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : LowerSet α
⊢ ⋃ a ∈ Set.Iic 1, a • ↑s ⊆ ↑s

Tactic:
exact Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset

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
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : ↑(z - y) ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain
⊢ 0 < ↑(f.extendFun hx) (z - y)

Tactic:
LinearPMap.domain_supSpanSingleton

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
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyz : 0 < z - y
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
⊢ 0 < ↑(f.extendFun hx) (z - y)
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
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) ⟨y', hy'✝⟩))) ∈ (f.extendFun hx).toFun.range

Tactic:
LinearPMap.domain_supSpanSingleton

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
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
⊢ toLex ((truncLTLinearMap K c) (ofLex (↑(f.extendFun hx) ⟨y', hy'✝⟩))) ∈ (f.extendFun hx).toFun.range
Module: Mathlib.RingTheory.Derivation.MapCoeffs

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
x : A
⊢ d.mapCoeffs (C x) = PolynomialModule.single A 0 (d x)

Tactic:
simp [← monomial_zero_left]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
x : A
⊢ mapCoeffs (C x) = C x′

Tactic:
simp [← monomial_zero_left]

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

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

Tactic:
exact dvd_mul_right g h

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

Goal state before:
pp: case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
hab : R a b
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

Tactic:
simp_all [Nat.le_succ]

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

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

Tactic:
simp_all [Nat.le_succ]

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

Goal state before:
pp: case add
R : Type u_1
inst✝³ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x

Tactic:
| add p q ph qh =>

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

Goal state before:
pp: case add
R : Type u_1
inst✝³ : Semiring R
r : R
p✝ : R[X]
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Module R S
inst✝ : Pow S ℕ
x : S
p q : R[X]
ph : (C r * p).smeval x = r • p.smeval x
qh : (C r * q).smeval x = r • q.smeval x
⊢ (C r * (p + q)).smeval x = r • (p + q).smeval x

Tactic:
| add p q ph qh =>

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

Goal state before:
pp: case add
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
p q : ℕ[X]
ph : ∀ (n : ℕ), p.smeval ↑n = ↑(p.smeval n)
qh : ∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)
⊢ ∀ (n : ℕ), (p + q).smeval ↑n = ↑((p + q).smeval n)

Tactic:
| add p q ph qh =>

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

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

Tactic:
| add p q ph qh =>

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁵ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
p q : R[X]
ph : (X * p).smeval x = x * p.smeval x
qh : (X * q).smeval x = x * q.smeval x
⊢ (X * (p + q)).smeval x = x * (p + q).smeval x

Tactic:
| add p q ph qh =>

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁵ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
m n : ℕ
p q : R[X]
ph : x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
qh : x ^ m * x ^ n * q.smeval x = x ^ m * (x ^ n * q.smeval x)
⊢ x ^ m * x ^ n * (p + q).smeval x = x ^ m * (x ^ n * (p + q).smeval x)

Tactic:
| add p q ph qh =>

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

Goal state before:
pp: case add
R : Type u_1
inst✝⁵ : Semiring R
r✝ : R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : SMulCommClass R S S
n : ℕ
r s : R[X]
hr : ((monomial n) r✝ * r).smeval x = r✝ • (x ^ n * r.smeval x)
hs : ((monomial n) r✝ * s).smeval x = r✝ • (x ^ n * s.smeval x)
⊢ ((monomial n) r✝ * (r + s)).smeval x = r✝ • (x ^ n * (r.smeval x + s.smeval x))

Tactic:
rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]

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

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

Tactic:
| add p q ph qh =>

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

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

Tactic:
| add p q ph qh =>

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

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

Tactic:
smeval_mul_X,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ (p * X ^ n).smeval x * x = p.smeval x * x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.SpecificDegree

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

Tactic:
by_cases hdeg2 : 2 ≤ p.natDegree

Goal state after:
case pos
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

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
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑1 + (↑1 + ↑1) = 3

Tactic:
Units.val_one

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ 1 + (1 + 1) = 3
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:
rw [leadingCoeff_eraseLead_eq_nextCoeff hc.ne, ← self_sub_monomial_natDegree_leadingCoeff]

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 - (monomial P.natDegree) P.leadingCoeff) - (monomial P.natDegree) P.nextCoeff