mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)

Tactic:
· rw [Ico_eq_empty, sum_empty]
    · apply div_nonneg (pow_nonneg hx _)
      simpa using h'x.le
    · simpa using hmn.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
a✝ b a : M
ha : a ≠ 1
⊢ a⁻¹ ≠ 1

Tactic:
by simp [ha]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
obtain ha | ha := le_or_gt a 0

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : a ≤ 0
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

case inr
α : Type u_2
β : Type u_3
inst✝⁷ : AddCommMonoid α
inst✝⁶ : LinearOrder α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a
Module: Mathlib.Algebra.Order.Group.DenselyOrdered

Goal state before:
pp: M : Type u_2
inst✝⁴ : LinearOrder M
inst✝³ : DenselyOrdered M
x : M
inst✝² : CommMonoid M
inst✝¹ : ExistsMulOfLE M
inst✝ : IsOrderedCancelMonoid M
hx : 1 < x
⊢ ∃ y, 1 < y ∧ y ^ 2 ≤ x

Tactic:
by
  obtain ⟨y, hy, hyx⟩ := exists_between hx
  obtain hyx | hxy := le_total (y ^ 2) x
  · exact ⟨y, hy, hyx⟩
  obtain ⟨z, hz, rfl⟩ := exists_one_lt_mul_of_lt' hyx
  exact ⟨z, hz, by simpa [pow_succ] using hxy⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: case mp
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
I : SemigroupIdeal M
hpwo : {x | x ∈ I}.IsPWO
z : M
hz' : Minimal (fun x ↦ x ∈ {x | x ∈ I}) z
y : M
hx : y * z ∈ I
⊢ ∃ y_1 z_1, Minimal (fun x ↦ x ∈ I) z_1 ∧ y_1 * z_1 = y * z

Tactic:
exact ⟨y, z, hz', rfl⟩

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|
⊢ mk (k • a) = mk a

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)

Goal state after:
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
⊢ mk (k • a) = mk a
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : NonemptyInterval α
⊢ (∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1

Tactic:
· rintro ⟨b, c, rfl, rfl, h⟩
    rw [pure_mul_pure, h, pure_one]

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

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
      Interval.coe_inj, NonemptyInterval.coe_eq_pure]

Goal state after:
case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ a✝¹ * a✝ = 1 ↔ ∃ a b, a✝¹ = NonemptyInterval.pure a ∧ a✝ = NonemptyInterval.pure b ∧ a * b = 1
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 '' {g}

Tactic:
Set.image_singleton,

Goal state after:
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 g}
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
by_cases hxy : x + y = 0

Goal state after:
case pos
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

case neg
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: 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
h : x.order = y.order
hyne : (single y.order) (y.coeff y.order) ≠ 0
⊢ False

Tactic:
← h,

Goal state after:
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
h : x.order = y.order
hyne : (single x.order) (y.coeff x.order) ≠ 0
⊢ False
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⟩

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ 0 < (ofLex x).leadingCoeff
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 : Lex R⟦Γ⟧
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop

Tactic:
obtain hle | hge := le_total x 0
  · rw [abs_eq_neg_self.mpr hle, ofLex_neg, orderTop_neg]
  · rw [abs_eq_self.mpr hge]

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

Goal state before:
pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hgt : 0 < x
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

Tactic:
· obtain hgt' := leadingCoeff_pos_iff.mpr hgt
    rw [abs_eq_self.mpr hgt.le, abs_eq_self.mpr hgt'.le]

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
Γ' : 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
⊢ ↑(⋯.min ⋯) +ᵥ ↑(⋯.min ⋯) ≤ ((of R).symm (x • y)).orderTop

Tactic:
← h,

Goal state after:
case neg
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
⊢ ↑(⋯.min ⋯ +ᵥ ⋯.min ⋯) ≤ ((of R).symm (x • y)).orderTop
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2
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
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))

Tactic:
rw [DFinsupp.sum, ArchimedeanClass.mk_sum hsupport hmono]

Goal state after:
case refine_2
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
⊢ ArchimedeanClass.mk ↑(f (f.support.min' hsupport)) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))
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
⊢ (x * y).orderTop = ↑x.order + y.orderTop

Tactic:
← order_eq_orderTop_of_ne_zero hy,

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
⊢ (x * y).orderTop = ↑x.order + ↑y.order
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c

Tactic:
have heq : (k • y).val - k • x = k • (y.val - x) := by simp [smul_sub]

Goal state after:
case pos
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
k : K
x : M
hk : ¬k = 0
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
heq : ↑(k • y) - k • x = k • (↑y - x)
⊢ f.evalCoeff (k • x) c = k • f.evalCoeff x c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.inl
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : ↑a / ↑b ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a

pp: case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : (↑a / ↑b)⁻¹ ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· use ⟨a / b, hh⟩
      right
      ext
      simp [field]

Goal state after:
case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : (↑a / ↑b)⁻¹ ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a
Module: Mathlib.Algebra.Order.Star.Real

Goal state before:
pp: case refine_1
x y : ℝ≥0
h : x ≤ y
⊢ ∃ s, y = x + star s * s

Tactic:
obtain ⟨d, rfl⟩ := exists_add_of_le h
    refine ⟨sqrt d, ?_⟩
    simp only [star_trivial, mul_self_sqrt]

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
d : FiniteArchimedeanClass M
hd : c ≤ d
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K d
⊢ c ≤ d

Tactic:
by simpa using hd

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup ↔ A ≤ B

Tactic:
constructor
  · intro h x hx
    rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    by_cases h_2 : 1 + x = 0
    · simp only [← add_eq_zero_iff_neg_eq.1 h_2, neg_mem _ _ (one_mem _)]
    rcases hx with hx | hx
    · have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)
      simpa using
        B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
          (B.neg_mem _ B.one_mem)
    · have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)
      exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)
  · rintro h x (hx : A.valuation x = 1)
    apply_fun A.mapOfLE B h at hx
    simpa using hx

Goal state after:
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : PartialOrder α
a b : WithTop α
hb : b ≠ ⊤
h : a ≤ b
⊢ a.untop₀ ≤ b.untop₀

Tactic:
lift b to α using hb
  by_cases ha : a = ⊤
  · simp_all
  lift a to α using ha
  simp_all

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).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
this : z - y = ⟨a + b, ⋯⟩
⊢ 0 < ↑(f.extendFun hx) (z - y)

Tactic:
rw [this] at ⊢ hyz

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
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
⊢ 0 < ↑(f.extendFun hx) ⟨a + b, ⋯⟩
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G s ≤ stabilizer G (s ∪ t)

Tactic:
· calc
      stabilizer G s
        ≤ stabilizer G s ⊓ stabilizer G t := by simpa
      _ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝ : k + 1 < ((monomial n) x).coeffList.length
h₁ : k + 1 < (x :: List.replicate n 0).length
⊢ ((monomial n) x).coeffList.get ⟨k + 1, h₁✝⟩ = (x :: List.replicate n 0).get ⟨k + 1, h₁⟩

Tactic:
· rw [List.length_cons, List.length_replicate] at h₁
    have : ((monomial n) x).natDegree.succ = n + 1 := by
      simp [Polynomial.natDegree_monomial_eq n hx]
    simpa [coeffList, withBotSucc_degree_eq_natDegree_add_one h]
      using Polynomial.coeff_monomial_of_ne _ (by lia)

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
⊢ mapCoeffs X = 0

Tactic:
simp [← monomial_one_one_eq_X]

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

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
⊢ swap (C (C a)) * C X ^ n = C (C a * X ^ n)

Tactic:
C_mul,

Goal state after:
case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
⊢ swap (C (C a)) * C X ^ n = C (C a) * C (X ^ n)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (MvPolynomial.pderiv 1) ((equivMvPolynomial R) ((monomial n) p)) = (equivMvPolynomial R) (derivative ((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 [derivative_pow]

Goal state after:
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 : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
⊢ p.IsMonicOfDegree m

Tactic:
have h₂ : p.Monic := hq.monic.of_mul_monic_right hpq.monic

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
H : Nontrivial R
h₂ : p.Monic
⊢ p.IsMonicOfDegree m
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 : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ 1 * 1 ^ p.natDegree = 1

Tactic:
one_pow,

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
h : Nontrivial R
⊢ 1 * 1 = 1
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
q : R[X]
hq₁ : p = X ^ n + q
hq₂ : q.natDegree < n
⊢ (p - X ^ n).natDegree < n

Tactic:
simpa [hq₁]

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

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

Tactic:
rw [← sub_sub_sub_cancel_right p q (X ^ n)]
  replace hp := hp.natDegree_sub_X_pow hn
  replace hq := hq.natDegree_sub_X_pow hn
  rw [← Nat.le_sub_one_iff_lt (Nat.zero_lt_of_ne_zero hn)] at hp hq ⊢
  exact (natDegree_sub_le_iff_left hq).mpr hp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a - r
⊢ ∃ q, q.IsMonicOfDegree (m - n) ∧ a = q * b + r

Tactic:
convert ha.of_dvd_add hmn hb ?_ h with q
  · rw [sub_neg_eq_add]
  · rwa [natDegree_neg]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = (a * b).leadingCoeff
⊢ IsUnit a ∨ IsUnit b

Tactic:
← h,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = f.leadingCoeff
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : ¬p.natDegree < n
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
not_lt

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ Finset.range (p.mirror.natDegree + 1), p.mirror.coeff i * 1 ^ i =
    ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * 1 ^ i

Tactic:
one_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ x ∈ Finset.range (p.mirror.natDegree + 1), p.mirror.coeff x * 1 =
    ∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x * 1
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n i : ℕ
v : Fin n → R
hi : n ≤ i
⊢ ((ofFn n) v).coeff i = 0

Tactic:
by
  simp [ofFn, Nat.not_lt_of_ge hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
⊢ p.coeff i = 0

Tactic:
rcases le_or_gt i p.natDegree with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = 0

case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R a b
⊢ destutter' R a [b] = [a, b]

Tactic:
simp! [h]

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

Goal state before:
pp: case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R a b
⊢ destutter' R a [b] = [a]

Tactic:
simp! [h]

Goal state after: