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

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
⊢ b < a

Tactic:
obtain h := hab 1

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
ha : a ∈ Set.Iic 1
b : M
hb : b ∈ Set.Iic 1
hab : ∀ (n : ℕ), |a|ₘ ^ n < |b|ₘ
h : |a|ₘ ^ 1 < |b|ₘ
⊢ b < a
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hgcd_ne_zero : x.gcd y ≠ 0
hlcm_ne_zero : x.lcm y ≠ 0
hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1
⊢ y.factorization.support ⊆ x.primeFactors ∪ y.primeFactors

Tactic:
apply subset_union_right

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

Goal state before:
pp: case e'_7
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ g = g ∘ ⇑σ⁻¹ ∘ ⇑σ

Tactic:
inv_def,

Goal state after:
case e'_7
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
hσinv : {x | σ⁻¹ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ⁻¹) ↑s
⊢ g = g ∘ ⇑(Equiv.symm σ) ∘ ⇑σ
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
⊢ s < t → subsemigroup t < subsemigroup s

Tactic:
hst

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s < t
⊢ subsemigroup t < subsemigroup s
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 ∈ Set.Iio ⊤
t : UpperSet (MulArchimedeanClass M)
ht : t ∈ Set.Iio ⊤
⊢ s < t → subgroup t < subgroup s

Tactic:
hst

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s : UpperSet (MulArchimedeanClass M)
hs : s ∈ Set.Iio ⊤
t : UpperSet (MulArchimedeanClass M)
ht : t ∈ Set.Iio ⊤
hst : s < t
⊢ subgroup t < subgroup s
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
⊢ s ≤ t → subgroup t ≤ subgroup s

Tactic:
hst

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
s t : UpperSet (MulArchimedeanClass M)
hst : s ≤ t
⊢ subgroup t ≤ subgroup s
Module: Mathlib.Algebra.Order.Hom.Lattice

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
i : ι
hi : x i ≠ 0
this : Nonempty { j // x j ≠ 0 }
⊢ ⨆ i, v (x i) = ⨆ i, v (x ↑i)

Tactic:
have : Nonempty ι := .intro i

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
F : Type u_4
inst✝⁶ : Finite ι
inst✝⁵ : Zero K
inst✝⁴ : Zero M
inst✝³ : ConditionallyCompleteLattice M
inst✝² : FunLike F K M
inst✝¹ : ZeroHomClass F K M
inst✝ : NonnegHomClass F K M
x : ι → K
hx : x ≠ 0
v : F
i : ι
hi : x i ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : Nonempty ι
⊢ ⨆ i, v (x i) = ⨆ i, v (x ↑i)
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
by
  simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici a

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 : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff g ≠ 0

Tactic:
rw [← hg]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff (⋯.min ⋯) ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : V⟦Γ⟧
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
by
  by_cases hrx : r • x = 0
  · rw [hrx, orderTop_zero]
    exact not_top_lt
  · simp only [orderTop_of_ne_zero hrx, orderTop_of_ne_zero <| right_ne_zero_of_smul hrx,
      WithTop.coe_lt_coe]
    exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ ↑g = min (↑g) y.orderTop

Tactic:
hyg,

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ ↑g = min ↑g ↑g
Module: Mathlib.Algebra.Order.Module.PositiveLinearMap

Goal state before:
pp: F' : Type u_5
E₁' : Type u_6
E₂' : Type u_7
inst✝⁷ : FunLike F' E₁' E₂'
inst✝⁶ : AddGroup E₁'
inst✝⁵ : LE E₁'
inst✝⁴ : AddRightMono E₁'
inst✝³ : AddGroup E₂'
inst✝² : LE E₂'
inst✝¹ : AddRightMono E₂'
inst✝ : AddMonoidHomClass F' E₁' E₂'
h : ∀ (f : F') (x : E₁'), 0 ≤ x → 0 ≤ f x
f : F'
a b : E₁'
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
by simpa using h f (b - a) (sub_nonneg.mpr hab)

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a ≤ a * d

Tactic:
simpa using h₁

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulRightMono M
a b : M
u : Mˣ
⊢ a * ↑u⁻¹ ≤ b ↔ a ≤ b * ↑u

Tactic:
rw [← u.mul_le_mul_iff_right, u.inv_mul_cancel_right]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
a : Γ'
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
h2 : a ∈ ((of R).symm x).support
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ False

Tactic:
exact h2 hx

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
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
hx : 0 < mk x
y : S
hy : 0 < y
⊢ x < f y

Tactic:
by
  apply lt_of_mk_lt_mk_of_nonneg
  · rwa [mk_map_of_archimedean' f hy.ne']
  · simpa using f.monotone' hy.le

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✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
hr : ¬r = 0
a1 : Γ
hx : x.coeff a1 = 0
a2 : Γ
h2 : a1 ∈ x.support
h1 : a1 + a2 = a + a2
⊢ False

Tactic:
exact h2 hx

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✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ (x * y).support ⊆ x.support + y.support

Tactic:
by
  rw [← of_symm_smul_of_eq_mul, ← vadd_eq_add]
  exact HahnModule.support_smul_subset_vadd_support

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

Goal state before:
pp: Γ : 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
⊢ (x * y).order = x.order + y.order

Tactic:
by
  have hx : x.leadingCoeff ≠ 0 := by aesop
  have hy : y.leadingCoeff ≠ 0 := by aesop
  have hxy : (x * y).coeff (x.order + y.order) ≠ 0 :=
    ne_of_eq_of_ne (coeff_mul_order_add_order x y) h
  refine le_antisymm (order_le_of_coeff_ne_zero
    (Eq.mpr (congrArg (fun _a ↦ _a ≠ 0) (coeff_mul_order_add_order x y)) h)) ?_
  rw [order_of_ne <| leadingCoeff_ne_zero.mp hx, order_of_ne <| leadingCoeff_ne_zero.mp hy,
    order_of_ne <| ne_zero_of_coeff_ne_zero hxy, ← Set.IsWF.min_add]
  exact Set.IsWF.min_le_min_of_subset support_mul_subset

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this✝ : ¬(a ∈ P ∨ b ∈ P)
this : a * b ∈ P
⊢ False

Tactic:
have : a ∈ P.support ∨ b ∈ P.support :=
      Ideal.IsPrime.mem_or_mem inferInstance (by simp_all [mem_support])

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x✝¹ : P.IsOrdering
a b : R
x✝ : -(a * b) ∈ P
this✝¹ : ¬(a ∈ P ∨ b ∈ P)
this✝ : a * b ∈ P
this : a ∈ P.support ∨ b ∈ P.support
⊢ False
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
r : R
⊢ (C r).order = 0

Tactic:
by
  by_cases h : r = 0
  · rw [h, C_zero, order_zero]
  · exact order_single h

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

Goal state before:
pp: case neg.inl
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z ∈ A
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

pp: case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1

Tactic:
· use (⟨z, hh⟩, 1); simp

Goal state after:
case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
z : K
h : ¬z = 0
hh : z⁻¹ ∈ A
⊢ ∃ x, z * (algebraMap (↥A) K) ↑x.2 = (algebraMap (↥A) K) x.1
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a - f b ≤ f (a - b)

Tactic:
tsub_le_iff_right,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a ≤ f (a - b) + f b
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)
⊢ 0 < ↑(f.extendFun hx) (z - y)

Tactic:
have : z - y = ⟨a + b, hab.symm ▸ (z - y).prop⟩ := by simp_rw [hab]

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
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)
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x✝ : G
⊢ x✝ ∈ ↑(stabilizer G s) * s ↔ x✝ ∈ s

Tactic:
refine ⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x✝ : G
⊢ x✝ ∈ ↑(stabilizer G s) * s → x✝ ∈ s
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s t : Set α
f : Set α → Set α → Set α
hf : ∀ (a : G), a • f s t = f (a • s) (a • t)
⊢ stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (f s t)

Tactic:
by aesop (add simp [SetLike.le_def])

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
⊢ stdPart 0 = 0

Tactic:
by
  rw [stdPart, dif_pos] <;> simp

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
⊢ stdPart 1 = 1

Tactic:
by
  rw [stdPart, dif_pos] <;> simp

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
hx : 0 ≤ mk x
hy : 0 ≤ mk y
⊢ stdPart (x - y) = stdPart x - stdPart y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, stdPart_add hx, stdPart_neg]
  rwa [mk_neg]

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
⊢ StrictMono ↑(f.extendFun hx)

Tactic:
by
  have hx' {c : K} (hc : c ≠ 0) : -c • x ∉ f.val.domain := by
    contrapose hx
    rwa [neg_smul, neg_mem_iff, Submodule.smul_mem_iff _ hc] at hx
  -- only need to prove `0 < f v` for `0 < v = z - y`
  intro y z hyz
  rw [← sub_pos] at hyz
  apply lt_of_sub_pos
  rw [← LinearPMap.map_sub]
  obtain hyzmem := (z - y).prop
  nth_rw 1 [extendFun, LinearPMap.domain_supSpanSingleton] at hyzmem
  -- decompose `v = a + c • x`, reducing this to eval_lt
  obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hyzmem
  have : z - y = ⟨a + b, hab.symm ▸ (z - y).prop⟩ := by simp_rw [hab]
  rw [this] at ⊢ hyz
  have habpos : 0 < a + b := by exact hyz
  obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hb
  rw [← hc] at habpos
  simp_rw [← hc, extendFun]
  rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ hx _ ha]
  suffices f.eval (-c • x) < f.val ⟨a, ha⟩ by
    rw [eval_smul, neg_smul] at this
    exact neg_lt_iff_pos_add.mp this
  have hac : -c • x < a := by
    rw [neg_smul]
    exact neg_lt_iff_pos_add.mpr habpos
  by_cases hc : c = 0
  · rw [hc] at ⊢ hac
    suffices f.val 0 < f.val ⟨a, ha⟩ by simpa using! this
    exact f.prop.strictMono (by simpa using! hac)
  · exact f.eval_lt (hx' hc) ⟨a, ha⟩ hac

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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
⊢ (if p * q = 0 then 0 else ↑(Fintype.card Fq) ^ (p * q).natDegree) =
    (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) * if q = 0 then 0 else ↑(Fintype.card Fq) ^ q.natDegree

Tactic:
by_cases hp : p = 0; · simp [hp]
      by_cases hq : q = 0; · simp [hq]
      have hpq : p * q ≠ 0 := mul_ne_zero hp hq
      simp only [hpq, hp, hq, if_false, Polynomial.natDegree_mul hp hq, pow_add]

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

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

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

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ span (Set.range (Function.update v j (v j %ₘ v i))) = span (Set.range v)

Tactic:
modByMonic_eq_sub_mul_div,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ span (Set.range (Function.update v j (v j - v i * (v j /ₘ v i)))) = span (Set.range v)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)

Tactic:
intro n hn hp

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

Tactic:
intro n hn hp

Goal state after:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ a,
    ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
      (revAt (p.natDegree + p.natTrailingDegree)) a = n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.trailingCoeff = p.leadingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.trailingCoeff = p.coeff p.natDegree
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).smeval x * x = p.smeval x * x ^ (n + 1)

Tactic:
smeval_mul_X_pow n,

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.smeval x * x ^ n * x = p.smeval x * x ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ sumIDeriv (derivative p) = derivative (sumIDeriv p)

Tactic:
rw [sumIDeriv_apply_of_le ((natDegree_derivative_le p).trans tsub_le_self), sumIDeriv_apply,
    derivative_sum]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ range (p.natDegree + 1), (⇑derivative)^[i] (derivative p) =
    ∑ b ∈ range (p.natDegree + 1), derivative ((⇑derivative)^[b] p)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (⇑derivative)^[0] p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + 0) =
    p + (∑ x ∈ range p.natDegree, (⇑derivative)^[x.succ] p + (⇑derivative)^[p.natDegree.succ] p)

Tactic:
Nat.succ_eq_add_one,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (⇑derivative)^[0] p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + 0) =
    p + (∑ k ∈ range p.natDegree, (⇑derivative)^[k + 1] p + (⇑derivative)^[p.natDegree + 1] p)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).leadingCoeff = w

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).coeff (trinomial k m n u v w).natDegree = w
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 : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
have h₂ : nextCoeff P ≠ 0 := by intro; simp_all
    obtain ⟨_, hl⟩ := coeffList_eq_cons_leadingCoeff (mt nextCoeff_eq_zero_of_eraseLead_eq_zero h₂)
    simp [signVariations, List.destutter, leadingCoeff_eraseLead_eq_nextCoeff h₂, hl, h, h₂,
      coeffList_eraseLead hpz]

Goal state after:
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 * P - C η * P - (monomial (P.natDegree + 1)) P.leadingCoeff -
      ((monomial P.natDegree) (P.coeff d) - (monomial P.natDegree) (η * P.coeff (d + 1))) =
    X * P - C η * P - ((monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) (η * P.leadingCoeff)) -
      (monomial P.natDegree) P.nextCoeff

Tactic:
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 * P - C η * P - (monomial (P.natDegree + 1)) (P.coeff P.natDegree) -
      ((monomial P.natDegree) (P.coeff d) - (monomial P.natDegree) (η * P.coeff (d + 1))) =
    X * P - C η * P -
        ((monomial (P.natDegree + 1)) (P.coeff P.natDegree) - (monomial P.natDegree) (η * P.coeff P.natDegree)) -
      (monomial P.natDegree) P.nextCoeff
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
⊢ star z ∈ (QuadraticAlgebra R a b)⁰ ↔ z ∈ (QuadraticAlgebra R a b)⁰

Tactic:
refine ⟨fun h ↦ ?_, star_mem_nonZeroDivisors⟩
  rw [← star_involutive z]
  exact star_mem_nonZeroDivisors h

Goal state after: