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

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ : MvPolynomial σ R) (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
    c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0 →
      m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
        (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
            (c₁ * c₂) *
          m.sPolynomial p₁ p₂
H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

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
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

Tactic:
· (obtain rfl | rfl | rfl | rfl := H) <;> simp

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
H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂

Tactic:
classical
  wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  simp [H, degree_mul, sPolynomial_monomial_mul, degree_monomial]

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
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
    (p₁ p₂ q₁ q₂ : MvPolynomial σ R),
    p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0 →
      m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
        (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
            (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
          m.sPolynomial q₁ q₂
H : p₁ = 0 ∨ p₂ = 0 ∨ q₁ = 0 ∨ q₂ = 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

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₂ q₁ q₂ : MvPolynomial σ R
H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂

Tactic:
· (obtain rfl | rfl | rfl | rfl := H) <;> simp

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₂ q₁ q₂ : MvPolynomial σ R
H : p₁ ≠ 0 ∧ p₂ ≠ 0 ∧ q₁ ≠ 0 ∧ q₂ ≠ 0
⊢ m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (monomial (m.degree (p₁ * q₁) ⊔ m.degree (p₂ * q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ Set.SurjOn
    (fun x ↦
      match x with
      | ((i, j), k, l) => (i * k, j * l))
    ↑(m.divisorsAntidiagonal ×ˢ n.divisorsAntidiagonal) ↑(m * n).divisorsAntidiagonal

Tactic:
simp only [Set.SurjOn, Set.subset_def, mem_coe, mem_divisorsAntidiagonal, mem_product,
      Set.mem_image]

Goal state after:
case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ ∀ (x : ℕ × ℕ),
    x.1 * x.2 = m * n ∧ m * n ≠ 0 →
      ∃ x_1,
        ((x_1.1.1 * x_1.1.2 = m ∧ m ≠ 0) ∧ x_1.2.1 * x_1.2.2 = n ∧ n ≠ 0) ∧ (x_1.1.1 * x_1.2.1, x_1.1.2 * x_1.2.2) = x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ 0 < m.toSyn (single i 1)

Tactic:
← bot_eq_zero,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_3
m : MonomialOrder ι
i : ι
r : R
⊢ ⊥ < m.toSyn (single i 1)
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑(#s) * ∑ i ∈ s, f i * g i

Tactic:
← nsmul_eq_mul

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i * g i
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ ↑(#s) * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
← nsmul_eq_mul

Goal state after:
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ #s • ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, 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
α : Type u_2
f : M → M → α
h : ∀ (a₁ b₁ a₂ b₂ : M), mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂
a b : M
⊢ lift₂ f h (mk a) (mk b) = f a b

Tactic:
by
  unfold lift₂
  exact Quotient.lift₂_mk f (fun _ _ _ _ h₁ h₂ ↦ h _ _ _ _ (mk_eq_mk.mpr h₁) (mk_eq_mk.mpr h₂)) a b

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 b : M
h : mk (a * b) < mk a ∧ mk (a * b) < mk b
⊢ False

Tactic:
have h1 := (mk_lt_mk.mp h.1 2).trans_le (mabs_mul_le _ _)

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
h : mk (a * b) < mk a ∧ mk (a * b) < mk b
h1 : |a|ₘ ^ 2 < |a|ₘ * |b|ₘ
⊢ False
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
← sub_pos

Goal state after:
case inr
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0∞
n : ℕ∞
hn : n ≠ ⊤
⊢ ⌊r⌋ₑ ≤ n ↔ r < ↑n + 1

Tactic:
by simp [← lt_add_one_iff hn]

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

Goal state before:
pp: case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c + ↑x ∈ Ico c (c + ↑(#s))

Tactic:
rw [mem_Ico]

Goal state after:
case refine_1
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + ↑x ∧ c + ↑x < c + ↑(#s)
Module: Mathlib.Algebra.Order.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : Invertible 2
inst✝³ : Lattice M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsOrderedAddMonoid M
x y : M
⊢ x ⊔ y = ⅟2 • (x + y + |y - x|)

Tactic:
by
  rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R,
    smul_smul, invOf_mul_self, one_smul]

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 α
s t : NonemptyInterval α
h : s + t = 0
⊢ -s = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
    rw [neg_pure, neg_eq_of_add_eq_zero_right hab]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ↑a ≤ ((single a) r).orderTop

Tactic:
by_cases hr : r = 0
  · simp only [hr, map_zero, orderTop_zero, le_top]
  · rw [orderTop_single hr]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
⊢ embDomain f ((single g) r) = (single (f g)) r

Tactic:
ext g'

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
⊢ (embDomain f ((single g) r)).coeff g' = ((single (f g)) r).coeff g'
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hle : x ≤ 0
⊢ (ofLex |x|).support = (ofLex x).support

Tactic:
abs_eq_neg_self.mpr hle

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hle : x ≤ 0
⊢ (ofLex (-x)).support = (ofLex x).support
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
g : G
⊢ 0 < g → 0 < (orderAddMonoidHom G) g

Tactic:
H

Goal state after:
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
g : G
H : 0 < g
⊢ 0 < (orderAddMonoidHom G) g
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
this : 1 ∈ (orderAddMonoidHom G).range
⊢ Function.Surjective ⇑(orderAddMonoidHom G)

Tactic:
by
    obtain ⟨x, hx⟩ := this
    exact fun a ↦ ⟨a • x, by simp_all⟩

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

Goal state before:
pp: x : ↥(nonZeroDivisors ℕ)
⊢ 0 < ↑x

Tactic:
simp [Nat.pos_iff_ne_zero]

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⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ (ofLex y).orderTop < (ofLex (n • x)).orderTop

Tactic:
apply lt_of_lt_of_le hgt

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⟦Γ⟧
hgt : (ofLex y).orderTop < (ofLex x).orderTop
n : ℕ
hn :
  (ofLex y).orderTop ≤ (ofLex x).orderTop ∧
    ((ofLex x).orderTop = (ofLex y).orderTop → ∀ (n : ℕ), n • |(ofLex x).leadingCoeff| < |(ofLex y).leadingCoeff|)
⊢ (ofLex x).orderTop ≤ (ofLex (n • x)).orderTop
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := ⋯
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ seed.baseDomain.subtype x = seed.baseDomain.subtype ((DirectSum.coeAddMonoidHom seed.stratum') f')

Tactic:
rw [DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index (by simp)]

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
x : ↥seed.baseDomain
f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)
h : ↑x = f.sum fun c ↦ ⇑(seed.stratum c).subtype
c : FiniteArchimedeanClass M
hxm : ∀ {c : FiniteArchimedeanClass M} (x : ↥(seed.stratum c)), ↑x ∈ seed.baseDomain
f' : ⨁ (c : FiniteArchimedeanClass M), ↥(seed.stratum' c) := DFinsupp.mapRange (fun c x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩) ⋯ f
hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c)
⊢ seed.baseDomain.subtype x = seed.baseDomain.subtype (f.sum fun i b ↦ ↑⟨⟨↑b, ⋯⟩, ⋯⟩)
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✝³ : NonAssocSemiring α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (↑n * a) ≤ f a

Tactic:
← nsmul_eq_mul

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝³ : NonAssocSemiring α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (n • a) ≤ f a
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 : α
hne : f x ≠ f y
⊢ f (x + y) = max (f x) (f y)

Tactic:
by
  rcases hne.lt_or_gt with h_lt | h_lt
  · rw [add_eq_right_of_lt hna h_lt]
    exact (max_eq_right_of_lt h_lt).symm
  · rw [add_eq_left_of_lt hna h_lt]
    exact (max_eq_left_of_lt h_lt).symm

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
s : Multiset β
hs : s ≠ 0
⊢ ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
y : S
hy : y ≠ 0
⊢ mk x ≤ mk (f y) + mk x

Tactic:
rw [mk_map_of_archimedean' f hy, zero_add]

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
β : Type u_4
inst✝⁴ : AddCommMonoid α
inst✝³ : FunLike F α R
inst✝² : ZeroHomClass F α R
inst✝¹ : NonnegHomClass F α R
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: S : Type u_3
inst✝² : LinearOrder S
inst✝¹ : CommRing S
inst✝ : IsStrictOrderedRing S
n : ℤ
h : n ≠ 0
⊢ mk ↑n = 0

Tactic:
obtain _ | _ := subsingleton_or_nontrivial S
  · exact Subsingleton.allEq ..
  · exact mk_map_of_archimedean' ⟨Int.castRingHom S, fun _ ↦ by simp⟩ h

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

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : PartialOrder Γ'
inst✝¹ : AddCommGroup Γ'
inst✝ : IsOrderedAddMonoid Γ'
r : R
x : R⟦Γ'⟧
a b : Γ'
⊢ (x * (single b) r).coeff a = x.coeff (a - b) * r

Tactic:
simpa using coeff_mul_single_add (a := a - b) (b := b)

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∑ ij ∈ VAddAntidiagonal b ⋯, (x * y).coeff ij.1 • ((of R).symm z).coeff ij.2 =
    ∑ ij ∈ VAddAntidiagonal b ⋯, x.coeff ij.1 • ((of R).symm (y • z)).coeff ij.2

Tactic:
simp only [HahnSeries.coeff_mul, coeff_smul, sum_smul, smul_sum, sum_sigma']

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
⊢ ∑ x_1 ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ antidiagonal ⋯ ⋯ a.1,
      (x.coeff x_1.snd.1 * y.coeff x_1.snd.2) • ((of R).symm z).coeff x_1.fst.2 =
    ∑ x_1 ∈ (VAddAntidiagonal b ⋯).sigma fun a ↦ VAddAntidiagonal a.2 ⋯,
      x.coeff x_1.fst.1 • y.coeff x_1.snd.1 • ((of R).symm z).coeff x_1.snd.2
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: F : Type u_2
inst✝ : Field F
P : RingPreordering F
a : F
ha : a ∈ P
⊢ a⁻¹ ∈ P

Tactic:
have mem : a * (a⁻¹ * a⁻¹) ∈ P := by aesop
  field_simp at mem
  simp_all

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ (C 0).order = 0

Tactic:
C_zero,

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ order 0 = 0
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✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
hyz : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ y = z

Tactic:
let : AddCancelCommMonoid R := ⟨⟩

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
hyz : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
⊢ y = z
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✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
hyz : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ y = z

Tactic:
let : AddCancelCommMonoid R := ⟨⟩

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : IsCancelAdd R
inst✝ : IsCancelMulZero R
x : R⟦Γ⟧
hx : x ≠ 0
y z : R⟦Γ⟧
hyz : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
this : AddCancelCommMonoid R := { toAddCommMonoid := inst✝².toAddCommMonoid, toIsLeftCancelAdd := ⋯ }
⊢ y = z
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
⊢ f.eval 0 = 0

Tactic:
by
  unfold eval
  convert! toLex_zero
  ext c
  rw [f.evalCoeff_eq (y := 0) (by simp)]
  simp

Goal state after:
Module: Mathlib.Algebra.Star.Conjneg

Goal state before:
pp: G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ x✝ ∈ support (conjneg f) ↔ x✝ ∈ -support f

Tactic:
simp [starRingEnd_apply]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Conjneg

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ ∀ (b : G), 0 ((Equiv.symm (Equiv.neg G)) b) ≤ conjneg f ((Equiv.symm (Equiv.neg G)) b) ↔ 0 b ≤ f b

Tactic:
simp [starRingEnd_apply]

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

Goal state before:
pp: case neg.inr
K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : ↥A
h✝ : ¬↑b = 0
h : ¬↑a = 0
hh : (↑a / ↑b)⁻¹ ∈ A
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
· rw [show (a / b : K)⁻¹ = b / a by simp] at hh
      use ⟨b / a, hh⟩
      left
      ext
      simp [field]

Goal state after: