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

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

Tactic:
rw [Prod.Lex.le_iff]
      simp only [ofLex_toLex]
      rw [FiniteArchimedeanClass.mk_le_mk] at ⊢ h
      rw [WithTop.untop_eq_iff]
      simpa using archimedeanClassMk_le_archimedeanClassMk_iff.mp h

Goal state after:
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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
h : True
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support

Tactic:
have := u.archimedeanClassMk_of_mem_stratum ha h0

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : M
ha : a ∈ u.stratum c
b : M
hb : b ∈ ⨆ j, ⨆ (_ : j ≠ c), u.stratum j
hab : a = b
f : Π₀ (i : FiniteArchimedeanClass M), ↥(⨆ (_ : i ≠ c), u.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = b
h0 : a ≠ 0
hnonempty : f.support.Nonempty
hmem : ∀ (x : FiniteArchimedeanClass M), ↑(f x) ∈ u.stratum x
hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk ↑(f i)) ↑f.support
this✝ : f.support.min' hnonempty = FiniteArchimedeanClass.mk a h0
h : True
this : ArchimedeanClass.mk a = ↑c
⊢ FiniteArchimedeanClass.mk a h0 ∉ f.support
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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := DFinsupp.mapRange (fun c x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ⋯ f
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ seed.baseDomain.subtype x = seed.baseDomain.subtype (f.sum fun i b ↦ ↑⟨⟨↑b, ⋯⟩, ⋯⟩)

Tactic:
simp [h]

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

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

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

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of (x₂ * y₂))| =
    |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| * |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)|

Tactic:
simp_rw [ArchimedeanOrder.val_of, abs_mul]

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

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • |ArchimedeanOrder.val (ArchimedeanOrder.of (x₁ * y₁))| =
    m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)| * n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|

Tactic:
simp_rw [ArchimedeanOrder.val_of, abs_mul]

Goal state after:
case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • (|x₁| * |y₁|) = m • |x₁| * n • |y₁|
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)
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk ((f.sum fun x x_1 ↦ ↑x_1) - ↑(f (f.support.min' hsupport)))

Tactic:
hferase

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)
⊢ ArchimedeanClass.mk (f.sum fun x x_1 ↦ ↑x_1) <
    ArchimedeanClass.mk (∑ x ∈ f.support.erase (f.support.min' hsupport), ↑(f x))
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
⊢ mk (x ^ ↑n) = mk (y ^ ↑n)

Tactic:
simp [h]

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
⊢ mk (x ^ (-↑n)) = mk (y ^ (-↑n))

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LE α
x : Quotient s
⊢ x ≤ x

Tactic:
by
    induction x using Quotient.inductionOn with | h x
    exact .single <| .inr (refl x)

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 : P.supportAddSubgroup = ⊤
⊢ 1 ∈ P.supportAddSubgroup

Tactic:
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:
simp [h]

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

Goal state before:
pp: case pos
Γ : 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 : Γ
h : a = 0
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a

Tactic:
simp [h]

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

Goal state before:
pp: case neg
Γ : 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 : Γ
h : ¬a = 0
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a

Tactic:
simp [h]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

Tactic:
simp [h]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : ¬g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

Tactic:
simp [h]

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

Goal state before:
pp: case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
fst✝ snd✝ : Γ'
h1 : (fst✝, snd✝) ∈ antidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (fst✝, snd✝).1 * (embDomain f y).coeff (fst✝, snd✝).2 ≠ 0
⊢ (fst✝, snd✝) ∈ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g)

Tactic:
obtain ⟨i, _, rfl⟩ := support_embDomain_subset (ne_zero_and_ne_zero_of_mul h2).1

Goal state after:
case hf
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ
snd✝ : Γ'
i : Γ
left✝ : i ∈ x.support
h1 : (f i, snd✝) ∈ antidiagonal ⋯ ⋯ (f g)
h2 : (embDomain f x).coeff (f i, snd✝).1 * (embDomain f y).coeff (f i, snd✝).2 ≠ 0
⊢ (f i, snd✝) ∈ Finset.map (f.prodMap f.toEmbedding) (antidiagonal ⋯ ⋯ g)
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 : ↥(↑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
⊢ ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x

Tactic:
apply seed.archimedeanClassMk_of_mem_stratum hx'mem

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 : ↥(↑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
⊢ x' ≠ 0
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 < f

Tactic:
lt_iff_le_and_ne,

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 ∧ 0 ≠ conjneg f ↔ 0 ≤ f ∧ 0 ≠ f
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:
simp [h]

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

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h : ↑b = 0
⊢ ↑(a * 0) = ↑b

Tactic:
simp [h]

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

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ↑a = 0
⊢ ↑(b * 0) = ↑a

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ A.valuation ↑↑a = 1

Tactic:
← A.valuation.map_one,

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ A.valuation ↑↑a = A.valuation 1
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ A.valuation ↑↑a = A.valuation 1

Tactic:
valuation_eq_iff

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
a : (↥A)ˣ
⊢ ∃ a_1, ↑↑a_1 * 1 = ↑↑a
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1

Tactic:
let π := Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)

Goal state after:
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ ↑((Units.map ↑(IsLocalRing.residue ↥A)) (A.unitGroupMulEquiv x)) = ↑1
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteResidueField K
hy : 0 < y
⊢ ∃ n, x ≤ n • y

Tactic:
by
    induction x with | mk x
    induction y with | mk y
    obtain hx | hx := le_or_gt (mk x) 0
    · use 0
      rwa [zero_nsmul]
    · obtain ⟨n, hn⟩ := ((mk_ne_zero.1 hy.ne').trans (mk_ne_zero.1 hx.ne').symm).le
      refine ⟨n, mk.monotone' ?_⟩
      change x.1 ≤ n • y.1
      convert! ← hn
      · exact abs_of_pos <| lt_of_mk_lt_mk hx
      · exact abs_of_pos <| lt_of_mk_lt_mk hy

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

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
⊢ (have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧ (0, p).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
swap

Goal state after:
case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧ (0, p).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
⊢ (have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (have z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
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
⊢ ↑0 < ↑⟨↑(y - x), hf⟩

Tactic:
simp [h]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hp : p.IsMonicOfDegree m
hq : q.IsMonicOfDegree n
H : Subsingleton R
⊢ (p * q).IsMonicOfDegree (m + n)

Tactic:
simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hp hq ⊢
    exact ⟨hp, hq⟩

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:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

Tactic:
simp [h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

Tactic:
simp [h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

Tactic:
simp [h]

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

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : n < m
r : R
⊢ ((monomial m) r).homogenize n = 0

Tactic:
rw [homogenize]
  apply Finset.sum_eq_zero
  aesop (add simp coeff_monomial)

Goal state after:
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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ ↑(q + k)! * (aeval r) p' = ↑(q ! * (q + k).descFactorial k) * (aeval r) p'

Tactic:
Nat.add_descFactorial_eq_ascFactorial,

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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
r : A
⊢ ↑(q + k)! * (aeval r) p' = ↑(q ! * (q + 1).ascFactorial k) * (aeval r) p'