mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ degreeOf j (C c * p) = degreeOf j p

Tactic:
degreeOf_eq_natDegree,

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) (C c * p))).natDegree =
    ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).natDegree
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x ≤ y ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)

Tactic:
simp only [le_iff_eq_or_lt, lt_iff, EmbeddingLike.apply_eq_iff_eq]
  by_cases h : x = y
  · simp [h]
  · by_cases k : (ofDegLex x).degree < (ofDegLex y).degree
    · simp [k]
    · simp only [h, k, false_or]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f ≠ 0 → m.leadingCoeff f ≠ 0

Tactic:
· intro hf
    rw [← support_nonempty] at hf
    rw [leadingCoeff, ← mem_support_iff, degree]
    suffices f.support.sup m.toSyn ∈ m.toSyn '' f.support by
      obtain ⟨d, hd, hd'⟩ := this
      rw [← hd', AddEquiv.symm_apply_apply]
      exact hd
    exact Finset.sup_mem_of_nonempty hf

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LieAdmissibleRing L
⊢ ∀ (x : L), ⁅x, x⁆ = 0

Tactic:
simp [Ring.lie_def]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ s.prod ≠ 0

Tactic:
Ne,

Goal state after:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ ¬s.prod = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
n : ℕ
hf : m.Monic f
a✝ : Nontrivial R
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.withBotDegree ((monomial d) c) = if c = 0 then ⊥ else ↑d

Tactic:
classical
  split_ifs <;> simp [withBotDegree_eq, *, m.degree_monomial]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ s.val.prod ≠ 0

Tactic:
Ne,

Goal state after:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ ¬s.val.prod = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Eq (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod

Tactic:
Multiset.rel_eq

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
g : MvPolynomial σ R
⊢ m.sPolynomial 0 g = 0

Tactic:
by
  simp [sPolynomial]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
refine ⟨p, pp, ?_⟩

Goal state after:
case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
⊢ n / p ^ n.factorization p = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case e_s.mpr
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N n a✝¹ : ℕ
hn : 0 < n ∧ n ≤ N
a✝ : 0 < a✝¹
⊢ a✝¹ ≤ N / n → a✝¹ ≤ N ∧ n * a✝¹ ≤ N

Tactic:
· intro hm
    grw [hm]
    simp [mul_div_le, div_le_self]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
⊢ cutMap β (a + b) = cutMap β a + cutMap β b

Tactic:
refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
  · rw [mem_ofPred_eq, ← sub_lt_iff_lt_add] at hq
    obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
    refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩
    norm_cast
    rw [coe_mem_cutMap_iff]
    exact mod_cast sub_lt_comm.mp hq₁q
  · rintro _ ⟨_, ⟨qa, ha, rfl⟩, _, ⟨qb, hb, rfl⟩, rfl⟩
    -- After https://github.com/leanprover/lean4/pull/2734, `norm_cast` needs help with beta reduction.
    refine ⟨qa + qb, ?_, by beta_reduce; norm_cast⟩
    rw [mem_ofPred_eq, cast_add]
    exact add_lt_add ha hb

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
⊢ ∃ c ∈ cutMap β (a * a), b < c

Tactic:
obtain hb | hb := lt_or_ge b 0

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : b < 0
⊢ ∃ c ∈ cutMap β (a * a), b < c

case inr
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
⊢ ∃ c ∈ cutMap β (a * a), b < c
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case inr.inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁹ : Field α
inst✝⁸ : LinearOrder α
inst✝⁷ : IsStrictOrderedRing α
inst✝⁶ : Field β
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : IsStrictOrderedRing β
inst✝³ : Field γ
inst✝² : ConditionallyCompleteLinearOrder γ
inst✝¹ : IsStrictOrderedRing γ
inst✝ : Archimedean α
a : α
b : β
q : ℚ
this : ∀ (x : α), 0 < x → (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x
x : α
h : 0 < x
⊢ (inducedAddHom α β) (x * x) = (inducedAddHom α β) x * (inducedAddHom α β) x

Tactic:
exact this x h

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ m * n ≠ 0
⊢ ((m = m ∧ m ≠ 0) ∧ n = n ∧ n ≠ 0) ∧ (b1.gcd ((b1, b2).1 * (b1, b2).2), b2.gcd ((b1, b2).1 * (b1, b2).2)) = (b1, b2)

Tactic:
Ne,

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
b1 b2 : ℕ
h : (b1, b2).1 * (b1, b2).2 = m * n ∧ ¬m * n = 0
⊢ ((m = m ∧ m ≠ 0) ∧ n = n ∧ n ≠ 0) ∧ (b1.gcd ((b1, b2).1 * (b1, b2).2), b2.gcd ((b1, b2).1 * (b1, b2).2)) = (b1, b2)
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✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
⊢ (Equiv.symm σ) a ∈ s

Tactic:
Ne,

Goal state after:
ι : 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)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : ¬a = σ a
⊢ (Equiv.symm σ) a ∈ s
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_3
ι : 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)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : x ≠ (Equiv.symm σ) a ∧ x ∈ s
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))

