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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
f✝ : ι →₀ β
a✝ a : α
ha : a ≤ 0
f : ι →₀ β
i : ι
⊢ (mapRange (fun x ↦ x ⌈/⌉ a) ⋯ f) i = 0 i

Tactic:
exact ceilDiv_of_nonpos ha _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 < a

Tactic:
by norm_num at ha ⊢; exact ha

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a : K
ha : 2⁻¹ ≤ a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 ≤ a

Tactic:
by norm_num at ha ⊢; exact ha

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : M₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : M₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero M₀
inst✝² : GroupWithZero N₀
inst✝¹ : Preorder N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : M₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
⊢ 0 ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inl.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
y : N₀ˣ
⊢ 0 ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) 0 ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inl
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x : N₀ˣ
⊢ ↑x ≤ 0 → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) 0

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case inr.inr
M₀ : Type u_1
N₀ : Type u_2
inst✝³ : GroupWithZero M₀
inst✝² : Preorder M₀
inst✝¹ : LinearOrderedCommGroupWithZero N₀
inst✝ : DecidablePred fun x ↦ x = 0
x y : N₀ˣ
⊢ ↑x ≤ ↑y → (ofClass WithZero.withZeroUnitsEquiv.symm) ↑x ≤ (ofClass WithZero.withZeroUnitsEquiv.symm) ↑y

Tactic:
simp [WithZero.withZeroUnitsEquiv]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
⊢ ↑(if h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2 then
        ↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ }
      else ⊥) =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
h : s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2
⊢ ↑↑{ fst := s.toProd.1 ⊔ t.toProd.1, snd := s.toProd.2 ⊓ t.toProd.2, fst_le_snd := ⋯ } =
    Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)

case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : DecidableLE α
s t : NonemptyInterval α
h : ¬(s.toProd.1 ≤ t.toProd.2 ∧ t.toProd.1 ≤ s.toProd.2)
⊢ ↑⊥ = Icc (s.toProd.1 ⊔ t.toProd.1) (s.toProd.2 ⊓ t.toProd.2)
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
⊢ s ≤
    if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
h : x✝ ⊆ {⊥}
⊢ s ≤ ⊥

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ x✝
h : ¬x✝ ⊆ {⊥}
⊢ s ≤ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
⊢ (if h : x✝ ⊆ {⊥} then ⊥
    else ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ }) ≤
    s

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : x✝ ⊆ {⊥}
⊢ ⊥ ≤ s

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
x✝ : Set (Interval α)
s : Interval α
ha : s ∈ upperBounds x✝
h : ¬x✝ ⊆ {⊥}
⊢ ↑{ fst := ⨅ s, ⨅ (_ : ↑s ∈ x✝), s.toProd.1, snd := ⨆ s, ⨆ (_ : ↑s ∈ x✝), s.toProd.2, fst_le_snd := ⋯ } ≤ s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
⊢ (if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥) ≤
    s

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ } ≤ s

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : Interval α
ha : s ∈ s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ⊥ ≤ s
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: case right.coe
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : ↑s ∈ lowerBounds s₁
⊢ ↑s ≤
    if h :
        ⊥ ∉ s₁ ∧
          ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2 then
      ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }
    else ⊥

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : ↑s ∈ lowerBounds s₁
h : ⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2
⊢ ↑s ≤ ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ s₁), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ s₁), s.toProd.2, fst_le_snd := ⋯ }

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
s₁ : Set (Interval α)
s : NonemptyInterval α
ha : ↑s ∈ lowerBounds s₁
h : ¬(⊥ ∉ s₁ ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ s₁ → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ s₁ → s.toProd.1 ≤ t.toProd.2)
⊢ ↑s ≤ ⊥
Module: Mathlib.Order.Interval.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : DecidableLE α
S : Set (Interval α)
⊢ ↑(if h :
          ⊥ ∉ S ∧ ∀ ⦃s : NonemptyInterval α⦄, ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.toProd.1 ≤ t.toProd.2 then
        ↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2, fst_le_snd := ⋯ }
      else ⊥) =
    ⋂ s ∈ S, ↑s

Tactic:
split_ifs with h

Goal state after:
case pos
α : 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
⊢ ↑↑{ fst := ⨆ s, ⨆ (_ : ↑s ∈ S), s.toProd.1, snd := ⨅ s, ⨅ (_ : ↑s ∈ S), s.toProd.2, fst_le_snd := ⋯ } = ⋂ s ∈ S, ↑s

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.RingTheory.HahnSeries.Basic

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
⊢ ((single a) r).coeff b = if b = a then r else 0

Tactic:
split_ifs with h

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
h : b = a
⊢ ((single a) r).coeff b = r

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
h : ¬b = a
⊢ ((single a) r).coeff b = 0
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:
by rw [hxg, hyg, inf_idem]

Goal state after:
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 ∈ (ofLex x).support
⊢ i ≤ g

Tactic:
contrapose! hg

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
⊢ g ∉ (ofLex x).support
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ↑(ofLex ((finiteArchimedeanClassOrderIsoLex Γ R) (FiniteArchimedeanClass.mk x h))).1 = (ofLex x).orderTop

Tactic:
simp [finiteArchimedeanClassOrderIsoLex, finiteArchimedeanClassOrderHomLex]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ↑(ofLex ((finiteArchimedeanClassOrderIsoLex Γ R) (FiniteArchimedeanClass.mk x h))).2 =
    ArchimedeanClass.mk (ofLex x).leadingCoeff

Tactic:
simp [finiteArchimedeanClassOrderIsoLex, finiteArchimedeanClassOrderHomLex]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj : ∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : (embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i
⊢ i ∈ Set.range ⇑f

Tactic:
contrapose hi

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : PartialOrder R
Γ' : Type u_3
inst✝¹ : LinearOrder Γ'
f : Γ ↪o Γ'
inst✝ : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj : ∀ j < i, (embDomain f (ofLex a)).coeff j = (embDomain f (ofLex b)).coeff j
hi : i ∉ Set.range ⇑f
⊢ ¬(embDomain f (ofLex a)).coeff i < (embDomain f (ofLex b)).coeff i
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
hy : mk y₁ ≤ mk y₂
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
⊢ mk (x₁ * y₁) ≤ mk (x₂ * y₂)

Tactic:
obtain ⟨n, hn⟩ := hy

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ mk (x₁ * y₁) ≤ mk (x₂ * y₂)
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of (x₂ * y₂))| =
    |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| * |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)|

Tactic:
ArchimedeanOrder.val_of,

Goal state after:
case e'_3
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ |x₂ * y₂| = |x₂| * |y₂|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • |ArchimedeanOrder.val (ArchimedeanOrder.of (x₁ * y₁))| =
    m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)| * n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|

Tactic:
ArchimedeanOrder.val_of,

Goal state after:
case e'_4
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x₁ y₁ x₂ y₂ : R
m : ℕ
hm : |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| ≤ m • |ArchimedeanOrder.val (ArchimedeanOrder.of x₁)|
n : ℕ
hn : |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)| ≤ n • |ArchimedeanOrder.val (ArchimedeanOrder.of y₁)|
⊢ (m * n) • |x₁ * y₁| = m • |x₁| * n • |y₁|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : CommRing R
inst✝⁴ : IsStrictOrderedRing R
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
f : S →+*o R
x : R
y : S
⊢ mk x ≤ mk (f y) + mk x

Tactic:
exact mk_le_mk_add_of_archimedean f x y

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
x : M
c : FiniteArchimedeanClass M
hx : x ∈ seed.stratum c
⊢ x ∈ (↑f).domain

Tactic:
apply Set.mem_of_subset_of_mem f.prop.baseEmbedding_le.1
  apply seed.mem_domain_baseEmbedding hx

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f x * embDomain f y).coeff g = 0

Tactic:
contrapose! hg

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝⁶ : AddCommMonoid Γ
inst✝⁵ : PartialOrder Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
Γ' : Type u_6
inst✝³ : AddCommMonoid Γ'
inst✝² : PartialOrder Γ'
inst✝¹ : IsOrderedCancelAddMonoid Γ'
inst✝ : NonUnitalNonAssocSemiring R
f : Γ ↪o Γ'
hf : ∀ (x y : Γ), f (x + y) = f x + f y
x y : R⟦Γ⟧
g : Γ'
hg : (embDomain f x * embDomain f y).coeff g ≠ 0
⊢ g ∈ Set.range ⇑f
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a : ↥A
h : A.valuation ↑a = 1
ha : ↑a ≠ 0
⊢ (↑a)⁻¹ ∈ A

Tactic:
rw [← valuation_le_one_iff, map_inv₀, h, inv_one]

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
⊢ f.evalCoeff x (FiniteArchimedeanClass.mk (↑y - x) hxy0) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)

Tactic:
f.evalCoeff_eq hz

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
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
y : ↥(↑f).domain
h : x < ↑y
hxy0 : ↑y - x ≠ 0
z : ↥(↑f).domain
hz : ↑z - x ∈ ball K (FiniteArchimedeanClass.mk (↑y - x) ⋯)
⊢ (ofLex (↑↑f z)).coeff (FiniteArchimedeanClass.mk (↑y - x) ⋯) <
    (ofLex (↑↑f y)).coeff (FiniteArchimedeanClass.mk (↑y - x) hxy0)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk.mk.inl
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h✝ : mk x ≤ mk y
z : FiniteElement K
h : x ≤ y
⊢ mk x + mk z ≤ mk y + mk z

Tactic:
exact mk.monotone' <| add_le_add_left h _

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

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
obtain hx | hx := eq_or_ne (mk x) 0

Goal state after:
case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

case inr
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x ≠ 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
hx : mk x = 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
unfold stdPart
    have hx' : 0 ≤ mk x⁻¹ := by simp_all
    rw [dif_pos hx.ge, dif_pos hx']
    · apply eq_inv_of_mul_eq_one_left
      suffices FiniteElement.mk x⁻¹ hx' * .mk x hx.ge = 1 by
        rw [← map_mul, this, map_one]
      ext
      apply inv_mul_cancel₀
      aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (map C p) = eval y p

Tactic:
by
  rw [evalEval, eval_map_apply, eval_C]

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
⊢ 0 < ↑f ⟨↑(y - x), hf⟩

Tactic:
have hmono : StrictMono f := hf'.symm ▸ f'.prop.strictMono

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
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x y : ↥(sSupFun hc).domain
h : x < y
hyx : ↑(y - x) ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c
hf : ↑(y - x) ∈ f.domain
this : ↑(sSupFun hc) (y - x) = ↑f ⟨↑(y - x), hf⟩
f' : Partial seed
left✝ : f' ∈ c
hf' : ↑f' = f
hmono : StrictMono ↑f
⊢ 0 < ↑f ⟨↑(y - x), hf⟩
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
⊢ IsMonicOfDegree 1 n

Tactic:
H,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Subsingleton R
p : R[X]
n : ℕ
H : n = 0
⊢ IsMonicOfDegree 1 0
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
⊢ (ofFn n) ((toFn n) p) = p

Tactic:
ext i
  by_cases! h : i < n
  · simp [h, toFn]
  · have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by lia
    simp [*]

Goal state after: