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✝ : Field R
d : m.syn
ι : Type u_3
B : Finset ι
g : ι → MvPolynomial σ R
hd : ∀ b ∈ B, m.toSyn (m.degree (g b)) = d ∨ g b = 0
hfd : m.toSyn (m.degree (∑ b ∈ B, g b)) < d
⊢ ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)

Tactic:
refine m.sPolynomial_decomposition ?_ hfd
  simpa [and_or_right, em']

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

Goal state before:
pp: case pos
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
h₁ : ¬σ x = a
h₂ : σ x = σ a
hx : ¬a = x
⊢ x ∈ ↑s

pp: case neg
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
h₁ : ¬σ x = a
h₂ : ¬σ x = σ a
hx : ¬σ x = x
⊢ x ∈ ↑s

Tactic:
· exact (hx <| σ.injective h₂.symm).elim

Goal state after:
case neg
ι : 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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
h₁ : ¬σ x = a
h₂ : ¬σ x = σ a
hx : ¬σ x = x
⊢ x ∈ ↑s
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ f 0 = g 0

Tactic:
ArithmeticFunction.map_zero,

Goal state after:
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
g : ArithmeticFunction R
hg : g.IsMultiplicative
h : ∀ (p i : ℕ), Nat.Prime p → f (p ^ i) = g (p ^ i)
n : ℕ
hn : n = 0
⊢ 0 = g 0
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
by
  cases nonempty_fintype ι
  cases isEmpty_or_nonempty ι
  · obtain ⟨a, ha⟩ := exists_ne (0 : α)
    obtain ha | ha := ha.lt_or_gt <;> obtain ⟨b, hb, -⟩ := exists_pos_add_of_lt' ha <;>
      exact ⟨b, hb, isEmptyElim⟩
  choose ε hε hxε using fun i => exists_pos_add_of_lt' (h i)
  obtain rfl : x + ε = y := funext hxε
  have hε : 0 < Finset.univ.inf' Finset.univ_nonempty ε := (Finset.lt_inf'_iff _).2 fun i _ => hε _
  obtain ⟨δ, hδ, hδε⟩ := exists_between hε
  exact ⟨δ, hδ, fun i ↦ add_lt_add_right (hδε.trans_le <| Finset.inf'_le _ <| Finset.mem_univ _) _⟩

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

Goal state before:
pp: ι : 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
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
z : ι
hz : z ∈ {x_1 | (Equiv.swap x y) x_1 ≠ x_1}
⊢ z ∈ ↑s

Tactic:
obtain ⟨_, rfl | rfl⟩ := swap_apply_ne_self_iff.1 hz <;> assumption

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

Goal state before:
pp: case refine_1
ι : 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
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)

Tactic:
σ.sum_comp' s (fun i j ↦ f i • g j) hσ

Goal state after:
case refine_1
ι : 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
⊢ ∑ x ∈ s, f x • g ((Equiv.symm σ) x) = ∑ i ∈ s, f i • g (σ⁻¹ i)
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : 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 α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Monovary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.monovaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

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
⊢ ⊤.closedBallSubgroup = ⊥

Tactic:
by
  ext
  simp

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

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = H
⊢ g = Subgroup.genLTOne H

Tactic:
have hg' : ¬ IsOfFinOrder g := not_isOfFinOrder_of_isMulTorsionFree (ne_of_lt hg)

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = H
hg' : ¬IsOfFinOrder g
⊢ g = Subgroup.genLTOne H
Module: Mathlib.Algebra.Order.Group.Cyclic

Goal state before:
pp: case inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = Subgroup.zpowers (Subgroup.genLTOne H)
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H

Tactic:
rw [← one_lt_inv', h] at hg

Goal state after:
case inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH✝ : IsCyclic ↥H
g : G
hg : 1 < Subgroup.genLTOne H
hH : Subgroup.zpowers g = Subgroup.zpowers (Subgroup.genLTOne H)
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ ∑ x ∈ s, x ≤ ∑ x ∈ Ioc (c - ↑(#s)) c, x

Tactic:
set r := Ioc (c - #s) c
  calc
    _ ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - #s) := by
      rw [← sum_inter_add_sum_sdiff s r _]
      gcongr
      apply sum_le_card_nsmul
      grind
    _ = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]
    _ ≤ _ := by
      rw [← sum_inter_add_sum_sdiff r s _]
      gcongr
      refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_
      rw [mem_sdiff, mem_Ioc] at mx; exact mx.1.1.le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
⊢ ∀ (x y : α),
    (Prod.Lex.toLexOrderHom.comp ↑(inl α β)).toFun (x * y) =
      (Prod.Lex.toLexOrderHom.comp ↑(inl α β)).toFun x * (Prod.Lex.toLexOrderHom.comp ↑(inl α β)).toFun y

Tactic:
by simp [← toLex_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Monoid α
inst✝² : PartialOrder α
inst✝¹ : Monoid β
inst✝ : Preorder β
⊢ ∀ (x y : β),
    (Prod.Lex.toLexOrderHom.comp ↑(inr α β)).toFun (x * y) =
      (Prod.Lex.toLexOrderHom.comp ↑(inr α β)).toFun x * (Prod.Lex.toLexOrderHom.comp ↑(inr α β)).toFun y

Tactic:
by simp [← toLex_mul]

Goal state after:
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✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬S ⊆ {⊥}
⊢ (⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.1, ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.2).1 ≤
    (⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.1, ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.2).2

Tactic:
by
          obtain ⟨s, hs, ha⟩ := not_subset.1 h
          lift s to NonemptyInterval α using ha
          exact iInf₂_le_of_le s hs (le_iSup₂_of_le s hs s.fst_le_snd)

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⟦Γ⟧
⊢ x.leadingCoeff = 0 ↔ x = 0

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> simp [leadingCoeff_of_ne_zero, coeff_orderTop_ne, *]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : R⟦Γ⟧
⊢ (-x).support = x.support

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup E₁
inst✝⁶ : PartialOrder E₁
inst✝⁵ : IsOrderedAddMonoid E₁
inst✝⁴ : AddCommGroup E₂
inst✝³ : PartialOrder E₂
inst✝² : IsOrderedAddMonoid E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x
a b : E₁
hab : a ≤ b
⊢ f.toFun a ≤ f.toFun b

Tactic:
← sub_nonneg

Goal state after:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup E₁
inst✝⁶ : PartialOrder E₁
inst✝⁵ : IsOrderedAddMonoid E₁
inst✝⁴ : AddCommGroup E₂
inst✝³ : PartialOrder E₂
inst✝² : IsOrderedAddMonoid E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
f : E₁ →ₗ[R] E₂
hf : ∀ (x : E₁), 0 ≤ x → 0 ≤ f x
a b : E₁
hab : 0 ≤ b - a
⊢ 0 ≤ f.toFun b - f.toFun a
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
hvu : v ⊆ u
hv : v.IsWF
i : Γ := hv.min hab
hji : ∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j
hne : (ofLex a).coeff i ≠ (ofLex b).coeff i
hi : (ofLex b).coeff i < (ofLex a).coeff i
⊢ a ≤ b ∨ b ≤ a

Tactic:
· exact Or.inr (le_of_lt ⟨i, fun j hj ↦ (hji j hj).symm, hi⟩)

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
⊢ Nonempty (ArchimedeanStrata K M)

Tactic:
by
  have hstratum (c : FiniteArchimedeanClass M) :
      ∃ G : Submodule K M, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c :=
    IsModularLattice.exists_disjoint_and_sup_eq (ball_lt_closedBall _).le
  choose g h1 h2 using hstratum
  exact ⟨g, h1, h2⟩

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✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
← sub_nonneg

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ a * c - a * b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
← sub_nonneg

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁶ : LinearOrder Γ
inst✝⁵ : LinearOrder R
inst✝⁴ : Ring R
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : IsOrderedRing R
inst✝ : NoZeroDivisors R
a : Lex R⟦Γ⟧
ha : 0 ≤ a
b c : Lex R⟦Γ⟧
hbc : 0 ≤ c - b
⊢ 0 ≤ c * a - b * a
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : 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 : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal (b +ᵥ a) ⋯, ((single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 =
    r • ((of R).symm x).coeff a

Tactic:
simp only [hx, smul_zero]

Goal state after:
case pos
Γ : 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 : Γ'
b : Γ
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
⊢ ∑ x_1 ∈ VAddAntidiagonal (b +ᵥ a) ⋯, ((single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 = 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
⊢ (seed.coeff d) (f' d) = ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d

Tactic:
unfold f'

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) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) =
    ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ((single a) r * (single b) s).coeff x = ((single (a + b)) (r * s)).coeff x

Tactic:
coeff_single_of_ne h,

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ((single a) r * (single b) s).coeff x = 0
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: 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)
⊢ a * b ∈ P

Tactic:
simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)

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

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single (n • a + a)) (r ^ n * r) = (single ((n + 1) • a)) (r ^ n * r)

Tactic:
succ_nsmul

Goal state after:
case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
a : Γ
r : R
n : ℕ
IH : (single a) r ^ n = (single (n • a)) (r ^ n)
⊢ (single (n • a + a)) (r ^ n * r) = (single (n • a + a)) (r ^ n * r)
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

Tactic:
by
  apply eq_of_sub_eq_zero
  rw [← HahnSeries.coeff_sub, ← ofLex_sub, ← LinearPMap.map_sub]
  refine coeff_eq_zero_of_mem f ?_ hd
  have : (y - z).val = (y.val - x) - (z.val - x) := by
    push_cast
    simp
  rw [this]
  exact Submodule.sub_mem _ hy hz

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ stabilizer G univ = ⊤

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Algebra.Pointwise.Stabilizer

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ stabilizer G Finset.univ = ⊤

Tactic:
by
  ext
  simp

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 : M
hx : x ∉ (↑f).domain
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -c • x < a
hc : ¬c = 0
⊢ f.eval (-c • x) < ↑↑f ⟨a, ha⟩

Tactic:
exact f.eval_lt (hx' hc) ⟨a, ha⟩ hac

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 : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ 0 ≤ mk x

Tactic:
apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _) <;> simp

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
⊢ d.mapCoeffs (C x) = PolynomialModule.single A 0 (d x)

Tactic:
by simp [← monomial_zero_left]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
x : A
⊢ mapCoeffs (C x) = C x′

Tactic:
by simp [← monomial_zero_left]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.IsMonicOfDegree 0 ↔ p = 1

Tactic:
simp only [isMonicOfDegree_iff']

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree = 0 ∧ p.Monic ↔ p = 1
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
⊢ p.IsMonicOfDegree n ↔ n = 0

Tactic:
by
  rw [Subsingleton.eq_one p]
  refine ⟨fun ⟨H, _⟩ ↦ ?_, fun H ↦ ?_⟩
  · rwa [natDegree_one, eq_comm] at H
  · rw [H, isMonicOfDegree_zero_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
⊢ p.IsMonicOfDegree n ↔ p.natDegree ≤ n ∧ p.coeff n = 1

Tactic:
simp only [isMonicOfDegree_iff']

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
⊢ p.natDegree = n ∧ p.Monic ↔ p.natDegree ≤ n ∧ p.coeff n = 1