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

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

Tactic:
by
  by_cases hi : IsMax i
  · have : i + 1 = i := by
      have h : i ≤ i + 1 := by
        rw [← Order.succ_eq_add_one]
        apply Order.le_succ
      exact le_antisymm (hi h) h
    simp only [this, left_eq_sup, ge_iff_le, disjointed, sdiff_le_iff]
    apply le_trans (le_partialSups _ _) le_sup_right
  · rw [← Order.succ_eq_add_one, disjointed_succ _ hi]
    simp

Goal state after:
Module: Mathlib.Algebra.Order.Field.Pi

Goal state before:
pp: case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x y : ι → α
h : ∀ (i : ι), x i < y i
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
hxε : ∀ (i : ι), x i + ε i = y i
⊢ ∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i

Tactic:
obtain rfl : x + ε = y := funext hxε

Goal state after:
case intro.inr
α : Type u_1
ι : Type u_2
inst✝⁶ : AddCommMonoid α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedCancelAddMonoid α
inst✝³ : Nontrivial α
inst✝² : DenselyOrdered α
inst✝¹ : ExistsAddOfLE α
inst✝ : Finite ι
x : ι → α
val✝ : Fintype ι
h✝ : Nonempty ι
ε : ι → α
hε : ∀ (i : ι), 0 < ε i
h : ∀ (i : ι), x i < (x + ε) i
hxε : ∀ (i : ι), x i + ε i = (x + ε) i
⊢ ∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : Interval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
cases s
  · simp
  cases t
  · simp
  · simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
      Interval.coe_inj, NonemptyInterval.coe_eq_pure]
    exact NonemptyInterval.mul_eq_one_iff

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : R⟦Γ⟧
i : Γ
hi : ↑i < x.orderTop
⊢ x.coeff i = 0

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)
  · exact coeff_zero
  contrapose! hi
  rw [← mem_support] at hi
  rw [orderTop_of_ne_zero hx, WithTop.coe_lt_coe]
  exact Set.IsWF.not_lt_min _ _ hi

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ leadingCoeff 0 = coeff 0 (order 0)

Tactic:
leadingCoeff_zero,

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ 0 = coeff 0 (order 0)
Module: Mathlib.RingTheory.HahnSeries.Addition

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (x + y)).coeff g = (embDomain f x + embDomain f y).coeff g

Tactic:
simp [embDomain_of_notMem_range hg]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : Zero Γ
f : R⟦Γ⟧
hf : f = 0
⊢ (-f).order = f.order

Tactic:
simp only [hf, neg_zero]

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

Goal state before:
pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
simp [embDomain_of_notMem_range hg]

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

Goal state before:
pp: case inr
Γ : 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}
hvu : v ⊆ u
⊢ a ≤ b ∨ b ≤ a

Tactic:
have hv : v.IsWF :=
        ((ofLex a).isPWO_support'.isWF.union (ofLex b).isPWO_support'.isWF).subset hvu

Goal state after:
case inr
Γ : 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}
hvu : v ⊆ u
hv : v.IsWF
⊢ a ≤ b ∨ b ≤ a
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)
⊢ x = (decompose seed.stratum').symm f'

Tactic:
change x = f'.coeAddMonoidHom _

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.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)
⊢ x = (DirectSum.coeAddMonoidHom seed.stratum') f'
Module: Mathlib.Algebra.Order.Ring.IsNonarchimedean

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f y < f x
h : f (x + y) ≠ f x
⊢ False

Tactic:
have h1 : f (x + y) ≤ f x := (hna x y).trans_eq (max_eq_left_of_lt h_lt)

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
F : Type u_2
α : Type u_3
inst✝² : AddGroup α
inst✝¹ : FunLike F α R
inst✝ : AddGroupSeminormClass F α R
f : F
hna : IsNonarchimedean ⇑f
x y : α
h_lt : f y < f x
h : f (x + y) ≠ f x
h1 : f (x + y) ≤ f x
⊢ False
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x : R
hx : 0 ≤ mk x
⊢ ∃ n, x < ↑n

Tactic:
by
  obtain ⟨n, hn⟩ := exists_nat_gt_of_mk_nonneg hx
  exact ⟨n, mod_cast hn⟩

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
⊢ ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩) = (truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))

Tactic:
ext d

