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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f.support ⊆ g.support
hg : ¬g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)

Tactic:
rw [m.withBotDegree_le_withBotDegree_iff_of_ne_zero _ hg]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f.support ⊆ g.support
hg : ¬g = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
a : σ
h : (m.degree f) a ≤ (m.degree g) a
⊢ (m.degree g - m.degree f) a = (m.degree f ⊔ m.degree g - m.degree f) a

Tactic:
simp [h]

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

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
a : σ
h : (m.degree g) a ≤ (m.degree f) a
⊢ (m.degree g - m.degree f) a = (m.degree f ⊔ m.degree g - m.degree f) a

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
h : x = 1
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } x =
    ({ toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1) x

Tactic:
simp [h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
h : ¬x = 1
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } x =
    ({ toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1) x

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ 0 ^ k = 0

Tactic:
zero_pow h0

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

Goal state before:
pp: case refine_2.refine_1
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a

Tactic:
use y

Goal state after:
case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_2.refine_2
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a

Tactic:
use y

Goal state after:
case h
n : ℕ
S : Finset ℕ := ⋯
hSne : S.Nonempty
s : ℕ := ⋯
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
⊢ ↑f 1 = 1

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
⊢ ↑f 1 = 1

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ ∀ {m n : ℕ}, m.Coprime n → (f * g) (m * n) = (f * g) m * (f * g) n

Tactic:
simp only [mul_apply]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ ∀ {m n : ℕ},
    m.Coprime n →
      ∑ x ∈ (m * n).divisorsAntidiagonal, f x.1 * g x.2 =
        (∑ x ∈ m.divisorsAntidiagonal, f x.1 * g x.2) * ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
hn : n ≠ 0
h : n = 1
⊢ #n.divisors = 1

Tactic:
simp [h]

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

Goal state before:
pp: case mpr
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ a, (∏ i, a i = k * r ∧ k * r ≠ 0) ∧ a i = k

Tactic:
use fun j => if j = i then k else if j = i' then r else 1

Goal state after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ i_1, (fun j ↦ if j = i then k else if j = i' then r else 1) i_1 = k * r ∧ k * r ≠ 0) ∧
    (fun j ↦ if j = i then k else if j = i' then r else 1) i = k
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, (f * g) n = ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2

Tactic:
simp only [mul_apply]

Goal state after:
R : Type u_2
inst✝ : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ ∑ n ∈ Ioc 0 N, ∑ x ∈ n.divisorsAntidiagonal, f x.1 * g x.2 =
    ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N, f x.1 * g x.2
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁)) (c₂ * c₁ * m.leadingCoeff p₂) * p₁ -
      (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂)) (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂

Tactic:
mul_comm c₂ c₁

Goal state after:
σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₁ + m.degree p₁) + d₁)) (c₁ * c₂ * m.leadingCoeff p₂) * p₁ -
      (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - (d₂ + m.degree p₂) + d₂)) (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case e_a.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h✝ :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : m.degree (g b') = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b'))
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
simp [h]

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

Goal state before:
pp: case e_a.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h✝ :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
h : g b' = 0
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
a✝ : Nontrivial R
⊢ m.toSyn (m.degree (C r)) < m.toSyn (m.degree (X i))

Tactic:
simp [degree_C, degree_X, ← not_le, ← eq_zero_iff]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ min (mk y) (mk z) ≤ mk (max |y|ₘ |z|ₘ)

Tactic:
max_eq_left h,

Goal state after:
case inr
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
x y z : M
hy : y ≤ x
hz : x ≤ z
H : |x|ₘ ≤ |max |y|ₘ |z|ₘ|ₘ
h : |z|ₘ ≤ |y|ₘ
⊢ min (mk y) (mk z) ≤ mk |y|ₘ
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
⊢ ¬∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i

Tactic:
set τ : Perm ι := (Equiv.swap x y).trans σ

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✝ : 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) σ
⊢ ¬∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i
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)
heq : ↑(subsemigroup t) = ↑(subsemigroup s)
⊢ t = s

Tactic:
simpa [MulArchimedeanClass.mk_surjective, MulArchimedeanClass.subsemigroup] using heq

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

Goal state before:
pp: case pos
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
α : Type u_2
f : { a // a ≠ 1 } → α
h : ∀ (a b : { a // a ≠ 1 }), mk ↑a ⋯ = mk ↑b ⋯ → f a = f b
x✝ : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : MulArchimedeanClass.mk a = MulArchimedeanClass.mk b
ha : ¬a = 1
hb : b = 1
⊢ ↑(f ⟨a, ha⟩) = ⊤

Tactic:
exact (ha (MulArchimedeanClass.mk_eq_top_iff.mp (by apply hb ▸ h'))).elim

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

Goal state before:
pp: case inr.inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
H : Subgroup G
inst✝ : Nontrivial ↥H
hH : IsCyclic ↥H
ha : Subgroup.zpowers 1 = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
rw [Subgroup.zpowers_one_eq_bot] at ha
    exact absurd ha.symm <| (H.nontrivial_iff_ne_bot).mp inferInstance

Goal state after:
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
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Subgroup.zpowers g1 = Subgroup.zpowers g2
h' : Nontrivial ↥(Subgroup.zpowers g2)
h1 : IsCyclic ↥(Subgroup.zpowers g2)
h2 : Nontrivial ↥(Subgroup.zpowers g1)
h3 : IsCyclic ↥(Subgroup.zpowers g1)
⊢ Subgroup.genLTOne (Subgroup.zpowers g1) = g2

Tactic:
simp only [(Subgroup.zpowers g1).genLTOne_unique hg2 h.symm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s : NonemptyInterval α
⊢ ↑⊥ = ↑↑s ∩ ↑⊥

Tactic:
exact (inter_empty _).symm

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 : NonemptyInterval α✝
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
hab : a + b = 0
h : pure a + pure b = 0
⊢ -pure a = pure b

Tactic:
rw [neg_pure, neg_eq_of_add_eq_zero_right hab]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
h : b = a
⊢ ((single a) r).coeff b = r

Tactic:
simp [h]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
h : ¬b = a
⊢ ((single a) r).coeff b = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
g : Γ
h : g = a
⊢ (((single a) r).map f).coeff g = ((single a) (f r)).coeff g

Tactic:
simp [h]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
g : Γ
h : ¬g = a
⊢ (((single a) r).map f).coeff g = ((single a) (f r)).coeff g

Tactic:
simp [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
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
⊢ 0 < x.orderTop

Tactic:
by
  by_cases h : x = 0
  · simp_all only [order_zero, lt_self_iff_false]
  · exact (zero_lt_orderTop_iff h).mpr hx

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

Goal state before:
pp: case neg.hnc
Γ : 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
⊢ f a ∉ ⇑f '' x.support

Tactic:
contrapose ha

Goal state after:
case neg.hnc
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : f a ∈ ⇑f '' x.support
⊢ a ∈ x.support
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 Γ'
g : Γ
r : R
g' : Γ'
h : g' = f g
⊢ (embDomain f ((single g) r)).coeff g' = ((single (f g)) r).coeff g'

Tactic:
simp [h]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c i : Γ
h : i < c
x : R⟦Γ⟧
⊢ ((truncLT c) x).coeff i = x.coeff i

Tactic:
simp [h]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
c i : Γ
h : c ≤ i
x : R⟦Γ⟧
⊢ ((truncLT c) x).coeff i = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
h : i < c
⊢ ((truncLT c) (x + y)).coeff i = ((truncLT c) x + (truncLT c) y).coeff i

Tactic:
simp [h]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : DecidableLT Γ
c : Γ
x y : R⟦Γ⟧
i : Γ
h : ¬i < c
⊢ ((truncLT c) (x + y)).coeff i = ((truncLT c) x + (truncLT c) y).coeff i

Tactic:
simp [h]

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

Goal state before:
pp: case pos
Γ : 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 Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
a : Γ
r : R
s : V
b : Γ
h : b = a
⊢ ((↑(addMonoidHom a)).toFun (r • s)).coeff b = ((RingHom.id R) r • (↑(addMonoidHom a)).toFun s).coeff b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
Γ : 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 Γ
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
a : Γ
r : R
s : V
b : Γ
h : ¬b = a
⊢ ((↑(addMonoidHom a)).toFun (r • s)).coeff b = ((RingHom.id R) r • (↑(addMonoidHom a)).toFun s).coeff b

Tactic:
simp [h]

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:
rw [← sub_nonneg] at hab ⊢

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 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 |y|).orderTop < (ofLex |x|).orderTop
⊢ (ofLex |x|).coeff ((ofLex |y|).orderTop.untop ⋯) < (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯)

Tactic:
· simpa [-orderTop_abs, coeff_eq_zero_of_lt_orderTop, coeff_untop_eq_leadingCoeff, h]
      using h.ne_top

Goal state after:
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
x : G
h₁ : 0 ≤ x
h₂ : x < ↑b
hx' : ¬x = 0
this : 0 ≤ ↑b ∧ ↑b ≤ a
⊢ ⟨0, ⋯⟩ ≠ ⟨x, ⋯⟩

Tactic:
by simpa using! Ne.symm hx'

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
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
eq : u.stratum c = ⊥
⊢ ball K c ⊔ ⊥ < closedBall K c

Tactic:
by simpa using ball_lt_closedBall _

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 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|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex |y|).coeff ((ofLex x).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex x).orderTop.untop ⋯)

Tactic:
convert! this using 3

Goal state after:
case e'_3
Γ : 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|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop = (ofLex |y|).orderTop

case e'_4
Γ : 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|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop.untop ⋯ = (ofLex |x|).orderTop.untop ⋯
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case e'_3
Γ : 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|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop = (ofLex |y|).orderTop

Tactic:
simp [h]

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

Goal state before:
pp: case e'_4
Γ : 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|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop.untop ⋯ = (ofLex |x|).orderTop.untop ⋯

Tactic:
simp [h]

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

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
u : ArchimedeanStrata K M
c : FiniteArchimedeanClass M
a : ↥(u.stratum c)
ha : a ≠ 0
b : ↥(u.stratum c)
hb : b ≠ 0
⊢ ↑a ≠ 0

Tactic:
by simpa using ha

Goal state after: