mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (b - 1)) = Icc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a - 1 ≤ b
⊢ insert (a - 1) (Icc a b) = Icc (a - 1) b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a - 1 ≤ b
⊢ insert (pred a) (Icc a b) = Icc (pred a) b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (a - 1) b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (b - 1)) = Ioc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (b - 1)) = Ioc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert (b - 1) (Ico a (b - 1)) = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert (b - 1) (Ico a (b - 1)) = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo (a - 1) b = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ insert a (Ioc a b) = Ioc (a - 1) b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
a b : α
inst✝ : NoMinOrder α
h : a ≤ b
⊢ insert a (Ioc a b) = Ioc (a - 1) b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : One α
inst✝⁴ : Add α
inst✝³ : Sub α
inst✝² : SuccAddOrder α
inst✝¹ : PredSubOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : One α
inst✝⁴ : Add α
inst✝³ : Sub α
inst✝² : SuccAddOrder α
inst✝¹ : PredSubOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
b : α
⊢ Iio (b + 1) = Iic b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
b : α
⊢ Iic (b - 1) = Iio b
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
⊢ Ici (a + 1) = Ioi a

Tactic:
by
  simpa [succ_eq_add_one] using Ici_succ_eq_Ioi_of_not_isMax ha

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Ici (a + 1) = Ioi a
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a
Module: Mathlib.Algebra.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a : α
⊢ Ioi (a - 1) = Ici a
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: α : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : Interval α
⊢ (s - t).length ≤ s.length + t.length

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
s t : Interval α
⊢ (s + -t).length ≤ s.length + t.length
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x.orderTop ≠ ⊤

Tactic:
simpa using

Goal state after:
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ ¬x = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr.hg
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ f (x.orderTop.untop ⋯) ∈ (embDomain f x).support

Tactic:
simpa using

Goal state after:
case inr.hg
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ ¬x.coeff (x.orderTop.untop ⋯) = 0
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ x.coeff z ≠ 0

Tactic:
simpa using

Goal state after:
case inr.hx
Γ' : Type u_2
R : Type u_3
inst✝² : Zero R
inst✝¹ : PartialOrder Γ'
Γ : Type u_5
inst✝ : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : f z ∈ (embDomain f x).support
⊢ ¬x.coeff z = 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).orderTop = y.orderTop

Tactic:
simpa using

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).orderTop = y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ ↑(x.orderTop.untop ⋯) < y.orderTop

Tactic:
simpa using

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ x.orderTop < y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).leadingCoeff = y.leadingCoeff

Tactic:
simpa using

Goal state after:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : y.orderTop < x.orderTop
⊢ (x + y).leadingCoeff = y.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
⊢ y.coeff x.order = 0

Tactic:
simpa using

Goal state after:
Γ : Type u_1
inst✝² : PartialOrder Γ
R : Type u_8
inst✝¹ : AddCancelCommMonoid R
inst✝ : Zero Γ
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
⊢ y.coeff x.order = 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case inl
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
hg : x.order ∈ y.support
⊢ x.order ∈ x.support

Tactic:
simpa using

Goal state after:
case inl
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this : x.order ≠ y.order
hg : x.order ∈ y.support
⊢ ¬x = 0
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = y.coeff g
⊢ g ∈ x.support

Tactic:
simpa using

Goal state after:
case inr
R : Type u_8
Γ : Type u_9
inst✝² : LinearOrder Γ
inst✝¹ : Zero Γ
inst✝ : AddCancelCommMonoid R
x y : R⟦Γ⟧
hxy : x = y + (single x.order) x.leadingCoeff
hy : y ≠ 0
this✝ : x.order ≠ y.order
g : Γ
hg : g ∈ y.support
hgx : g ≠ x.order
this : x.coeff g = y.coeff g
⊢ ¬y.coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Addition

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

Tactic:
by_cases h : i < c <;> simp [h]

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

Goal state before:
pp: F' : Type u_5
E₁' : Type u_6
E₂' : Type u_7
inst✝⁷ : FunLike F' E₁' E₂'
inst✝⁶ : AddGroup E₁'
inst✝⁵ : LE E₁'
inst✝⁴ : AddRightMono E₁'
inst✝³ : AddGroup E₂'
inst✝² : LE E₂'
inst✝¹ : AddRightMono E₂'
inst✝ : AddMonoidHomClass F' E₁' E₂'
h : ∀ (f : F') (x : E₁'), 0 ≤ x → 0 ≤ f x
f : F'
a b : E₁'
hab : a ≤ b
⊢ f a ≤ f b

Tactic:
simpa using

Goal state after:
F' : Type u_5
E₁' : Type u_6
E₂' : Type u_7
inst✝⁷ : FunLike F' E₁' E₂'
inst✝⁶ : AddGroup E₁'
inst✝⁵ : LE E₁'
inst✝⁴ : AddRightMono E₁'
inst✝³ : AddGroup E₂'
inst✝² : LE E₂'
inst✝¹ : AddRightMono E₂'
inst✝ : AddMonoidHomClass F' E₁' E₂'
h : ∀ (f : F') (x : E₁'), 0 ≤ x → 0 ≤ f x
f : F'
a b : E₁'
hab : a ≤ b
⊢ f a ≤ f b
Module: Mathlib.Algebra.Order.Module.PositiveLinearMap

Goal state before:
pp: case succ
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
n : ℕ
ih : (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y
⊢ ((n + 1) • f.toLinearMap).toFun x ≤ ((n + 1) • f.toLinearMap).toFun y

Tactic:
simpa using

Goal state after:
case succ
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
n : ℕ
ih : (n • f.toLinearMap).toFun x ≤ (n • f.toLinearMap).toFun y
⊢ n • f x + f x ≤ n • f y + f y
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 : 0 ≤ b - a
this : 0 ≤ f (b - a)
⊢ 0 ≤ f.toFun b - f.toFun a

Tactic:
simpa using

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
this : 0 ≤ f (b - a)
⊢ f a ≤ f b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : 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 ≠ ⊤
⊢ (ofLex 0).coeff ((ofLex x).orderTop.untop htop) < (ofLex x).coeff ((ofLex x).orderTop.untop htop)

Tactic:
simpa using

Goal state after:
Γ : 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 ≠ ⊤
⊢ 0 < (ofLex x).leadingCoeff
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 : Γ
hj : j < (ofLex x).orderTop.untop htop
⊢ (ofLex 0).coeff j = (ofLex x).coeff j

Tactic:
simpa using

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 : Γ
hj : j < (ofLex x).orderTop.untop htop
⊢ 0 = (ofLex x).coeff j
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case hg
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ i ∈ (ofLex x).support

Tactic:
simpa using

Goal state after:
case hg
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
⊢ ¬(ofLex x).coeff i = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
g : Γ
hg : g < i
⊢ g ∉ (ofLex x).support

Tactic:
simpa using

Goal state after:
case hx
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
g : Γ
hg : g < i
⊢ (ofLex x).coeff g = 0
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
hne : ofLex x ≠ 0
horder' : (ofLex x).orderTop.untop htop = i
⊢ 0 < (ofLex x).coeff i

Tactic:
simpa using

Goal state after:
case mpr
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
x : Lex R⟦Γ⟧
i : Γ
hj : ∀ j < i, (ofLex 0).coeff j = (ofLex x).coeff j
hi : (ofLex 0).coeff i < (ofLex x).coeff i
horder : (ofLex x).orderTop = ↑i
htop : (ofLex x).orderTop ≠ ⊤
hne : ofLex x ≠ 0
horder' : (ofLex x).orderTop.untop htop = i
⊢ 0 < (ofLex x).coeff i
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
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
⊢ ofLex |x| ≠ 0

Tactic:
simpa using

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : LinearOrder R
inst✝² : AddCommGroup R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Zero Γ
x : Lex R⟦Γ⟧
hne : x ≠ 0
hne' : ofLex x ≠ 0
⊢ ¬x = 0
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a ≤ a * d

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ 1 ≤ d
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * d < b

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * d < b
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 using

Goal state after:
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
⊢ ¬y = 0
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
⊢ x ≠ 0

Tactic:
simpa using

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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
⊢ ¬x = 0
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
⊢ ofLex y ≠ 0

Tactic:
simpa using

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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
⊢ ¬y = 0
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
⊢ (ofLex |x|).orderTop = (ofLex |y|).orderTop

Tactic:
simpa using

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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex y).orderTop
hy : y ≠ 0
hx : x ≠ 0
⊢ (ofLex x).orderTop = (ofLex y).orderTop