Goal state after:
case refine_2
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
x : ↥seed.baseEmbedding.domain
c : FiniteArchimedeanClass M
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
f' : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i) := DFinsupp.mk f.support fun d ↦ if ↑c ≤ ↑↑d then 0 else f ↑d
d : FiniteArchimedeanClass M
⊢ (ofLex (↑seed.baseEmbedding ⟨f'.sum fun d x ↦ ↑x, ⋯⟩)).coeff d =
    ((truncLTLinearMap K c) (ofLex (↑seed.baseEmbedding x))).coeff d
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
f : Partial seed
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
⊢ ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩) = (single c) ((seed.coeff c) ⟨↑x, hx⟩)

Tactic:
ext d

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
f : Partial seed
x : ↥(↑f).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ seed.stratum c
hx' : ↑x ∈ seed.baseEmbedding.domain
heq : ↑⟨↑x, hx'⟩ = ↑x
fx : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c) := DFinsupp.single c ⟨↑x, hx⟩
hfx : ↑x = fx.sum fun c ↦ ⇑(seed.stratum c).subtype
d : FiniteArchimedeanClass M
⊢ (ofLex (↑seed.baseEmbedding ⟨↑x, hx'⟩)).coeff d = ((single c) ((seed.coeff c) ⟨↑x, hx⟩)).coeff d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ¬x = 0
hx0' : ↑x ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
hx'0 : ⟨x', hx'mem⟩ ≠ 0
heq : ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x
x'' : ↥(↑f).domain := ⟨x', ⋯⟩
hx''mem : ↑x'' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
h0 : (seed.coeff (FiniteArchimedeanClass.mk (↑x) hx0')) ⟨↑x'', hx''mem⟩ ≠ 0
heq' : ArchimedeanClass.mk ↑x'' = ArchimedeanClass.mk ↑x
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x

Tactic:
← orderTop_eq_iff,

Goal state after:
case neg
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : ↥(↑f).domain
hx0 : ¬x = 0
hx0' : ↑x ≠ 0
x' : M
hx'mem : x' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
hx'0 : ⟨x', hx'mem⟩ ≠ 0
heq : ArchimedeanClass.mk x' = ArchimedeanClass.mk ↑x
x'' : ↥(↑f).domain := ⟨x', ⋯⟩
hx''mem : ↑x'' ∈ seed.stratum (FiniteArchimedeanClass.mk (↑x) hx0')
h0 : (seed.coeff (FiniteArchimedeanClass.mk (↑x) hx0')) ⟨↑x'', hx''mem⟩ ≠ 0
heq' : (ofLex (↑↑f x'')).orderTop = (ofLex (↑↑f x)).orderTop
⊢ (withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x
Module: Mathlib.Algebra.Order.Star.Real

Goal state before:
pp: case refine_2
x p : ℝ≥0
⊢ x ≤ x + star p * p

Tactic:
exact le_self_add

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ } = (truncLTLinearMap K c) (ofLex (↑↑f y))

Tactic:
ext d

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ArchimedeanClass.mk (↑y - x) = ↑c
h : ∀ (z : ↥(↑f).domain), ↑z - x ∉ ball K c
d : FiniteArchimedeanClass M
⊢ { coeff := f.evalCoeff x, isPWO_support' := ⋯ }.coeff d = ((truncLTLinearMap K c) (ofLex (↑↑f y))).coeff d
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)

Tactic:
rw [mul_comm]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : UpperSet α
⊢ s * 1 = s

Tactic:
rw [mul_comm]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : UpperSet α
⊢ 1 * s = s
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : LowerSet α
⊢ s * 1 = s

Tactic:
rw [mul_comm]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s✝ t : Set α
a : α
s : LowerSet α
⊢ 1 * s = s
Module: Mathlib.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : IsOrderedMonoid α
s t : Set α
⊢ s * ↑(upperClosure t) = ↑(upperClosure (s * t))

Tactic:
by
  simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul,
    UpperSet.coe_iInf₂]
  rfl

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

Goal state before:
pp: case pos
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ (truncLTLinearMap K c) (ofLex (↑↑f y)) = (truncLTLinearMap K c) (ofLex (f.eval x))

Tactic:
ext d

Goal state after:
case pos
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
⊢ ((truncLTLinearMap K c) (ofLex (↑↑f y))).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case neg
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ ofLex (f.eval x) = (truncLTLinearMap K c) (ofLex (f.eval x))

Tactic:
ext d

Goal state after:
case neg
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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
d : FiniteArchimedeanClass M
⊢ (ofLex (f.eval x)).coeff d = ((truncLTLinearMap K c) (ofLex (f.eval x))).coeff d
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.eraseLead.natDegree < n

Tactic:
refine p.eraseLead_natDegree_le.trans_lt ?_

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ p.natDegree - 1 < n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : R[X]
m n : ℕ
hq : q.IsMonicOfDegree n
hpq : (p * q).IsMonicOfDegree (m + n)
⊢ p.IsMonicOfDegree m

Tactic:
rcases subsingleton_or_nontrivial R with H | H
  · simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero_iff] at hpq ⊢
    exact hpq.1
  have h₂ : p.Monic := hq.monic.of_mul_monic_right hpq.monic
  refine ⟨?_, h₂⟩
  have := hpq.natDegree_eq
  have h : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
    rw [h₂.leadingCoeff, hq.leadingCoeff_eq, one_mul]
    exact one_ne_zero
  rw [natDegree_mul' h, hq.natDegree_eq] at this
  exact (Nat.add_right_cancel this.symm).symm

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ (q * b).IsMonicOfDegree (m - n + n)

Tactic:
rw [← hq, show m - n + n = m by lia]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ (a + r).IsMonicOfDegree m
Module: Mathlib.Algebra.Polynomial.Eval.Irreducible

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ b.leadingCoeff * ?refine_2.b = 1

Tactic:
rw [mul_comm]

Goal state after:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ ?h.b * b.leadingCoeff = 1

case h.b
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
h_mon : f.leadingCoeff = 1
h_irr : Irreducible (map φ f)
a b : R[X]
h : f = a * b
q : a.leadingCoeff * b.leadingCoeff = 1
⊢ R
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]
    by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree
    · rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]
      grw [h2, add_tsub_cancel_left]
    · rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp),

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ p.natTrailingDegree + p.mirror.natTrailingDegree = 2 * p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ((monomial m) r).homogenize n = (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

Tactic:
rw [homogenize, Finset.sum_eq_single (a := (m, n - m))]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) =
    (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

case h₀
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case isUnit_or_isUnit.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
· exact Or.inl (h3 g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : P = 0
⊢ P.eraseLead.signVariations ≤ P.signVariations

Tactic:
simp [hpz]

Goal state after:
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
hpz : P = 0
⊢ P.signVariations ≤ P.eraseLead.signVariations + 1

Tactic:
simp [hpz]

Goal state after: