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 →
      (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₁) c₁ * p₁)))
              (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
            ((monomial d₁) c₁ * p₁) -
          (monomial
                (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) -
                  m.degree ((monomial d₂) c₂ * p₂)))
              (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
            ((monomial d₂) c₂ * p₂) =
        (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
          ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
            (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)
H : c₁ = 0 ∨ c₂ = 0 ∨ p₁ = 0 ∨ p₂ = 0
⊢ (monomial (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₁) c₁ * p₁)))
          (m.leadingCoeff ((monomial d₂) c₂ * p₂)) *
        ((monomial d₁) c₁ * p₁) -
      (monomial
            (m.degree ((monomial d₁) c₁ * p₁) ⊔ m.degree ((monomial d₂) c₂ * p₂) - m.degree ((monomial d₂) c₂ * p₂)))
          (m.leadingCoeff ((monomial d₁) c₁ * p₁)) *
        ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) *
      ((monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)) (m.leadingCoeff p₂) * p₁ -
        (monomial (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)) (m.leadingCoeff p₁) * p₂)

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

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

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

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₂

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

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 : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = (fun x1 x2 ↦ x1 + x2) ↑qa ↑qb

Tactic:
beta_reduce

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
a b : α
qa : ℚ
ha : qa ∈ {t | ↑t < a}
qb : ℚ
hb : qb ∈ {t | ↑t < b}
⊢ ↑(qa + qb) = ↑qa + ↑qb
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

Tactic:
by_cases hi : IsMax i

Goal state after:
case pos
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ 1 - x ≠ 0

Tactic:
ne_eq,

Goal state after:
K : Type u_1
inst✝⁵ : Semifield K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : CanonicallyOrderedAdd K
inst✝¹ : Sub K
inst✝ : OrderedSub K
x : K
h0 : 0 < x
h1 : x < 1
n : ℕ
⊢ ¬1 - x = 0
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case insert.inr.refine_2.inr
ι : 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
σ : 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
hamax : (g (σ a), f (σ a)).1 = (g a, f a).1 ∧ (g (σ a), f (σ a)).2 ≤ (g a, f a).2
⊢ g (σ a) ≤ g a

Tactic:
exact hamax.1.le

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

Goal state before:
pp: case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ s.min' hs = (Finset.cons i s hi).min' ⋯

Tactic:
refine le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ hminmem)

Goal state after:
case cons.inr
M : Type u_1
inst✝³ : CommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedMonoid M
ι : Type u_2
inst✝ : LinearOrder ι
s✝ : Finset ι
a : ι → M
i : ι
s : Finset ι
hi : i ∉ s
hs : s.Nonempty
ih✝ : StrictMonoOn (mk ∘ a) ↑s → mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hmono : StrictMonoOn (mk ∘ a) ↑(Finset.cons i s hi)
ih : mk (∏ i ∈ s, a i) = mk (a (s.min' hs))
hminmem : s.min' hs ∈ Finset.cons i s hi
hne : mk (a i) ≠ mk (∏ i ∈ s, a i)
hlt : mk (∏ i ∈ s, a i) < mk (a i)
⊢ ∀ y ∈ Finset.cons i s hi, s.min' hs ≤ y
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: case mp
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = hs.min hns * ht.min hnt
⊢ a = hs.min hns ∧ b = ht.min hnt

Tactic:
obtain rfl :=
      (hs.min_le hns has).eq_of_not_lt fun hlt =>
        (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst

Goal state after:
case mp
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : α
hat : b ∈ t
has : hs.min hns ∈ s
hst : hs.min hns * b = hs.min hns * ht.min hnt
⊢ hs.min hns = hs.min hns ∧ b = ht.min hnt
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
⊢ leadingCoeff 0 = 0

Tactic:
by simp [leadingCoeff]

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
⊢ leadingCoeff 0 = 0 ↔ 0 = 0

Tactic:
simp [leadingCoeff_of_ne_zero, coeff_orderTop_ne, *]

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

Goal state before:
pp: case inr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.leadingCoeff = 0 ↔ x = 0

Tactic:
simp [leadingCoeff_of_ne_zero, coeff_orderTop_ne, *]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ ¬i ≤ x.orderTop ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0

Tactic:
le_orderTop_iff_forall

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ (¬∀ (j : Γ), ↑j < i → x.coeff j = 0) ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop

Tactic:
← addOppositeEquiv_orderTop,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv (addOppositeEquiv.symm x))).orderTop = (AddOpposite.unop x).orderTop
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✝⁵ : AddCommMonoid E₁
inst✝⁴ : PartialOrder E₁
inst✝³ : AddCommMonoid E₂
inst✝² : PartialOrder E₂
inst✝¹ : Module R E₁
inst✝ : Module R E₂
x✝¹ x✝ : E₁ →ₚ[R] E₂
h : x✝¹.toLinearMap = x✝.toLinearMap
⊢ x✝¹ = x✝

Tactic:
by ext x; congrm($h x)

Goal state after:
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⟦Γ⟧
hlt : x < 0
hlt' : (ofLex x).leadingCoeff < 0
⊢ (-ofLex x).leadingCoeff = -(ofLex x).leadingCoeff

Tactic:
leadingCoeff_neg

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⟦Γ⟧
hlt : x < 0
hlt' : (ofLex x).leadingCoeff < 0
⊢ -(ofLex x).leadingCoeff = -(ofLex x).leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : 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
a1 : Γ
a2 : Γ'
⊢ a1 = b → a2 ∈ ((of R).symm x).support → ¬a1 +ᵥ a2 = b +ᵥ a

Tactic:
rintro rfl h2 h1

Goal state after:
Γ : 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 : Γ'
hr : ¬r = 0
hx : ((of R).symm x).coeff a = 0
a1 : Γ
a2 : Γ'
h2 : a2 ∈ ((of R).symm x).support
h1 : a1 +ᵥ a2 = a1 +ᵥ a
⊢ False
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

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

Tactic:
by_cases h1 : s = 0

Goal state after:
case pos
R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : s ≠ 0 → ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
h1 : s = 0
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)

