mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
⊢ (∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ) ↔ (∃ n, |val b|ₘ ≤ |val a|ₘ ^ n) ∧ ¬∃ n, |val a|ₘ ≤ |val b|ₘ ^ n

Tactic:
suffices (∀ (n : ℕ), |b.val|ₘ ^ n < |a.val|ₘ) → ∃ n, |b.val|ₘ ≤ |a.val|ₘ ^ n by
      simpa using this

Goal state after:
M✝ : Type u_1
inst✝⁴ : Group M✝
inst✝³ : Lattice M✝
M : Type u_2
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b✝ : M
a b : MulArchimedeanOrder M
⊢ (∀ (n : ℕ), |val b|ₘ ^ n < |val a|ₘ) → ∃ n, |val b|ₘ ≤ |val a|ₘ ^ n
Module: Mathlib.Algebra.Order.Chebyshev

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

Tactic:
[

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

Goal state before:
pp: M✝ : Type u_1
inst✝⁷ : Group M✝
inst✝⁶ : Lattice M✝
M : Type u_2
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a✝ b✝ : M
N : Type u_3
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn : |val b|ₘ ≤ |val a|ₘ ^ n
⊢ of (f (val a)) ≤ of (f (val b))

Tactic:
[

Goal state after:
M✝ : Type u_1
inst✝⁷ : Group M✝
inst✝⁶ : Lattice M✝
M : Type u_2
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a✝ b✝ : M
N : Type u_3
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
a b : MulArchimedeanOrder M
n : ℕ
hn : |val b|ₘ ≤ |val a|ₘ ^ n
⊢ of (f (val a)) ≤ of (f (val b))
Module: Mathlib.Algebra.Order.Field.GeomSum

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ 0 ≤ x ^ m / (1 - x)

pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ¬m < n

Tactic:
· apply div_nonneg (pow_nonneg hx _)
      simpa using h'x.le

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
m n : ℕ
hx : 0 ≤ x
h'x : x < 1
hmn : n < m
⊢ ¬m < n
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: case 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ∈ (s.erase x).erase y
⊢ f z • g (σ z) = f z • g (σ ((Equiv.swap x y) z))

Tactic:
[

Goal state after:
case 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✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
x : ι
hx : x ∈ ↑s
y : ι
hy : y ∈ ↑s
hgxy : (g ∘ ⇑σ) x < (g ∘ ⇑σ) y
hfxy : f y < f x
τ : Perm ι := Equiv.trans (Equiv.swap x y) σ
hτs : {x | τ x ≠ x} ⊆ ↑s
hxy : x ≠ y
z : ι
hz : z ∈ (s.erase x).erase y
⊢ f z • g (σ z) = f z • g (σ ((Equiv.swap x y) z))
Module: Mathlib.Algebra.Order.Archimedean.Class

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

Tactic:
apply ((hmono.lt_iff_lt hminmem (by simp)).mp ?_).le
        rw [ih] at hlt
        exact hlt

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

Goal state before:
pp: ι : 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✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Antivary f g
⊢ ∑ i, f i • g i < ∑ i, f (σ i) • g i ↔ ¬Antivary (f ∘ ⇑σ) g

Tactic:
by
  simp [(hfg.antivaryOn _).sum_smul_lt_sum_comp_perm_smul_iff fun _ _ ↦ mem_univ _]

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

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ (orderHom f) (mk a) = (orderHom f) (mk b) → mk a = mk b

Tactic:
[

Goal state after:
case mk.mk
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
f : M →*o N
h : Function.Injective ⇑f
a b : M
⊢ (orderHom f) (mk a) = (orderHom f) (mk b) → mk a = mk b
Module: Mathlib.Algebra.Order.Floor.Div

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
⊢ (b + a - 1) / a = 0

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
a : ℕ
ha : a ≤ 0
b : ℕ
⊢ (b + a - 1) / a = 0
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s < t
⊢ { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ } <
    { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ t}, upper' := ⋯ }

Tactic:
[

Goal state after:
M : Type u_1
inst✝⁵ : CommGroup M
inst✝⁴ : LinearOrder M
inst✝³ : IsOrderedMonoid M
a b : M
N : Type u_2
inst✝² : CommGroup N
inst✝¹ : LinearOrder N
inst✝ : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s < t
⊢ { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ s}, upper' := ⋯ } <
    { carrier := {a | ∀ (h : a ≠ ⊤), ⟨a, h⟩ ∈ t}, upper' := ⋯ }
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), mk a h ∈ s

Tactic:
[

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), mk a h ∈ s
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)

Tactic:
[

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ ↑(Ioc (c - ↑(#s)) c)
⊢ x ∈ (fun x ↦ c - ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.Group.Int.Sum

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

Tactic:
[

Goal state after:
case refine_3
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ ↑(Ico c (c + ↑(#s)))
⊢ x ∈ (fun x ↦ c + ↑x) '' ↑(range #s)
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
m : α
n : β
hm : m ≠ 0
hn : n ≠ 0
⊢ (inl α β) m * (inr α β) n = ↑(toLex (Units.mk0 m hm, Units.mk0 n hn))

Tactic:
by
  rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Icc a b) = Icc (a + c) (b + c)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ico a b) = Ico (a + c) (b + c)

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ico a b) = Ico (a + c) (b + c)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioc a b) = Ioc (a + c) (b + c)
Module: Mathlib.Algebra.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
[

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ mk (k • a) = mk a

Tactic:
[

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ mk (k • a) = mk a
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ (∃ m, |a| ≤ m • |k • a|) ∧ ∃ n, |k • a| ≤ n • |a|

Tactic:
abs_smul

Goal state after:
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
⊢ (∃ m, |a| ≤ m • |k| • |a|) ∧ ∃ n, |k| • |a| ≤ n • |a|
Module: Mathlib.Algebra.Order.Module.Archimedean

Goal state before:
pp: case refine_2
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this✝ : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
this : n • |a| = (n • 1) • |a|
⊢ |k| • |a| ≤ n • |a|

Tactic:
this

Goal state after:
case refine_2
M : Type u_1
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
K : Type u_2
inst✝⁵ : Ring K
inst✝⁴ : LinearOrder K
inst✝³ : IsOrderedRing K
inst✝² : Archimedean K
inst✝¹ : Module K M
inst✝ : PosSMulMono K M
a : M
k : K
h : k ≠ 0
this✝ : Nontrivial K
m : ℕ
hm : 1 ≤ m • |k|
n : ℕ
hn : |k| ≤ n • 1
this : n • |a| = (n • 1) • |a|
⊢ |k| • |a| ≤ (n • 1) • |a|
Module: Mathlib.Data.Set.MulAntidiagonal

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightStrictMono α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
⊢ (s.mulAntidiagonal t a).Finite

Tactic:
by_contra! h
  have h1 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) :=
    fun f ↦ hs fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).1⟩
  have h2 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) :=
    fun f ↦ ht fun n ↦ ⟨_, (mem_mulAntidiagonal.1 (f n).2).2.1⟩
  obtain ⟨g, hg⟩ :=
    h1.exists_monotone_subseq fun n ↦ (h.natEmbedding _ n).2
  obtain ⟨m, n, mn, h2'⟩ := h2 fun n ↦ h.natEmbedding _ _
  refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)
  exact eq_of_fst_le_fst_of_snd_le_snd _ _ _ (hg _ _ mn.le) h2'

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun b ↦ 1 * b) s = s

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun b ↦ 1 * b) s = s
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun x ↦ x * 1) s = s

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s : Interval α
⊢ WithBot.map (fun x ↦ x * 1) s = s
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t s : NonemptyInterval α
⊢ s⁻¹⁻¹.toProd = s.toProd

Tactic:
exact inv_inv _

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1

Tactic:
[

Goal state after:
case coe.coe
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a✝¹ a✝ : NonemptyInterval α
⊢ ↑a✝¹ * ↑a✝ = 1 ↔ ∃ a b, ↑a✝¹ = pure a ∧ ↑a✝ = pure b ∧ a * b = 1
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2) ⊆ Function.support x.coeff

Tactic:
[

Goal state after:
case refine_1
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : PartialOrder Γ'
x : R⟦Γ'⟧⟦Γ⟧
⊢ ((fun x ↦ (ofLex x).1) '' Function.support fun g ↦ (x.coeff g.1).coeff g.2) ⊆ Function.support x.coeff
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h } = 0 ↔ f = 0

Tactic:
[

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h } = 0 ↔ f = 0
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬(⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2)
⊢ ↑⊥ = ⋂ s ∈ S, ↑s

Tactic:
[

Goal state after:
case neg
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
h : ¬(⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2)
⊢ ↑⊥ = ⋂ s ∈ S, ↑s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
f : (i : ι) → κ i → Interval α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
[

Goal state after:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
f : (i : ι) → κ i → Interval α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : (fun a ↦ AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Tactic:
[

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : Rᵃᵒᵖ⟦Γ⟧
⊢ (if h : (fun a ↦ AddOpposite.unop (x.coeff a)) = 0 then ⊤ else ↑(⋯.min ⋯)) = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)
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:
rw [← addOppositeEquiv_orderTop, AddEquiv.apply_symm_apply]

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

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

Tactic:
← addOppositeEquiv_leadingCoeff,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv (addOppositeEquiv.symm x))).leadingCoeff =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
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
⊢ (x + y).orderTop = x.orderTop

Tactic:
by
  have hx : x ≠ 0 := orderTop_ne_top.1 hxy.ne_top
  let g : Γ := Set.IsWF.min x.isWF_support (support_nonempty_iff.2 hx)
  have hcxyne : (x + y).coeff g ≠ 0 := by
    rw [coeff_add, coeff_eq_zero_of_lt_orderTop (lt_of_eq_of_lt (orderTop_of_ne_zero hx).symm hxy),
      add_zero]
    exact coeff_orderTop_ne (orderTop_of_ne_zero hx)
  have hxyx : (x + y).orderTop ≤ x.orderTop := by
    rw [orderTop_of_ne_zero hx]
    exact orderTop_le_of_coeff_ne_zero hcxyne
  exact le_antisymm hxyx (le_of_eq_of_le (min_eq_left_of_lt hxy).symm min_orderTop_le_orderTop_add)

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✝ : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x.orderTop < y.orderTop
hx : x ≠ 0
ho : (x + y).orderTop = x.orderTop
h : ¬x + y = 0
⊢ (x + y).leadingCoeff = x.leadingCoeff

Tactic:
[

Goal state after:
case neg
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 + y).leadingCoeff = x.leadingCoeff
Module: Mathlib.RingTheory.HahnSeries.Addition

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

Tactic:
by
  by_contra h
  simp only [h, order_zero, leadingCoeff_zero, map_zero, add_zero] at hxy
  exact hy hxy.symm

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_7
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s✝ : Finset α
x : α → R⟦Γ⟧
g : Γ
i : α
s : Finset α
his : i ∉ s
hsum : (∑ i ∈ s, x i).coeff g = ∑ i ∈ s, (x i).coeff g
⊢ (∑ i ∈ cons i s his, x i).coeff g = ∑ i ∈ cons i s his, (x i).coeff g

Tactic:
rw [sum_cons, sum_cons, coeff_add, hsum]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ ↑g = min x.orderTop y.orderTop

Tactic:
hxg,

Goal state after:
R : Type u_3
inst✝¹ : AddGroup R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : R⟦Γ⟧
g : Γ
hxg : x.orderTop = ↑g
hyg : y.orderTop = ↑g
hxyc : x.leadingCoeff = y.leadingCoeff
⊢ ↑g = min (↑g) y.orderTop
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : (ofLex a).coeff i = 0 ∧ (ofLex b).coeff i = 0
⊢ i ∉ v

Tactic:
Set.notMem_ofPred_iff,

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrder Γ
inst✝¹ : Zero R
inst✝ : LinearOrder R
a b : Lex R⟦Γ⟧
hab✝ : a ≠ b
hab : ∃ a_1, a.coeff a_1 ≠ b.coeff a_1
u : Set Γ := {i | (ofLex a).coeff i ≠ 0} ∪ {i | (ofLex b).coeff i ≠ 0}
v : Set Γ := {i | (ofLex a).coeff i ≠ (ofLex b).coeff i}
i : Γ
h : (ofLex a).coeff i = 0 ∧ (ofLex b).coeff i = 0
⊢ ¬(ofLex a).coeff i ≠ (ofLex b).coeff i
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 * c = a * c * d

Tactic:
[

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 * c = a * c * d
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
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff

Tactic:
[

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
⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔
    ArchimedeanClass.mk (ofLex x).leadingCoeff ≤ ArchimedeanClass.mk (ofLex y).leadingCoeff