mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : 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✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
x✝ : Γ
⊢ (x✝ ∈ Function.support fun a ↦ AddOpposite.unop (x.coeff a)) ↔ x✝ ∈ x.support

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Nonempty Γ
⊢ BddBelow (Function.support 0)

Tactic:
simp

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : Zero R
inst✝ : LinearOrder Γ
i : WithTop Γ
H : ∀ (j : Γ), ↑j < i → coeff 0 j = 0
⊢ i ≤ orderTop 0

Tactic:
simp

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

Goal state before:
pp: Γ : 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✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
x✝ : Γ
⊢ (x✝ ∈ Function.support fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) ↔ x✝ ∈ (AddOpposite.unop x).support

Tactic:
simp

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

Goal state before:
pp: Γ : 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✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (fun x ↦ { coeff := fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ })
      ((fun x ↦ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }) x) =
    x

Tactic:
simp

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 Γ
⊢ (¬∀ (j : Γ), ↑j < i → x.coeff j = 0) ↔ ∃ j, ↑j < i ∧ x.coeff j ≠ 0

Tactic:
simp

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

Goal state before:
pp: Γ : 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✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ AddOpposite.unop
      ((fun x ↦ AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ })
        ((fun x ↦ { coeff := fun a ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ }) x)) =
    AddOpposite.unop x

Tactic:
simp

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

Goal state before:
pp: Γ : 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✝ : AddMonoid R
x y : Rᵃᵒᵖ⟦Γ⟧
x✝ : Γ
⊢ (AddOpposite.unop (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ })).coeff
      x✝ =
    (AddOpposite.unop
          (AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ } +
            AddOpposite.op { coeff := fun a ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ })).coeff
      x✝

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero R
inst✝¹ : LinearOrder Γ
inst✝ : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : Zero R
inst✝² : LinearOrder Γ
inst✝¹ : LocallyFiniteOrder Γ
inst✝ : Nonempty Γ
⊢ BddBelow (Function.support 0)

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ (Function.support fun i ↦ if i < c then x.coeff i else 0) ⊆ x.support

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : Zero R
inst✝¹ : PartialOrder Γ
inst✝ : DecidableLT Γ
c x✝ : Γ
⊢ { coeff := fun i ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ }.coeff x✝ = coeff 0 x✝

Tactic:
simp

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
⊢ (AddOpposite.unop (addOppositeEquiv 0)).leadingCoeff = AddOpposite.unop (leadingCoeff 0)

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
rw [order_of_ne hx, order_of_ne hy, order_of_ne hxy]

Goal state after:
case neg
R : Type u_3
inst✝² : AddMonoid R
Γ : Type u_8
inst✝¹ : Zero Γ
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
a : Γ
⊢ (embDomain f (x + y)).coeff (f a) = (embDomain f x + embDomain f y).coeff (f a)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x : R⟦Γ⟧
x✝ : Γ
⊢ ((-x).map f).coeff x✝ = (-x.map f).coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : R⟦Γ⟧
x✝ : Γ
⊢ ((x - y).map f).coeff x✝ = (x.map f - y.map f).coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ (1 • x✝¹).coeff x✝ = x✝¹.coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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 Γ
V : Type u_8
inst✝² : Monoid R
inst✝¹ : AddMonoid V
inst✝ : DistribMulAction R V
x✝¹ : R
x✝ : Γ
⊢ (x✝¹ • 0).coeff x✝ = coeff 0 x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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 Γ
V : Type u_8
inst✝⁶ : Monoid R
inst✝⁵ : AddMonoid V
inst✝⁴ : DistribMulAction R V
S : Type u_9
inst✝³ : Monoid S
inst✝² : DistribMulAction S V
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S V
r : R
s : S
a : V⟦Γ⟧
x✝ : Γ
⊢ ((r • s) • a).coeff x✝ = (r • s • a).coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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
x✝¹ : V⟦Γ⟧
x✝ : Γ
⊢ (0 • x✝¹).coeff x✝ = coeff 0 x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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
⊢ (↑(addMonoidHom a)).toFun (r • s) = (RingHom.id R) r • (↑(addMonoidHom a)).toFun s

Tactic:
ext b

Goal state after:
Γ : 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 : Γ
⊢ ((↑(addMonoidHom a)).toFun (r • s)).coeff b = ((RingHom.id R) r • (↑(addMonoidHom a)).toFun s).coeff b
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
U : Type u_5
V : Type u_6
inst✝⁵ : PartialOrder Γ
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid V
inst✝² : Module R V
inst✝¹ : AddCommMonoid U
inst✝ : Module R U
f : U →ₗ[R] V
r : R
x : U⟦Γ⟧
x✝ : Γ
⊢ ((r • x).map f).coeff x✝ = (r • x.map f).coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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
x✝² x✝¹ : Γ →₀ V
x✝ : Γ
⊢ (ofFinsupp (x✝² + x✝¹)).coeff x✝ = (ofFinsupp x✝² + ofFinsupp x✝¹).coeff x✝

Tactic:
simp

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

Goal state before:
pp: Γ : 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
x✝² : R
x✝¹ : Γ →₀ V
x✝ : Γ
⊢ (ofFinsupp (x✝² • x✝¹)).coeff x✝ = ((RingHom.id R) x✝² • ofFinsupp x✝¹).coeff x✝

Tactic:
simp

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

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
a : Γ
⊢ (embDomain f (r • x)).coeff (f a) = (r • embDomain f x).coeff (f a)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid E₁
inst✝⁷ : PartialOrder E₁
inst✝⁶ : AddCommMonoid E₂
inst✝⁵ : PartialOrder E₂
inst✝⁴ : AddCommMonoid E₃
inst✝³ : PartialOrder E₃
inst✝² : Module R E₁
inst✝¹ : Module R E₂
inst✝ : Module R E₃
x✝ : E₁
⊢ ∀ ⦃b : E₁⦄, x✝ ≤ b → (LinearMap.toAddHom 0).toFun x✝ ≤ (LinearMap.toAddHom 0).toFun b

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
E₃ : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid E₁
inst✝⁸ : PartialOrder E₁
inst✝⁷ : AddCommMonoid E₂
inst✝⁶ : PartialOrder E₂
inst✝⁵ : AddCommMonoid E₃
inst✝⁴ : PartialOrder E₃
inst✝³ : Module R E₁
inst✝² : Module R E₂
inst✝¹ : Module R E₃
inst✝ : IsOrderedAddMonoid E₂
f : E₁ →ₚ[R] E₂
x y : E₁
h : x ≤ y
⊢ (0 • f.toLinearMap).toFun x ≤ (0 • f.toLinearMap).toFun y

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder R
x y : Lex R⟦Γ⟧
⊢ (fun x ↦ toLex (ofLex x).coeff) x = (fun x ↦ toLex (ofLex x).coeff) y → x = y

Tactic:
simp

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

Goal state before:
pp: case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
hpos : 0 < (ofLex x).leadingCoeff
hne : ofLex x ≠ 0
htop : (ofLex x).orderTop ≠ ⊤
⊢ ∀ j < (ofLex x).orderTop.untop htop, (ofLex 0).coeff j = (ofLex x).coeff j

Tactic:
intro j

Goal state after:
case mp
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
hpos : 0 < (ofLex x).leadingCoeff
hne : ofLex x ≠ 0
htop : (ofLex x).orderTop ≠ ⊤
j : Γ
⊢ j < (ofLex x).orderTop.untop htop → (ofLex 0).coeff j = (ofLex x).coeff j
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr.inl
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
h : 0 ≤ 0
⊢ 0 ≤ (ofLex 0).leadingCoeff

Tactic:
simp

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

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : PartialOrder R
inst✝² : AddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
a c : Lex R⟦Γ⟧
hab : a ≤ a
⊢ a + c ≤ a + c

Tactic:
simp

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⟦Γ⟧
hle : x ≤ 0
⊢ (ofLex (-x)).support = (ofLex x).support

Tactic:
simp

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 : Lex R⟦Γ⟧
⊢ (ofLex |x|).orderTop = (ofLex x).orderTop

Tactic:
by
  obtain hle | hge := le_total x 0
  · rw [abs_eq_neg_self.mpr hle, ofLex_neg, orderTop_neg]
  · rw [abs_eq_self.mpr hge]

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
inst✝ : Zero Γ
⊢ (ofLex |0|).order = (ofLex 0).order

Tactic:
simp

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

Goal state before:
pp: case inr.inl
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
⊢ (ofLex |0|).leadingCoeff = |(ofLex 0).leadingCoeff|

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
⊢ ↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))) = 0

Tactic:
simp

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

Goal state before:
pp: case inl.inr
M : Type u_1
G : Type u_2
inst✝⁷ : AddCancelCommMonoid M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : LocallyFiniteOrder M
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : LocallyFiniteOrder G
hb ha : 0 ≤ 0
hab : 0 ≤ 0
⊢ ↑(#(Ico 0 (0 + 0))) - ↑(#(Ico 0 (-(0 + 0)))) = ↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))) + (↑(#(Ico 0 0)) - ↑(#(Ico 0 (-0))))

Tactic:
simp

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 : |y| ≤ n • |x|
⊢ n < n + 1

Tactic:
simp

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

Goal state before:
pp: x : ℕ+
⊢ ↑x ∈ nonZeroDivisors ℕ

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ (x y : ℕ+), ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ {a b : ℕ+}, ⟨↑a, ⋯⟩ ≤ ⟨↑b, ⋯⟩ ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: case inr.mpr.refine_1
Γ : 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|
⊢ ∀ j < (ofLex x).orderTop.untop ⋯, (ofLex |y|).coeff j = (ofLex ((n + 1) • |x|)).coeff j

Tactic:
intro j

Goal state after:
case inr.mpr.refine_1
Γ : 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|
j : Γ
⊢ j < (ofLex x).orderTop.untop ⋯ → (ofLex |y|).coeff j = (ofLex ((n + 1) • |x|)).coeff j
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|
⊢ n < n + 1

Tactic:
simp

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
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
x : FiniteArchimedeanClass M
⊢ ↑(⨆ (_ : x ≠ c), u.stratum x) ⊆ ↑(u.stratum x)

Tactic:
simp

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

Goal state before:
pp: ⊢ ∀ ⦃x : PUnit⦄, x ≠ () → IsAddLeftRegular x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ x * (y ⊔ z) = x * y ⊔ x * z

Tactic:
by
  rw [← iSup_pair, ← sSup_pair, mul_sSup_distrib]

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
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
c : FiniteArchimedeanClass M
x : ↥(seed.stratum c)
⊢ ⟨↑x, ⋯⟩ ∈ seed.stratum' c

Tactic:
simp

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
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
⊢ ∀ (i : FiniteArchimedeanClass M), ⟨⟨↑0, ⋯⟩, ⋯⟩ = 0

Tactic:
simp

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
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)
⊢ ∀ (i : FiniteArchimedeanClass M), ↑0 = 0

Tactic:
simp

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
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
⊢ 0 < f.sum fun x x_1 ↦ ↑x_1

Tactic:
hf

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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
⊢ 0 < ↑x
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a : Lex R⟦Γ⟧
⊢ (∃ i,
      (∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex a)).coeff j) ∧
        (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex a)).coeff i) ∨
    embDomain f (ofLex a) = embDomain f (ofLex a)

Tactic:
simp

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : AddMonoid R
⊢ (embDomainOrderEmbedding f).toOrderHom.toFun 0 = 0

Tactic:
simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : SetLike S R
C : S
inst✝ : RingConeClass S R
x✝ : PartialOrder R := PartialOrder.mkOfAddGroupCone C
this : IsOrderedAddMonoid R
⊢ 1 - 0 ∈ C

Tactic:
simp

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

Goal state before:
pp: case refine_1
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
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
⊢ ∀ j < f.support.min' hsupport, (ofLex 0).coeff j = (ofLex (↑seed.baseEmbedding x)).coeff j

Tactic:
intro j

Goal state after:
case refine_1
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
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
⊢ j < f.support.min' hsupport → (ofLex 0).coeff j = (ofLex (↑seed.baseEmbedding x)).coeff j