Tactic:
Ne,

Goal state after:
case insert.inr.refine_3
ι : 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)
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hind : ∑ i ∈ s, f i • g (τ i) ≤ ∑ i ∈ s, f i • g i
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
hτs : {x | τ x ≠ x} ⊆ ↑s
hσa : a ≠ σ a
h1s : (Equiv.symm σ) a ∈ s
x : ι
hx : ¬x = (Equiv.symm σ) a ∧ x ∈ s
⊢ f x • g (σ x) = f x • g ((Equiv.swap a (σ a)) (σ x))
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: case mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
B : MulArchimedeanClass M
a : M
hle : mk a ≤ B
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ B

Tactic:
induction B using ind with | mk b

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
inst✝ : PartialOrder α
f : M → α
h : ∀ (a b : M), mk a ≤ mk b → f a ≤ f b
a b : M
hle : mk a ≤ mk b
⊢ lift f ⋯ (mk a) ≤ lift f ⋯ (mk b)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r s : ℝ≥0∞
hrs : r ≤ s
⊢ ⌊r⌋ₑ ≤ ⌊s⌋ₑ

Tactic:
by simpa using hrs.trans' floor_le_self

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
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), ⟨MulArchimedeanClass.mk a, ⋯⟩ ∈ s

Tactic:
Ne,

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : ¬a = 1), ⟨MulArchimedeanClass.mk a, ⋯⟩ ∈ s
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
⊢ ⌊r⌋ₑ = 0 ↔ r < 1

Tactic:
simp [← nonpos_iff_eq_zero]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : MulRightStrictMono α
a b c : α
hc : a * b < c
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a', a' > a ∧ a' * b < c

Tactic:
exact ⟨a', ha', lt_div_iff_mul_lt.1 hc'⟩

Goal state after:
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := ⋯
⊢ ∑ x ∈ s \ r, x ≤ #(s \ r) • (c - ↑(#s))

Tactic:
apply sum_le_card_nsmul

