mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f) -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0

Tactic:
← tsub_add_cancel_of_le le_sup_left,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g - m.degree f + m.degree f)
        ((monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f) -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0
Module: Mathlib.Algebra.Order.Antidiag.Tendsto

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
U : Set R
⊢ U ∈ F → U ∈ Filter.map (fun a ↦ (antidiagonal a).sup' ⋯ f) cofinite

Tactic:
hU

Goal state after:
M : Type u_1
R : Type u_2
inst✝² : AddMonoid M
inst✝¹ : HasAntidiagonal M
f : M × M → R
inst✝ : LinearOrder R
F : Filter R
hf : Tendsto f cofinite F
U : Set R
hU : U ∈ F
⊢ U ∈ Filter.map (fun a ↦ (antidiagonal a).sup' ⋯ f) cofinite
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
⊢ d.primeFactorsPiBij n f hf = d.primeFactorsPiBij n g hg → f = g

Tactic:
by
  contrapose!
  simp_rw [Function.ne_iff]
  intro ⟨p, hp, hfg⟩
  use f p hp
  dsimp only [Nat.primeFactorsPiBij]
  apply ne_of_mem_of_not_mem (s := {x | p ∣ x}) <;> simp_rw [Set.mem_ofPred_eq]
  · rw [Finset.prod_filter]
    convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)
    rw [if_pos rfl]
  · rw [mem_primeFactors] at hp
    rw [Prime.dvd_finsetProd_iff hp.1.prime]
    push Not
    intro q hq
    rw [Nat.prime_dvd_prime_iff_eq hp.1 (Nat.prime_of_mem_primeFactorsList
      <| List.mem_toFinset.mp q.2)]
    rintro rfl
    rw [(mem_filter.mp hq).2] at hfg
    exact hfg rfl

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2

Tactic:
rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_inj.fst.snd
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
a1 a2 b1 b2 : ℕ
ha : ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0
cop : (((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2).Coprime (((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2)
hb : ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
c1 c2 d1 d2 : ℕ
hcd :
  (((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).1.2 = ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ∧
      ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).1.2 ≠ 0) ∧
    ((c1, c2), d1, d2).2.1 * ((c1, c2), d1, d2).2.2 = ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ∧
      ((a1, a2), b1, b2).2.1 * ((a1, a2), b1, b2).2.2 ≠ 0
h :
  ((a1, a2), b1, b2).1.1 * ((a1, a2), b1, b2).2.1 = ((c1, c2), d1, d2).1.1 * ((c1, c2), d1, d2).2.1 ∧
    ((a1, a2), b1, b2).1.2 * ((a1, a2), b1, b2).2.2 = ((c1, c2), d1, d2).1.2 * ((c1, c2), d1, d2).2.2
⊢ ((a1, a2), b1, b2).1.2 = ((c1, c2), d1, d2).1.2

Tactic:
trans gcd (a1 * a2) (a2 * b2)
      · rw [mul_comm, gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one,
          mul_one]
      · rw [← hcd.1.1, ← hcd.2.1] at cop
        rw [← hcd.1.1, h.2, mul_comm, gcd_mul_left,
          cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]

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

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

Tactic:
refine Set.ssubset_iff_subset_ne.mpr ⟨fun _ h ↦ hst.le h, ?_⟩

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.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ s ≤ { fst := t.toProd.1 ⊔ c.toProd.1, snd := t.toProd.2 ⊓ c.toProd.2, fst_le_snd := ⋯ }

pp: case hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2

Tactic:
· exact ⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩

Goal state after:
case hc
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s✝ t✝ c✝ : Interval α
s t c : NonemptyInterval α
hb : s ≤ t
hc : s ≤ c
⊢ t.toProd.1 ≤ c.toProd.2 ∧ c.toProd.1 ≤ t.toProd.2
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
⊢ x.orderTop < ⊤ ↔ x ≠ 0

Tactic:
simp [lt_top_iff_ne_top]

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Tactic:
exact Set.IsWF.not_lt_min _ _ hi

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Tactic:
exact Set.IsWF.not_lt_min _ _ hi

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a

Tactic:
· rw [dif_pos (Set.mem_image_of_mem f ha)]
    exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
⊢ (if h : f a ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0) = x.coeff a
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
⊢ (x - y).orderTop = x.orderTop

Tactic:
rw [sub_eq_add_neg]
  rw [← orderTop_neg (x := y)] at hxy
  exact orderTop_add_eq_left hxy

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S✝ : Type u_4
U : Type u_5
V✝ : Type u_6
α : Type u_7
inst✝⁶ : PartialOrder Γ
V : Type u_8
inst✝⁵ : Monoid R
inst✝⁴ : AddMonoid V
inst✝³ : DistribMulAction R V
S : Type u_9
inst✝² : Monoid S
inst✝¹ : DistribMulAction S V
inst✝ : SMulCommClass R S V
r : R
s : S
a : V⟦Γ⟧
x✝ : Γ
⊢ (r • s • a).coeff x✝ = (s • r • a).coeff x✝

Tactic:
simp [smul_comm]

Goal state after:
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|).support = (ofLex x).support

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

Goal state after:
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 y : Lex R⟦Γ⟧
h : (ofLex y).orderTop < (ofLex x).orderTop
⊢ |x| < |y|

Tactic:
← orderTop_abs x,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex y).orderTop < (ofLex |x|).orderTop
⊢ |x| < |y|
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this✝ : 0 ≤ ↑b
this : Ico 0 ↑b = {0}
⊢ (orderAddMonoidHom G).toAddMonoidHom ↑b = 1

Tactic:
by simpa [orderAddMonoidHom, addMonoidHom, this]

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

Goal state before:
pp: case inr.mpr.refine_1
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ ∀ j < (ofLex x).orderTop.untop ⋯, (ofLex |y|).coeff j = (ofLex ((n + 1) • |x|)).coeff j

pp: case inr.mpr.refine_2
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (ofLex ((n + 1) • |x|)).coeff ((ofLex x).orderTop.untop ⋯)

Tactic:
· -- all coefficients before the leading coefficient are zero
      intro j hj
      trans 0
      · apply coeff_eq_zero_of_lt_orderTop
        simpa [← h] using hj
      · suffices (ofLex |x|).coeff j = 0 by simp [this]
        apply coeff_eq_zero_of_lt_orderTop
        simpa using hj

Goal state after:
case inr.mpr.refine_2
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x y : Lex R⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
h' : (ofLex |x|).orderTop = (ofLex |y|).orderTop
n : ℕ
hn : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (ofLex ((n + 1) • |x|)).coeff ((ofLex x).orderTop.untop ⋯)
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case pos
Γ : 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 : Γ
hj : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hi : (ofLex a).coeff i < (ofLex b).coeff i
j' : Γ
hki : f j' < f i
⊢ (embDomain f (ofLex a)).coeff (f j') = (embDomain f (ofLex b)).coeff (f j')

Tactic:
simpa using hj _ <| f.lt_iff_lt.mp hki

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : ArchimedeanClass R
⊢ x + y = y + x

Tactic:
induction x with | mk x
    induction y with | mk y
    rw [← mk_mul, mul_comm, mk_mul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : ArchimedeanClass R
h : x ≤ y
z : ArchimedeanClass R
⊢ x + z ≤ y + z

Tactic:
by
    induction x with | mk x
    induction y with | mk y
    induction z with | mk z
    rw [← mk_mul, ← mk_mul]
    exact mk_mul_le_of_le h le_rfl

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
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
h : x * y = 0
⊢ False

Tactic:
by simp [h] at this

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
inst✝² : Zero Γ
inst✝¹ : AddCommGroup R
inst✝ : One R
g : Γ
hg : 0 < g
r : R
⊢ 0 < (1 + (single g) r - 1).orderTop

Tactic:
by_cases hr : r = 0 <;> simp [hr, hg]

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

Goal state before:
pp: F : Type u_2
inst✝ : Field F
P : RingPreordering F
x : F
h : x ∈ P
h2 : -x ∈ P
⊢ x = 0

Tactic:
by
  by_contra
  have mem : -x * x⁻¹ ∈ P := by aesop (erase simp neg_mul)
  field_simp at mem
  exact RingPreordering.neg_one_notMem P mem

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

Tactic:
rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub]

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
y z : ↥(↑f).domain
c : FiniteArchimedeanClass M
hy : ↑y - x ∈ ball K c
hz : ↑z - x ∈ ball K c
d : FiniteArchimedeanClass M
hd : d ≤ c
⊢ (ofLex (↑↑f (y - z))).coeff d = 0
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case a
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ ((algebraMap (↥R) K) r)⁻¹ ∈ S

Tactic:
· rw [← valuation_le_one_iff, map_inv₀, ← inv_one, inv_le_inv₀]
      · exact not_lt.1 ((not_iff_not.2 <| valuation_lt_one_iff S _).1 hr)
      · simpa [Valuation.pos_iff] using fun hr₀ ↦ hr₀ ▸ hr <| Ideal.zero_mem (R.idealOfLE S h)
      · exact zero_lt_one

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
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ f.eval x = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))

Tactic:
by
  unfold eval
  rw [toLex.injective.eq_iff]
  ext d
  simp only
  obtain hd | hd := lt_or_ge d c
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hd]
    exact evalCoeff_eq _ fun _ ↦ by simpa [hy]
  · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hd]
    apply evalCoeff_eq_zero
    contrapose! h
    obtain ⟨z, hz⟩ := h
    exact ⟨z, (ball_strictAnti K).antitone (by simpa using hd) hz⟩

Goal state after:
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
  simp only [Set.mem_image, SetLike.mem_coe, mem_nonunits_iff_exists_mem_maximalIdeal]
  rw [Subtype.exists]
  simp_rw [exists_and_right, exists_eq_right]

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

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x = (-1)⁻¹
⊢ x ∈ B

Tactic:
inv_neg,

Goal state after:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x = -1⁻¹
⊢ x ∈ B
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:
by
  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
⊢ 0 < ↑(f.extendFun hx) (z - y)

Tactic:
obtain hyzmem := (z - y).prop

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.extendFun hx).domain
⊢ 0 < ↑(f.extendFun hx) (z - y)
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
  induction a using QuotientGroup.induction_on with | _ a
  simp only [mem_stabilizer_iff, Subgroup.mem_bot, QuotientGroup.eq_one_iff]
  have : q a • q '' s = q '' (a • s) :=
    (image_smul_distrib (QuotientGroup.mk' <| stabilizer G s) _ _).symm
  rw [this]
  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
  rwa [QuotientGroup.image_coe_inj, mul_smul_comm, stabilizer_mul_self] at h

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

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : mk x < 0
⊢ stdPart x = 0

pp: case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ stdPart x = 0

Tactic:
· exact dif_neg h.not_ge

Goal state after:
case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
h✝ : mk x ≠ 0
h : 0 < mk x
⊢ stdPart x = 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
hx : 0 ≤ mk x
h : r < stdPart x
⊢ stdPart x = r

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_between h
    cases (stdPart_le_of_le f hx (hr _ hs)).not_gt hs'

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

Goal state before:
pp: case pos.inl
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : d < c
⊢ ↑(ball K c) ⊆ ↑(ball K d)

Tactic:
simpa using (ball_strictAnti K hdc).le

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
x : A
p : A[X]
⊢ d (eval x p) = (PolynomialModule.eval x) (d.mapCoeffs p) + eval x (derivative p) • d x

Tactic:
convert! apply_aeval_eq d x p
  ext
  rfl

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

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

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
· rw [hp, zero_mul, mirror_zero, zero_mul]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
rcases le_or_gt k n with hkn | hnk

Goal state after:
case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b c : α
l : List α
IH : ∀ (a : α), IsChain R (destutter' R a l)
IH2 : ∀ (y a : α), IsChain R (destutter' R a (y :: l))
a : α
⊢ IsChain R (destutter' R a (b :: c :: l))

Tactic:
| cons_cons b c l IH IH2 =>

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

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

Tactic:
by simp [destutter]

Goal state after:
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
⊢ (trinomial k m n u v w).coeff m = v

Tactic:
by
  rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
    if_neg hkm.ne', if_pos rfl, if_neg hmn.ne, zero_add, add_zero]

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

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

Tactic:
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: