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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : ¬b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

pp: case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝ * b) = unbotD 0 ↑a✝ * unbotD 0 b

Tactic:
·

Goal state after:
case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 (↑a✝ * ⊥) = unbotD 0 ↑a✝ * unbotD 0 ⊥

pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ unbotD 0 (↑a✝¹ * ↑a✝) = unbotD 0 ↑a✝¹ * unbotD 0 ↑a✝

Tactic:
·

Goal state after:
case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 (↑a✝ * ⊥) = unbotD 0 ↑a✝ * unbotD 0 ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 (↑a✝ * ⊥) = unbotD 0 ↑a✝ * unbotD 0 ⊥

Tactic:
mul_bot ha,

Goal state after:
case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ unbotD 0 ⊥ = unbotD 0 ↑a✝ * unbotD 0 ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ 0 * a ≤ 0 * b

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x * a ≤ x * b

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ 0 * a ≤ 0 * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
⊢ ↑x * a ≤ ↑x * b

Tactic:
·

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ↑x * ⊥ ≤ ↑x * b

pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ b
⊢ ↑x * ↑a✝ ≤ ↑x * b

Tactic:
·

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ↑x * ⊥ ≤ ↑x * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ ⊥
⊢ ↑x * ↑a✝ ≤ ↑x * ⊥

pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ↑x * ↑a✝¹ ≤ ↑x * ↑a✝

Tactic:
·

Goal state after:
case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ ⊥
⊢ ↑x * ↑a✝ ≤ ↑x * ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ a * 0 ≤ b * 0

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ a * x ≤ b * x

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ a * 0 ≤ b * 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
⊢ a * ↑x ≤ b * ↑x

Tactic:
·

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x ≠ ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x

pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ b
⊢ ↑a✝ * ↑x ≤ b * ↑x

Tactic:
·

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
b : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ⊥ ≤ b
⊢ ⊥ * ↑x ≤ b * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ ⊥
⊢ ↑a✝ * ↑x ≤ ⊥ * ↑x

pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑a✝¹ ≤ ↑a✝
⊢ ↑a✝¹ * ↑x ≤ ↑a✝ * ↑x

Tactic:
·

Goal state after:
case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑a✝ ≤ ⊥
⊢ ↑a✝ * ↑x ≤ ⊥ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ ↑x * a < ↑x * ⊥

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ ↑x * a < ↑x * ↑a✝

Tactic:
·

Goal state after:
case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ ↑x * a < ↑x * ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ↑x * ⊥ < ↑x * ↑a✝

pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑x * ↑a✝ < ↑x * ↑a✝¹

Tactic:
·

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ↑x * ⊥ < ↑x * ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ a * ↑x < ⊥ * ↑x

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : a < ↑a✝
⊢ a * ↑x < ↑a✝ * ↑x

Tactic:
·

Goal state after:
case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : WithBot α
x : α
x0 : 0 < ↑x
h : a < ⊥
⊢ a * ↑x < ⊥ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x

pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑a✝ * ↑x < ↑a✝¹ * ↑x

Tactic:
·

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a b : WithBot α
x0 : 0 ≤ 0
h : 0 * a < 0 * b
⊢ a < b

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
x0' : x ≠ 0
⊢ a < b

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a b : WithBot α
x0 : 0 ≤ 0
h : 0 * a < 0 * b
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
x0' : x ≠ 0
⊢ x ≠ ⊥

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a b : WithBot α
x : α
x0 : 0 ≤ ↑x
h : ↑x * a < ↑x * b
x0' : ↑x ≠ 0
⊢ a < b

Tactic:
·

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : x * a < x * b
x0' : x ≠ 0
⊢ x ≠ ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ↑x * a < ↑x * ⊥
⊢ a < ⊥

pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑x * a < ↑x * ↑a✝
⊢ a < ↑a✝

Tactic:
·

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : ↑x * a < ↑x * ⊥
⊢ a < ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑x * ⊥ < ↑x * ↑a✝
⊢ ⊥ < ↑a✝

pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑x * ↑a✝ < ↑x * ↑a✝¹
⊢ ↑a✝ < ↑a✝¹

Tactic:
·

Goal state after:
case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ↑x * ⊥ < ↑x * ↑a✝
⊢ ⊥ < ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a b : WithBot α
x0 : 0 ≤ 0
h : a * 0 < b * 0
⊢ a < b

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
x0' : x ≠ 0
⊢ a < b

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a b : WithBot α
x0 : 0 ≤ 0
h : a * 0 < b * 0
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
x0' : x ≠ 0
⊢ x ≠ ⊥

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a b : WithBot α
x : α
x0 : 0 ≤ ↑x
h : a * ↑x < b * ↑x
x0' : ↑x ≠ 0
⊢ a < b

Tactic:
·

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a * x < b * x
x0' : x ≠ 0
⊢ x ≠ ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : a * ↑x < ⊥ * ↑x
⊢ a < ⊥

pp: case inr.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : a * ↑x < ↑a✝ * ↑x
⊢ a < ↑a✝

Tactic:
·

Goal state after:
case inr.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
a : WithBot α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
h : a * ↑x < ⊥ * ↑x
⊢ a < ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ⊥ * ↑x < ↑a✝ * ↑x
⊢ ⊥ < ↑a✝

pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : ↑a✝ * ↑x < ↑a✝¹ * ↑x
⊢ ↑a✝ < ↑a✝¹

Tactic:
·

Goal state after:
case inr.coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : α
x0 : 0 ≤ ↑x
x0' : ↑x ≠ 0
a✝ : α
h : ⊥ * ↑x < ↑a✝ * ↑x
⊢ ⊥ < ↑a✝
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
h : ↑x * ⊥ ≤ ↑x * b
⊢ ⊥ ≤ b

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑x * ↑a✝ ≤ ↑x * b
⊢ ↑a✝ ≤ b

Tactic:
·

Goal state after:
case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
h : ↑x * ⊥ ≤ ↑x * b
⊢ ⊥ ≤ b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑x * ↑a✝ ≤ ↑x * ⊥
⊢ ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑x * ↑a✝¹ ≤ ↑x * ↑a✝
⊢ ↑a✝¹ ≤ ↑a✝

Tactic:
·

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑x * ↑a✝ ≤ ↑x * ⊥
⊢ ↑a✝ ≤ ⊥
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
h : ⊥ * ↑x ≤ b * ↑x
⊢ ⊥ ≤ b

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ b * ↑x
⊢ ↑a✝ ≤ b

Tactic:
·

Goal state after:
case bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
b : WithBot α
x : α
x0 : 0 < ↑x
h : ⊥ * ↑x ≤ b * ↑x
⊢ ⊥ ≤ b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ ⊥ * ↑x
⊢ ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝¹ * ↑x ≤ ↑a✝ * ↑x
⊢ ↑a✝¹ ≤ ↑a✝

Tactic:
·

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑a✝ * ↑x ≤ ⊥ * ↑x
⊢ ↑a✝ ≤ ⊥
Module: Mathlib.Order.SuccPred.WithBot

Goal state before:
pp: case bot
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
⊢ ⊥.succ = ⊥ ↔ ⊥ = ⊥

pp: case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
⊢ (↑a✝).succ = ⊥ ↔ ↑a✝ = ⊥

Tactic:
·

Goal state after:
case bot
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
⊢ ⊥.succ = ⊥ ↔ ⊥ = ⊥
Module: Mathlib.Order.SuccPred.WithBot

Goal state before:
pp: case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
⊢ (↑a✝).succ = ⊥ ↔ ↑a✝ = ⊥

Tactic:
·

Goal state after:
case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
⊢ (↑a✝).succ = ⊥ ↔ ↑a✝ = ⊥
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

pp: α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂

pp: case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₁ ≤ v₂
⊢ v₁ < v₂
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : IsMax a
⊢ succ a ≤ b ↔ a < b

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : IsMax a
⊢ succ a ≤ b ↔ a < b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ∃ c, ⟨b, ⋯⟩ < c ∧ c < a
⊢ False

pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ ⟨b, ⋯⟩ < a

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ∃ c, ⟨b, ⋯⟩ < c ∧ c < a
⊢ False
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ ⟨b, ⋯⟩ < a

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ ⟨b, ⋯⟩ < a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a