Goal state after:
case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := ⋯
⊢ ∀ x ∈ s \ r, x ≤ c - ↑(#s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

pp: case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.InjOn (fun x ↦ c - ↑x) ↑(range #s)

pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.SurjOn (fun x ↦ c - ↑x) ↑(range #s) ↑(Ioc (c - ↑(#s)) c)

Tactic:
· intro x mx; rw [mem_Ioc]; rw [mem_range] at mx; lia

Goal state after:
case refine_2
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.InjOn (fun x ↦ c - ↑x) ↑(range #s)

case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Set.SurjOn (fun x ↦ c - ↑x) ↑(range #s) ↑(Ioc (c - ↑(#s)) c)
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:
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:
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 β
m : α
n : β
⊢ (inlₗ α β) m * (inrₗ α β) n = toLex (m, n)

Tactic:
simp [← toLex_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
inst✝⁵ : CommGroup α✝
inst✝⁴ : PartialOrder α✝
inst✝³ : IsOrderedMonoid α✝
s t : Interval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
⊢ ∀ (a b : Interval α), a + b = 0 → -a = b

Tactic:
rintro (_ | s) (_ | t) h <;>
      first
        | cases h
        | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)

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.coeff ≠ 0 ↔ x ≠ 0

Tactic:
Ne,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
⊢ ¬x.coeff = 0 ↔ x ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case 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
⊢ a ≤ b ∨ b ≤ a

Tactic:
obtain hi | hi := lt_or_gt_of_ne hne

Goal state after:
case inr.inl
Γ : 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 a).coeff i < (ofLex b).coeff i
⊢ a ≤ b ∨ b ≤ a

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
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
⊢ ArchimedeanClass.mk (∑ i ∈ f.support, ↑(f i)) ≠ ArchimedeanClass.mk a

Tactic:
have hmem (x : FiniteArchimedeanClass M) : (f x).val ∈ u.stratum x :=
      Set.mem_of_mem_of_subset (f x).prop (by simp)
    have hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk (f i).val) f.support := by
      intro x hx y hy hxy
      change ArchimedeanClass.mk (f x).val < ArchimedeanClass.mk (f y).val
      rw [u.archimedeanClassMk_of_mem_stratum (hmem x) (by simpa using hx)]
      rw [u.archimedeanClassMk_of_mem_stratum (hmem y) (by simpa using hy)]
      exact hxy
    rw [ArchimedeanClass.mk_sum hnonempty hmono, u.archimedeanClassMk_of_mem_stratum (hmem _)
      (by simpa using f.support.min'_mem hnonempty), ← val_mk h0, Subtype.coe_ne_coe]
    by_contra!
    obtain h := this ▸ Finset.min'_mem f.support hnonempty
    contrapose! h
    have := u.archimedeanClassMk_of_mem_stratum ha h0
    rw [← val_mk h0, ← Subtype.ext_iff] at this
    simpa [DFinsupp.notMem_support_iff, this] using (f c).prop

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

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁷ : PartialOrder Γ'
inst✝⁶ : AddCommMonoid V
Γ : Type u_6
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : PartialOrder Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MulZeroClass R
inst✝ : SMulWithZero R V
r : R
x : HahnModule Γ' R V
x✝ : Γ'
⊢ ((of R).symm ((single 0) r • x)).coeff x✝ = ((of R).symm (r • x)).coeff x✝

Tactic:
exact coeff_single_zero_smul

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f x < f y
h : f (x + y) ≠ f y
h1 : f (x + y) ≤ f y
⊢ f y < f y

Tactic:
calc
    f y = f (-x + (x + y)) := by simp
    _   ≤ max (f (-x)) (f (x + y)) := hna (-x) (x + y)
    _   < max (f y) (f y) := by
      rw [max_self, map_neg_eq_map]
      exact max_lt h_lt <| lt_of_le_of_ne h1 h
    _   = f y := max_self (f y)

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝² : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝¹ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝ : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
⊢ False

Tactic:
have := h x y

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝³ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝² : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝¹ : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
⊢ False
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✝⁴ : CommSemiring R
A : Type u_6
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Nontrivial Γ
inst✝ : Nontrivial R
⊢ ⊥ ≠ ⊤

Tactic:
Ne,

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✝⁴ : CommSemiring R
A : Type u_6
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Nontrivial Γ
inst✝ : Nontrivial R
⊢ ¬⊥ = ⊤
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
x'' : ↥(↑f).domain := ⟨x', ⋯⟩
hx''mem : ↑x'' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
h0 : (seed.coeff (FiniteArchimedeanClass.mk (↑x) hx0')) ⟨↑x'', hx''mem⟩ ≠ 0
heq' : ↑(FiniteArchimedeanClass.mk (↑x) hx0') = (ofLex (↑↑f x)).orderTop
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Tactic:
simp [← heq']

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

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
⊢ a ∈ IsLocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1

Tactic:
by
  rw [IsLocalRing.mem_maximalIdeal]
  dsimp [nonunits]; rw [valuation_eq_one_iff]
  exact (A.valuation_le_one a).lt_iff_ne.symm

Goal state after: