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

Goal state before:
pp: case e'_3
Γ : 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 |x|).orderTop.untop ⋯ = j

pp: case e'_4
Γ : 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 |x|).orderTop.untop ⋯ = j

Tactic:
<;>

Goal state after:
case e'_3
Γ : 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 |x|).orderTop.untop ⋯ = j

case e'_4
Γ : 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 |x|).orderTop.untop ⋯ = j
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case e'_3
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop = (ofLex |y|).orderTop

pp: case e'_4
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop.untop ⋯ = (ofLex |x|).orderTop.untop ⋯

Tactic:
<;>

Goal state after:
case e'_3
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop = (ofLex |y|).orderTop

case e'_4
Γ : 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 : |(ofLex y).leadingCoeff| ≤ n • |(ofLex x).leadingCoeff|
this : (ofLex |y|).coeff ((ofLex |y|).orderTop.untop ⋯) < (n + 1) • (ofLex |x|).coeff ((ofLex |x|).orderTop.untop ⋯)
⊢ (ofLex x).orderTop.untop ⋯ = (ofLex |x|).orderTop.untop ⋯
Module: Mathlib.Algebra.Order.Quantale

Goal state before:
pp: α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
⊢ (x ⊔ y) * z = x * z ⊔ y * z

Tactic:
by
  rw [← (@iSup_pair _ _ _ (fun _? => _? * z) _ _), ← sSup_pair, sSup_mul_distrib]

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 (Γ × FiniteArchimedeanClass R)
a : { a // a ≠ 0 }
⊢ toLex ((single (ofLex x).1) ↑a) ≠ 0

Tactic:
simpa using! a.prop

Goal state after:
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
a b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
ac : FiniteArchimedeanClass R
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
h✝ : toLex (ao, ac) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, ac))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, ac)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))

Tactic:
induction ac using FiniteArchimedeanClass.ind with | mk a ha
       =>  _ 

Goal state after:
case inl.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a✝ b : Lex (Γ × FiniteArchimedeanClass R)
x✝¹ : Γ × FiniteArchimedeanClass R
ao : Γ
x✝ : Γ × FiniteArchimedeanClass R
bo : Γ
bc : FiniteArchimedeanClass R
a : R
ha : a ≠ 0
h✝ : toLex (ao, FiniteArchimedeanClass.mk a ha) ≤ toLex (bo, bc)
h : (ofLex (toLex (ao, FiniteArchimedeanClass.mk a ha))).1 < (ofLex (toLex (bo, bc))).1
⊢ (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (ao, FiniteArchimedeanClass.mk a ha)) ≤
    (fun x ↦
        (FiniteArchimedeanClass.liftOrderHom (fun a ↦ FiniteArchimedeanClass.mk (toLex ((single (ofLex x).1) ↑a)) ⋯) ⋯)
          (ofLex x).2)
      (toLex (bo, bc))
Module: Mathlib.RingTheory.HahnSeries.Lex

Goal state before:
pp: case h₂
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
x : FiniteArchimedeanClass (Lex R⟦Γ⟧)
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R)) x) = ↑(OrderHom.id x)

Tactic:
induction x using FiniteArchimedeanClass.ind with | mk a ha

Goal state after:
case h₂.mk
Γ : Type u_1
R : Type u_2
inst✝³ : LinearOrder Γ
inst✝² : LinearOrder R
inst✝¹ : AddCommGroup R
inst✝ : IsOrderedAddMonoid R
a : Lex R⟦Γ⟧
ha : a ≠ 0
⊢ ↑(((finiteArchimedeanClassOrderHomInvLex Γ R).comp (finiteArchimedeanClassOrderHomLex Γ R))
        (FiniteArchimedeanClass.mk a ha)) =
    ↑(OrderHom.id (FiniteArchimedeanClass.mk a ha))
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
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk 0) =
    (ofLex 0).orderTop

pp: case inr
Γ : Type u_1
R : Type u_2
inst✝⁵ : LinearOrder Γ
inst✝⁴ : LinearOrder R
inst✝³ : AddCommGroup R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk x) =
    (ofLex x).orderTop

Tactic:
<;>

Goal state after:
case inl
Γ : Type u_1
R : Type u_2
inst✝⁵ : LinearOrder Γ
inst✝⁴ : LinearOrder R
inst✝³ : AddCommGroup R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk 0) =
    (ofLex 0).orderTop

case inr
Γ : Type u_1
R : Type u_2
inst✝⁵ : LinearOrder Γ
inst✝⁴ : LinearOrder R
inst✝³ : AddCommGroup R
inst✝² : IsOrderedAddMonoid R
inst✝¹ : Archimedean R
inst✝ : Nontrivial R
x : Lex R⟦Γ⟧
h : x ≠ 0
⊢ ((FiniteArchimedeanClass.withTopOrderIso (Lex R⟦Γ⟧)).symm.trans (finiteArchimedeanClassOrderIso Γ R).withTopCongr)
      (ArchimedeanClass.mk x) =
    (ofLex x).orderTop
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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j ∈ f.support
⊢ f.support.min' hsupport ≤ j

Tactic:
← Subtype.coe_le_coe,

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.baseEmbedding.domain
hx : 0 < x
hmem : ↑x ∈ seed.baseDomain
f : Π₀ (i : FiniteArchimedeanClass M), ↥(seed.stratum i)
hf : (f.sum fun x xi ↦ ↑xi) = ↑x
hfpos : 0 < f.sum fun x x_1 ↦ ↑x_1
hsupport : f.support.Nonempty
j : FiniteArchimedeanClass M
hj : j ∈ f.support
⊢ ↑(f.support.min' hsupport) ≤ ↑j
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✝³ : NonAssocSemiring α
inst✝² : FunLike F α R
inst✝¹ : ZeroHomClass F α R
inst✝ : NonnegHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
n : ℕ
a : α
⊢ f (↑n * a) ≤ f a

Tactic:
rw [← nsmul_eq_mul]
  exact nsmul_le hna

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : ℕ
⊢ f ↑↑a ≤ 1

pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : ℕ
⊢ f ↑(-↑a) ≤ 1

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : ℕ
⊢ f ↑↑a ≤ 1

case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
F : Type u_2
α : Type u_3
inst✝³ : AddGroupWithOne α
inst✝² : FunLike F α R
inst✝¹ : AddGroupSeminormClass F α R
inst✝ : OneHomClass F α R
f : F
hna : IsNonarchimedean ⇑f
a : ℕ
⊢ f ↑(-↑a) ≤ 1
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₂)|

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

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₁)|
⊢ |ArchimedeanOrder.val (ArchimedeanOrder.of (x₂ * y₂))| =
    |ArchimedeanOrder.val (ArchimedeanOrder.of x₂)| * |ArchimedeanOrder.val (ArchimedeanOrder.of y₂)|

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₁)|
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.inl
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
⊢ mk 0 = 0 ∨ mk 0 = ⊤

pp: case mk.inr
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
x : S
h : x ≠ 0
⊢ mk x = 0 ∨ mk x = ⊤

Tactic:
<;>

Goal state after:
case mk.inl
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
⊢ mk 0 = 0 ∨ mk 0 = ⊤

case mk.inr
S : Type u_3
inst✝³ : LinearOrder S
inst✝² : CommRing S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
x : S
h : x ≠ 0
⊢ mk x = 0 ∨ mk x = ⊤
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
⊢ mk (x ^ ↑n) = mk (y ^ ↑n)

pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
⊢ mk (x ^ (-↑n)) = mk (y ^ (-↑n))

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
⊢ mk (x ^ ↑n) = mk (y ^ ↑n)

case inr
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : Field R
inst✝ : IsOrderedRing R
x y : R
h : mk x = mk y
n : ℕ
⊢ mk (x ^ (-↑n)) = mk (y ^ (-↑n))
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ (x * y * z).coeff b = (x * (y * z)).coeff b

Tactic:
rw [coeff_mul_left' (x.isPWO_support.add y.isPWO_support) support_mul_subset,
    coeff_mul_right' (y.isPWO_support.add z.isPWO_support) support_mul_subset]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
⊢ ∑ ij ∈ antidiagonal ⋯ ⋯ b, (x * y).coeff ij.1 * z.coeff ij.2 =
    ∑ ij ∈ antidiagonal ⋯ ⋯ b, x.coeff ij.1 * (y * z).coeff ij.2
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
inst✝² : Zero Γ
inst✝¹ : AddCommGroup R
inst✝ : One R
g : Γ
hg : 0 < g
r : R
hr : r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
inst✝² : Zero Γ
inst✝¹ : AddCommGroup R
inst✝ : One R
g : Γ
hg : 0 < g
r : R
hr : ¬r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop

Tactic:
<;>

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
inst✝² : Zero Γ
inst✝¹ : AddCommGroup R
inst✝ : One R
g : Γ
hg : 0 < g
r : R
hr : r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
inst✝² : Zero Γ
inst✝¹ : AddCommGroup R
inst✝ : One R
g : Γ
hg : 0 < g
r : R
hr : ¬r = 0
⊢ 0 < (1 + (single g) r - 1).orderTop
Module: Mathlib.Order.Quotient

Goal state before:
pp: case refine_1
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂

pp: case refine_2
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂

case refine_2
α : Type u_1
s : Setoid α
inst✝ : LE α
x₁ x₂ y₁ y₂ : α
hx : x₁ ≈ y₁
hy : x₂ ≈ y₂
⊢ Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) y₁ y₂ → Relation.TransGen (fun x y ↦ x ≤ y ∨ x ≈ y) x₁ x₂
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ 0 ∈ P

pp: case sq_add
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x x✝ s✝ : R
hx✝ : IsSquare x✝
hs✝ : IsSumSq s✝
a✝ : s✝ ∈ P
⊢ x✝ + s✝ ∈ P

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x : R
⊢ 0 ∈ P

case sq_add
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
x x✝ s✝ : R
hx✝ : IsSquare x✝
hs✝ : IsSumSq s✝
a✝ : s✝ ∈ P
⊢ x✝ + s✝ ∈ P
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₂ : y ≤ z ∨ y ≈ z
h✝ : x ≤ y
⊢ x ≤ z ∨ x ≈ z

pp: case inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₂ : y ≤ z ∨ y ≈ z
h✝ : x ≈ y
⊢ x ≤ z ∨ x ≈ z

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₂ : y ≤ z ∨ y ≈ z
h✝ : x ≤ y
⊢ x ≤ z ∨ x ≈ z

case inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h₂ : y ≤ z ∨ y ≈ z
h✝ : x ≈ y
⊢ x ≤ z ∨ x ≈ z
Module: Mathlib.Order.Quotient

Goal state before:
pp: case inl.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≤ y
h✝ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

pp: case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≤ y
h✝ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

pp: case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≈ y
h✝ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

pp: case inr.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≈ y
h✝ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≤ y
h✝ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

case inl.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≤ y
h✝ : y ≈ z
⊢ x ≤ z ∨ x ≈ z

case inr.inl
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≈ y
h✝ : y ≤ z
⊢ x ≤ z ∨ x ≈ z

case inr.inr
α : Type u_1
s : Setoid α
inst✝ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
x y z : α
h✝¹ : x ≈ y
h✝ : y ≈ z
⊢ x ≤ z ∨ x ≈ z
Module: Mathlib.Algebra.Order.Ring.Ordering.Basic

Goal state before:
pp: case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
h✝ : x ∈ P
⊢ False

pp: case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
h✝ : -x ∈ P
⊢ False

Tactic:
<;>

Goal state after:
case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
h✝ : x ∈ P
⊢ False

case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : RingPreordering R
h : ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P
this✝⁴ : HasMemOrNegMem P
x y : R
x✝ : x * y ∈ P.support
this✝³ : ¬(x ∈ P.support ∨ y ∈ P.support)
this✝² : -(-x * y) ∈ P → -x ∈ P ∨ y ∈ P
this✝¹ : -(-x * -y) ∈ P → -x ∈ P ∨ -y ∈ P
this✝ : -(x * y) ∈ P → x ∈ P ∨ y ∈ P
this : -(x * -y) ∈ P → x ∈ P ∨ -y ∈ P
h✝ : -x ∈ P
⊢ False
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
a : Γ
h : a = 0
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a

pp: case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
a : Γ
h : ¬a = 0
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a

Tactic:
<;>

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
a : Γ
h : a = 0
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonAssocSemiring R
x y : R
a : Γ
h : ¬a = 0
⊢ ((single 0) (x + y)).coeff a = ((single 0) x + (single 0) y).coeff a