case neg
R : Type u_1
inst✝² : LinearOrder R
α : Type u_2
β : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Nonempty β
f : α → R
hna : IsNonarchimedean f
g : β → α
a : β
s : Multiset β
h : s ≠ 0 → ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
hs : a ::ₘ s ≠ 0
h1 : ¬s = 0
⊢ f (g a + (Multiset.map g s).sum) ≤ f (g a) ∨ ∃ a_1 ∈ s, f (g a + (Multiset.map g s).sum) ≤ f (g a_1)
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
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ x_1 ∈ antidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = x.coeff a * r

Tactic:
trans ∑ ij ∈ {(a, b)}, x.coeff ij.fst * (single b r).coeff ij.snd

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ x_1 ∈ antidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 =
    ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2

Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a b : Γ
hr : ¬r = 0
hx : ¬x.coeff a = 0
⊢ ∑ ij ∈ {(a, b)}, x.coeff ij.1 * ((single b) r).coeff ij.2 = x.coeff a * r
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ ((single 0) r * x).coeff (a + 0) = r * x.coeff (a + 0)

Tactic:
coeff_single_mul_add,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : R⟦Γ⟧
a : Γ
⊢ r * x.coeff a = r * x.coeff (a + 0)
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Subsingleton R
⊢ ((single g) r * x).order = g + x.order

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r * x).order = g + x.order

Tactic:
· exact (hx <| Subsingleton.eq_zero x).elim

Goal state after:
case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ((single g) r * x).order = g + x.order
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ r * x.leadingCoeff ≠ 0

Tactic:
ne_eq,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
g : Γ
r : R
hr : IsRegular r
x : R⟦Γ⟧
hx : x ≠ 0
h✝ : Nontrivial R
⊢ ¬r * x.leadingCoeff = 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✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x : R⟦Γ⟧
⊢ x * 1 = x

Tactic:
ext
    exact coeff_mul_single_zero.trans (mul_one _)

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

Goal state before:
pp: case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ (n + 1)).orderTop

Tactic:
pow_add

Goal state after:
case succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop
Module: Mathlib.Order.Quotient

Goal state before:
pp: case refine_1
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
h : Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂

Tactic:
exact .trans (.single <| .inr (symm hx)) <| .trans h (.single <| .inr hy)

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

Goal state before:
pp: case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
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
hdc : d < c
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = (seed.coeff d) (f d)

Tactic:
apply congrArg

Goal state after:
case refine_2.inl
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
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) := ⋯
d : FiniteArchimedeanClass M
hdc : d < c
⊢ (DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d = f d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_2.inr
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
hdc : c ≤ d
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = 0

Tactic:
have hcd : c.val ≤ d.val := hdc

Goal state after:
case refine_2.inr
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
hdc : c ≤ d
hcd : ↑c ≤ ↑d
⊢ (seed.coeff d) ((DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d) d) = 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✝¹³ : PartialOrder Γ✝
inst✝¹² : IsOrderedCancelAddMonoid Γ✝
inst✝¹¹ : PartialOrder Γ'
inst✝¹⁰ : AddAction Γ✝ Γ'
inst✝⁹ : IsOrderedCancelVAdd Γ✝ Γ'
inst✝⁸ : AddCommMonoid V✝
Γ : Type u_6
V : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Module R V
inst✝ : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ x • y ≠ 0

Tactic:
ne_eq,

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✝¹¹ : PartialOrder Γ'
inst✝¹⁰ : AddAction Γ✝ Γ'
inst✝⁹ : IsOrderedCancelVAdd Γ✝ Γ'
inst✝⁸ : AddCommMonoid V✝
Γ : Type u_6
V : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Module R V
inst✝ : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ¬x • y = 0
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ ⟦x⟧ ≤ ⟦y⟧ ↔ x ≤ y ∨ x ≈ y

Tactic:
rw [← propext_iff]

Goal state after:
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y : α
⊢ (⟦x⟧ ≤ ⟦y⟧) = (x ≤ y ∨ x ≈ y)
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

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

Tactic:
aesop (erase simp neg_mul)

Goal state after:
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
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬(y, z).1 + (y, z).2 = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0

Tactic:
eq_of_mem_support_single hy,

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
y z : Γ
hy : (y, z).1 ∈ ((single a) r).support
hz : (y, z).2 ∈ ((single b) s).support
h : ¬a + (y, z).2 = a + b
⊢ ((single a) r).coeff (y, z).1 * ((single b) s).coeff (y, z).2 = 0