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

Goal state before:
pp: case inr.left
Γ✝ : 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
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ (↑x).orderTop + (↑y).orderTop = 0

Tactic:
hx.1,

Goal state after:
case inr.left
Γ✝ : 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
x y : R⟦Γ⟧ˣ
hx : (↑x).orderTop = 0 ∧ (↑x).leadingCoeff = 1
hy : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
h✝ : Nontrivial R
h1 : (↑x).leadingCoeff * (↑y).leadingCoeff = 1
⊢ 0 + (↑y).orderTop = 0
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
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩)).coeff d =
    ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d

Tactic:
seed.coeff_baseEmbedding rfl

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
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (seed.coeff d) (f' d) = ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : P.supportAddSubgroup = ⊤
⊢ 1 ∈ P.supportAddSubgroup

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
⊢ ∀ (a : R), a ∈ P ∨ -a ∈ P

Tactic:
by simp [h]

Goal state after:
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
⊢ (single 0) (x + y) = (single 0) x + (single 0) y

Tactic:
ext a

Goal state after:
Γ : 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
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
x y : ↥(↑f).domain
⊢ ArchimedeanClass.mk x = ArchimedeanClass.mk y ↔ ArchimedeanClass.mk ↑x = ArchimedeanClass.mk ↑y

Tactic:
· simp_rw [mk_eq_mk]
    aesop

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ¬x = 0
hx0' : ↑x ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
hx'0 : ⟨x', hx'mem⟩ ≠ 0
heq : ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Tactic:
let x'' : f.val.domain := ⟨x', mem_domain f hx'mem⟩

Goal state after:
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ¬x = 0
hx0' : ↑x ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
hx'0 : ⟨x', hx'mem⟩ ≠ 0
heq : ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x
x'' : ↥(↑f).domain := ⟨x', ⋯⟩
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.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✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
x✝ y✝ x y : R⟦Γ⟧
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ¬(x * y).coeff (x.order + y.order) = coeff 0 (x.order + y.order)

Tactic:
by simpa [coeff_mul_order_add_order]

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

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

Tactic:
rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]

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

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ 0 ≤ conjneg f ∧ 0 ≠ conjneg f ↔ 0 ≤ f ∧ 0 ≠ f

Tactic:
ne_comm,

Goal state after:
G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ 0 ≤ conjneg f ∧ conjneg f ≠ 0 ↔ 0 ≤ f ∧ f ≠ 0
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
⊢ (∃ p, (∀ (i : ι), p i ∈ closure (Set.range fun s ↦ star s * s)) ∧ xy = xa + p) →
    ∀ (i : ι), ∃ p ∈ closure (Set.range fun s ↦ star s * s), xy i = xa i + p

Tactic:
simp only [forall_exists_index, and_imp]

Goal state after:
case refine_2
ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa xy : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
⊢ ∀ (x : (i : ι) → A i),
    (∀ (i : ι), x i ∈ closure (Set.range fun s ↦ star s * s)) →
      xy = xa + x → ∀ (i : ι), ∃ p ∈ closure (Set.range fun s ↦ star s * s), xy i = xa i + p
Module: Mathlib.Algebra.Order.Star.Pi

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Finite ι
A : ι → Type u_2
inst✝³ : (i : ι) → PartialOrder (A i)
inst✝² : (i : ι) → NonUnitalSemiring (A i)
inst✝¹ : (i : ι) → StarRing (A i)
inst✝ : ∀ (i : ι), StarOrderedRing (A i)
xa : (i : ι) → A i
this : closure (Set.range fun s ↦ star s * s) = pi Set.univ fun i ↦ closure (Set.range fun s ↦ star s * s)
x : (i : ι) → A i
h : ∀ (i : ι), x i ∈ closure (Set.range fun s ↦ star s * s)
i : ι
⊢ x i ∈ closure (Set.range fun s ↦ star s * s) ∧ (xa + x) i = xa i + x i

Tactic:
by simp [h]

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
y : ↥(↑f).domain
this : ↑y ≠ x
⊢ f.eval x ≠ ↑↑f y

Tactic:
ne_comm,

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
y : ↥(↑f).domain
this : x ≠ ↑y
⊢ f.eval x ≠ ↑↑f y
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
c : ↑a = 0
⊢ False

Tactic:
rw [c, A.valuation.map_zero] at h

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : 0 = 1
c : ↑a = 0
⊢ False
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case neg.refine_1
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x : K
hx : x ∈ S
this : x ≠ 0
hr : x⁻¹ ∈ R
⊢ ⟨x⁻¹, hr⟩ ∈ (R.idealOfLE S h).primeCompl

Tactic:
simp only [Ideal.primeCompl, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff,
        SetLike.mem_coe, idealOfLE, Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
        not_not]
      change IsUnit (⟨x⁻¹, h hr⟩ : S)
      refine .of_mul_eq_one (⟨x, hx⟩ : S) ?_
      ext
      simp [field]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Hom

Goal state before:
pp: R : Type u_3
inst✝⁴ : NonUnitalCommSemiring R
inst✝³ : Preorder R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : MulLeftMono R
a b c : R
⊢ a * c - b * c ≤ (a - b) * c

Tactic:
by
  simpa only [mul_comm _ c] using le_mul_tsub

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
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
⊢ ∃ z, ↑z - x ∈ ball K c

Tactic:
have hc : ArchimedeanClass.mk (y.val - x) = c := rfl

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
y : ↥(↑f).domain
c : FiniteArchimedeanClass M := FiniteArchimedeanClass.mk (↑y - x) ⋯
hc : ArchimedeanClass.mk (↑y - x) = ↑c
⊢ ∃ z, ↑z - x ∈ ball K c
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
⊢ Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥A) = ↑A.nonunits

Tactic:
ext a

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : K
⊢ a ∈ Subtype.val '' ↑(IsLocalRing.maximalIdeal ↥A) ↔ a ∈ ↑A.nonunits
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 α
hdisj : Disjoint s t
hstab : stabilizer G s ≤ stabilizer G t
hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t
⊢ stabilizer G ((s ∪ t) \ t) = stabilizer G s

Tactic:
union_sdiff_cancel_right

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

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
⊢ s ∩ t ⊆ ∅
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
q : ℚ
⊢ mk ↑q = ↑q

Tactic:
change mk (FiniteElement.mk ..) = _

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
q : ℚ
⊢ mk (FiniteElement.mk ↑q ⋯) = ↑q
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
s : Set G
⊢ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) = ⊥

Tactic:
ext a

Goal state after:
G : Type u_1
inst✝ : CommGroup G
s : Set G
a : G ⧸ stabilizer G s
⊢ a ∈ stabilizer (G ⧸ stabilizer G s) (QuotientGroup.mk '' s) ↔ a ∈ ⊥
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
n : ℕ
x : A
a✝ : ℕ
⊢ (d.mapCoeffs ((monomial n) x)).coeff a✝ = (PolynomialModule.single A n (d x)).coeff a✝

Tactic:
simp [coeff_monomial, apply_ite d, Finsupp.single_apply]

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
hmono : StrictMono ↑f
⊢ ↑f 0 < ↑f ⟨↑(y - x), hf⟩

Tactic:
apply hmono

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
hmono : StrictMono ↑f
⊢ 0 < ⟨↑(y - x), hf⟩
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
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = 1

Tactic:
rw [coeff_comp_degree_mul_degree (hq.natDegree_eq ▸ hn), hp.leadingCoeff_eq, hq.leadingCoeff_eq,
    one_pow, one_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
hp : p ∈ nonZeroDivisors R[X]
x : AEval R M a
⊢ (of R M a).symm (⟨p, hp⟩ • x) = (of R M a).symm 0

Tactic:
by simp [h]

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

Goal state before:
pp: case isUnit_or_isUnit
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
⊢ ∀ ⦃a b : R[X]⦄, f = a * b → IsUnit a ∨ IsUnit b

Tactic:
intro g h fgh

Goal state after:
case isUnit_or_isUnit
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
⊢ IsUnit g ∨ IsUnit h
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✝ : SMulCommClass R S S
n : ℕ
⊢ x * (x ^ n * p.smeval x) = x ^ 1 * x ^ n * p.smeval x

Tactic:
smeval_X_pow_assoc,

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✝ : SMulCommClass R S S
n : ℕ
⊢ x * (x ^ n * p.smeval x) = x ^ 1 * (x ^ n * p.smeval x)
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r (X - C r) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) • (X - C r) ^ (q - (k - i) - 1) * (⇑derivative)^[i] p') =
    0

Tactic:
eval_sub,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ (eval r X - eval r (C r)) *
      eval r
        (∑ i ∈ range k.succ,
          (k.choose i * q.descFactorial (k - i)) • (X - C r) ^ (q - (k - i) - 1) * (⇑derivative)^[i] p') =
    0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
hp : p.IsUnitTrinomial
k : ℕ
hk : k ∈ p.support
⊢ IsUnit (p.coeff k)

Tactic:
by
  obtain ⟨k, m, n, hkm, hmn, u, v, w, rfl⟩ := hp
  have := support_trinomial_subset k m n (u : ℤ) v w hk
  rw [mem_insert, mem_insert, mem_singleton] at this
  rcases this with (rfl | rfl | rfl)
  · refine ⟨u, by rw [trinomial_trailing_coeff' hkm hmn]⟩
  · refine ⟨v, by rw [trinomial_middle_coeff hkm hmn]⟩
  · refine ⟨w, by rw [trinomial_leading_coeff' hkm hmn]⟩

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

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
if_neg hmn.ne

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit (x * 0 + y + z * 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        (eval r (X - C r) * eval r ((X - C r) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative)^[x + 1] p') =
    0

Tactic:
eval_sub,

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) •
        ((eval r X - eval r (C r)) * eval r ((X - C r) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative)^[x + 1] p') =
    0
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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
obtain ⟨d, hd⟩ := Nat.exists_eq_add_one.mpr (natDegree_pos_of_nextCoeff_ne_zero hc.ne)

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
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations
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
this : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
⊢ ((X - C η) * P).eraseLead.signVariations = ((X - C η) * P.eraseLead).signVariations

Tactic:
by
    suffices (coeffList (eraseLead ((X - C η) * P))).map SignType.sign =
      (coeffList ((X - C η) * P.eraseLead)).map SignType.sign by
        rw [signVariations, signVariations, this]
    have : 0 < natDegree ((X - C η) * P.eraseLead) := by lia
    grind [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, leadingCoeff_eraseLead_eq_nextCoeff,
      LT.lt.ne, sign_neg, coeffList_eraseLead, ne_zero_of_natDegree_gt,
      nextCoeff_eq_zero_of_eraseLead_eq_zero]

Goal state after: