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

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

Tactic:
·

Goal state after:
case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hgt : 0 < x
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.inr
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
hgt : 0 < x
hgt' : 0 < (ofLex x).leadingCoeff
⊢ (ofLex |x|).leadingCoeff = |(ofLex x).leadingCoeff|

Tactic:
rw [abs_eq_self.mpr hgt.le, abs_eq_self.mpr hgt'.le]

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c

Tactic:
·

Goal state after:
case mpr
M : Type u_1
inst✝⁴ : CancelCommMonoid M
inst✝³ : LinearOrder M
inst✝² : IsOrderedMonoid M
inst✝¹ : LocallyFiniteOrder M
inst✝ : ExistsMulOfLE M
a b c x : M
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case 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 |y|).orderTop < (ofLex |x|).orderTop
⊢ ∀ j < (ofLex |y|).orderTop.untop ⋯, (ofLex |x|).coeff j = (ofLex |y|).coeff j

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

Goal state after:
case 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 |y|).orderTop < (ofLex |x|).orderTop
⊢ ∀ j < (ofLex |y|).orderTop.untop ⋯, (ofLex |x|).coeff j = (ofLex |y|).coeff j
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:
·

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
⊢ (ofLex |x|).coeff ((ofLex |y|).orderTop.untop ⋯) < (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯)
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case 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
a b : G
this :
  ∀ (a b : G),
    a ≤ b →
      ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) =
        ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
hab : ¬a ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

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
a b : G
hab : a ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
·

Goal state after:
case 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
a b : G
this :
  ∀ (a b : G),
    a ≤ b →
      ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) =
        ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
hab : ¬a ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex 0).orderTop
⊢ (∃ n, |0| ≤ n • |x|) ↔ ∃ n, |(ofLex 0).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

pp: case inr
Γ : 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
⊢ (∃ n, |y| ≤ n • |x|) ↔ ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

Tactic:
·

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⟦Γ⟧
h : (ofLex x).orderTop = (ofLex 0).orderTop
⊢ (∃ n, |0| ≤ n • |x|) ↔ ∃ n, |(ofLex 0).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inl.inl
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
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

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
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

pp: case inr.inl
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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

pp: case inr.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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
·

Goal state after:
case inl.inl
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
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp
Γ : 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, |y| ≤ n • |x|) → ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|

pp: case inr.mpr
Γ : 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, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|) → ∃ n, |y| ≤ n • |x|

Tactic:
·

Goal state after:
case inr.mp
Γ : 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, |y| ≤ n • |x|) → ∃ n, |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
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
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

pp: case inr.inl
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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

pp: case inr.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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
·

Goal state after:
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
a b : G
hab : a ≤ b
ha : 0 ≤ a
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.inl
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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

pp: case inr.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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
·

Goal state after:
case inr.inl
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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : 0 ≤ b
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.inl.inl
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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : 0 ≤ b
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))

pp: case inr.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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : b ≤ 0
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))

Tactic:
·

Goal state after:
case inr.inl.inl
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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : 0 ≤ b
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : b ≤ 0
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))

Tactic:
·

Goal state after:
case inr.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
a : G
ha : a ≤ 0
b : G
hab : a ≤ b - a
hb : 0 ≤ b - a
hb' : b ≤ 0
⊢ ↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))) = -↑(#(Ico 0 (-a))) + ↑(#(Ico 0 (b - a)))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inr.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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))

Tactic:
·

Goal state after:
case inr.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
a b : G
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ ↑(#(Ico 0 (a + b))) - ↑(#(Ico 0 (-(a + b)))) = ↑(#(Ico 0 a)) - ↑(#(Ico 0 (-a))) + (↑(#(Ico 0 b)) - ↑(#(Ico 0 (-b))))
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case h.mp
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ 0 ≤ x ∧ x < ↑b → x = 0

pp: case h.mpr
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ x = 0 → 0 ≤ x ∧ x < ↑b

Tactic:
·

Goal state after:
case h.mp
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ 0 ≤ x ∧ x < ↑b → x = 0
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case h.mp
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this✝ : 0 ≤ ↑b
x : G
h₁ : 0 ≤ x
h₂ : x < ↑b
hx' : ¬x = 0
this : 0 ≤ ↑b ∧ ↑b ≤ a
⊢ False

Tactic:
exact hb.2 (c := ⟨x, by simpa [h₁] using! h₂.le.trans this.2⟩)
      (lt_of_le_of_ne h₁ (by simpa using! Ne.symm hx')) h₂

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

Goal state before:
pp: case h.mpr
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ x = 0 → 0 ≤ x ∧ x < ↑b

Tactic:
·

Goal state after:
case h.mpr
G : Type u_2
inst✝⁴ : AddCommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : LocallyFiniteOrder G
inst✝ : Nontrivial G
a : G
ha : 0 < a
b : ↥(Icc 0 a)
hb : ⟨0, ⋯⟩ ⋖ b
this : 0 ≤ ↑b
x : G
⊢ x = 0 → 0 ≤ x ∧ x < ↑b
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case inl
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
inst✝ : Nontrivial G
a b : G
hb : 0 ≤ b
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b

pp: case 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
inst✝ : Nontrivial G
a b : G
hb : b ≤ 0
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b

Tactic:
·

Goal state after:
case inl
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
inst✝ : Nontrivial G
a b : G
hb : 0 ≤ b
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b
Module: Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Goal state before:
pp: case 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
inst✝ : Nontrivial G
a b : G
hb : b ≤ 0
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b

Tactic:
·

Goal state after:
case 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
inst✝ : Nontrivial G
a b : G
hb : b ≤ 0
⊢ 0 ≤ (orderAddMonoidHom G) b ↔ 0 ≤ b
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case inr.mp.inl
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjlt : ↑j < (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

pp: case inr.mp.inr.inl
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjeq : ↑j = (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

pp: case inr.mp.inr.inr
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjgt : (ofLex |x|).orderTop < ↑j
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

Tactic:
·

Goal state after:
case inr.mp.inl
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjlt : ↑j < (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Units

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
inst✝¹ : LE M
inst✝ : MulLeftMono M
u : Mˣ
a : M
⊢ 1 ≤ ↑u⁻¹ * a ↔ ↑u ≤ a

Tactic:
by
  rw [u.le_inv_mul_iff, mul_one]

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

Goal state before:
pp: case inr.mp.inr.inl
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjeq : ↑j = (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

pp: case inr.mp.inr.inr
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjgt : (ofLex |x|).orderTop < ↑j
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)

Tactic:
·

Goal state after:
case inr.mp.inr.inl
Γ : 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|
hn' : |y| < (n + 1) • |x|
j : Γ
hj : ∀ j_1 < j, (ofLex |y|).coeff j_1 = (n + 1) • (ofLex |x|).coeff j_1
hi : (ofLex |y|).coeff j < (n + 1) • (ofLex |x|).coeff j
hjeq : ↑j = (ofLex |x|).orderTop
⊢ (ofLex |y|).coeff ((ofLex |x|).orderTop.untop ⋯) ≤ (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)