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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
⊢ 0 ≤ y ∨ y ≤ 0

pp: case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
⊢ 0 ≤ y ∨ y ≤ 0

case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithZero α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ 0 ≤ 0 ∨ 0 ≤ 0

pp: case zero.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ 0 ≤ ↑a✝ ∨ ↑a✝ ≤ 0

pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ 0 ∨ 0 ≤ ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ 0 ≤ 0 ∨ 0 ≤ 0

case zero.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ 0 ≤ ↑a✝ ∨ ↑a✝ ≤ 0

case coe.zero
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ 0 ∨ 0 ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
⊢ ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z

pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝ : α
⊢ ⊤ ≤ z → ↑a✝ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝ ≤ z

pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝ : α
⊢ ↑a✝ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤ ≤ z

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ z → ↑a✝ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ z

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
⊢ ⊤ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ z

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝ : α
⊢ ⊤ ≤ z → ↑a✝ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝ ≤ z

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝ : α
⊢ ↑a✝ ≤ z → ⊤ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤ ≤ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ z → ↑a✝ ≤ z → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ z
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case right.left
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < x

pp: case right.right
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < y

Tactic:
<;>

Goal state after:
case right.left
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < x

case right.right
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 ≤ a
⊢ 0 ≤ exp a

pp: case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
hx : x ≠ 0
⊢ x ≤ exp a

Tactic:
<;>

Goal state after:
case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 ≤ a
⊢ 0 ≤ exp a

case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log ≤ a
hx : x ≠ 0
⊢ x ≤ exp a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 < a
⊢ 0 < exp a

pp: case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
hx : x ≠ 0
⊢ x < exp a

Tactic:
<;>

Goal state after:
case inl
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
hxa : log 0 < a
⊢ 0 < exp a

case inr
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hxa : x.log < a
hx : x ≠ 0
⊢ x < exp a
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case inr
y x : Multiplicative ℤ
⊢ (↑x).log < (↑y * exp 1).log ↔ (↑x).log ≤ (↑y).log

pp: case inr.hx
y x : Multiplicative ℤ
⊢ ↑x ≠ 0

pp: case inr.hy
y x : Multiplicative ℤ
⊢ ↑y * exp 1 ≠ 0

pp: case inr.hx
y x : Multiplicative ℤ
⊢ ↑x ≠ 0

pp: case inr.hy
y x : Multiplicative ℤ
⊢ ↑y ≠ 0

Tactic:
<;>

Goal state after:
case inr
y x : Multiplicative ℤ
⊢ (↑x).log < (↑y * exp 1).log ↔ (↑x).log ≤ (↑y).log

case inr.hx
y x : Multiplicative ℤ
⊢ ↑x ≠ 0

case inr.hy
y x : Multiplicative ℤ
⊢ ↑y * exp 1 ≠ 0

case inr.hx
y x : Multiplicative ℤ
⊢ ↑x ≠ 0

case inr.hy
y x : Multiplicative ℤ
⊢ ↑y ≠ 0
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ ⊤

pp: case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ ↑a✝

pp: case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝ ≤ ⊤

pp: case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ⊤ ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝¹ ≤ ↑a✝

pp: case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ ⊤ → ⊤ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤ ≤ ⊤

pp: case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ⊤ ≤ ↑a✝

pp: case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ ⊤

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝² ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
⊢ ⊤ ≤ ⊤ → ⊤ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ⊤ ≤ ↑a✝

case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ⊤ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝ ≤ ⊤

case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ⊤ ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⊤ ↑a✝¹ ≤ ↑a✝

case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝ : α
⊢ ↑a✝ ≤ ⊤ → ⊤ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝ ⊤ ≤ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ⊤ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ⊤ ≤ ↑a✝

case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ⊤ → ↑a✝ ≤ ⊤ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝¹ ↑a✝ ≤ ⊤

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : SemilatticeSup α
a✝² a✝¹ a✝ : α
⊢ ↑a✝² ≤ ↑a✝ → ↑a✝¹ ≤ ↑a✝ → WithTop.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ↑a✝² ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LE α
a b : α
hx : 0 = 0 → a ≤ b
⊢ unzeroD a 0 ≤ b ↔ 0 ≤ ↑b

pp: case coe
α : Type u_1
inst✝ : LE α
a b a✝ : α
hx : ↑a✝ = 0 → a ≤ b
⊢ unzeroD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : LE α
a b : α
hx : 0 = 0 → a ≤ b
⊢ unzeroD a 0 ≤ b ↔ 0 ≤ ↑b

case coe
α : Type u_1
inst✝ : LE α
a b a✝ : α
hx : ↑a✝ = 0 → a ≤ b
⊢ unzeroD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LE α
a x : α
h : ↑x ≤ 0
⊢ unzeroD a ↑x ≤ unzeroD a 0

pp: case coe
α : Type u_1
inst✝ : LE α
a x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unzeroD a ↑x ≤ unzeroD a ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : LE α
a x : α
h : ↑x ≤ 0
⊢ unzeroD a ↑x ≤ unzeroD a 0

case coe
α : Type u_1
inst✝ : LE α
a x a✝ : α
h : ↑x ≤ ↑a✝
⊢ unzeroD a ↑x ≤ unzeroD a ↑a✝
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LT α
a b : α
hx : 0 = 0 → a < b
⊢ unzeroD a 0 < b ↔ 0 < ↑b

pp: case coe
α : Type u_1
inst✝ : LT α
a b a✝ : α
hx : ↑a✝ = 0 → a < b
⊢ unzeroD a ↑a✝ < b ↔ ↑a✝ < ↑b

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : LT α
a b : α
hx : 0 = 0 → a < b
⊢ unzeroD a 0 < b ↔ 0 < ↑b

case coe
α : Type u_1
inst✝ : LT α
a b a✝ : α
hx : ↑a✝ = 0 → a < b
⊢ unzeroD a ↑a✝ < b ↔ ↑a✝ < ↑b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
b : α
⊢ 0 ≤ ↑(unzeroD b 0)

pp: case coe
α : Type u_1
inst✝ : Preorder α
b a✝ : α
⊢ ↑a✝ ≤ ↑(unzeroD b ↑a✝)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : Preorder α
b : α
⊢ 0 ≤ ↑(unzeroD b 0)

case coe
α : Type u_1
inst✝ : Preorder α
b a✝ : α
⊢ ↑a✝ ≤ ↑(unzeroD b ↑a✝)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithBot α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithBot α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ↑a✝ ⊓ z

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊥ ⊓ z

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ⊥ ⊓ z

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ ↑a✝ ⊓ z

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊥ ⊓ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithBot α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ⊥ ⊓ ⊥

pp: case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ⊥ ⊓ ↑a✝

pp: case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ↑a✝ ⊓ ⊥

pp: case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊥ ⊔ ↑a✝¹) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ↑a✝¹ ⊓ ↑a✝

pp: case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ ⊥) ≤ ↑a✝ ⊔ ⊥ ⊓ ⊥

pp: case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊥) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊥ ⊓ ↑a✝

pp: case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊥) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊥

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝

Tactic:
<;>

Goal state after:
case bot.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ⊥ ⊓ ⊥

case bot.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ⊥) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ⊥ ⊓ ↑a✝

case bot.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊥ ⊔ ↑a✝) ⊓ (⊥ ⊔ ⊥) ≤ ⊥ ⊔ ↑a✝ ⊓ ⊥

case bot.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊥ ⊔ ↑a✝¹) ⊓ (⊥ ⊔ ↑a✝) ≤ ⊥ ⊔ ↑a✝¹ ⊓ ↑a✝

case coe.bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊥) ⊓ (↑a✝ ⊔ ⊥) ≤ ↑a✝ ⊔ ⊥ ⊓ ⊥

case coe.bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊥) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊥ ⊓ ↑a✝

case coe.coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊥) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊥

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithTop α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithTop α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
y z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ y) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ y ⊓ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z

pp: case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ↑a✝ ⊓ z

pp: case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊤ ⊓ z

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ⊤ ⊓ z

case top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ ↑a✝ ⊓ z

case coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ z) ≤ ↑a✝ ⊔ ⊤ ⊓ z

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
z : WithTop α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ z) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ z
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ ⊤ ⊓ ⊤

pp: case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ↑a✝) ≤ ⊤ ⊔ ⊤ ⊓ ↑a✝

pp: case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ ↑a✝ ⊓ ⊤

pp: case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊤ ⊔ ↑a✝¹) ⊓ (⊤ ⊔ ↑a✝) ≤ ⊤ ⊔ ↑a✝¹ ⊓ ↑a✝

pp: case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ ⊤) ≤ ↑a✝ ⊔ ⊤ ⊓ ⊤

pp: case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊤) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊤ ⊓ ↑a✝

pp: case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊤) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊤

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝

Tactic:
<;>

Goal state after:
case top.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ ⊤ ⊓ ⊤

case top.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊤ ⊔ ⊤) ⊓ (⊤ ⊔ ↑a✝) ≤ ⊤ ⊔ ⊤ ⊓ ↑a✝

case top.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (⊤ ⊔ ↑a✝) ⊓ (⊤ ⊔ ⊤) ≤ ⊤ ⊔ ↑a✝ ⊓ ⊤

case top.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (⊤ ⊔ ↑a✝¹) ⊓ (⊤ ⊔ ↑a✝) ≤ ⊤ ⊔ ↑a✝¹ ⊓ ↑a✝

case coe.top.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝ : α
⊢ (↑a✝ ⊔ ⊤) ⊓ (↑a✝ ⊔ ⊤) ≤ ↑a✝ ⊔ ⊤ ⊓ ⊤

case coe.top.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ⊤) ⊓ (↑a✝¹ ⊔ ↑a✝) ≤ ↑a✝¹ ⊔ ⊤ ⊓ ↑a✝

case coe.coe.top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝¹ a✝ : α
⊢ (↑a✝¹ ⊔ ↑a✝) ⊓ (↑a✝¹ ⊔ ⊤) ≤ ↑a✝¹ ⊔ ↑a✝ ⊓ ⊤

case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (↑a✝² ⊔ ↑a✝¹) ⊓ (↑a✝² ⊔ ↑a✝) ≤ ↑a✝² ⊔ ↑a✝¹ ⊓ ↑a✝
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
floor_of_nonpos (tsub_nonpos_of_le h),

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ 0 = ⌊a⌋₊ - n
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
⊢ ⊥ ≤ y ∨ y ≤ ⊥

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
⊢ ⊥ ≤ y ∨ y ≤ ⊥

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithBot α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊥ ≤ ⊥ ∨ ⊥ ≤ ⊥

pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊥ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊥

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊥ ∨ ⊥ ≤ ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹

Tactic:
<;>

Goal state after:
case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ ⊥ ≤ ⊥ ∨ ⊥ ≤ ⊥

case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ⊥ ≤ ↑a✝ ∨ ↑a✝ ≤ ⊥

case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝ : α
⊢ ↑a✝ ≤ ⊥ ∨ ⊥ ≤ ↑a✝

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ ∨ ↑a✝ ≤ ↑a✝¹
Module: Mathlib.Order.WithBot

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
⊢ ⊤ ≤ y ∨ y ≤ ⊤

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
⊢ ⊤ ≤ y ∨ y ≤ ⊤

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
y : WithTop α
a✝ : α
⊢ ↑a✝ ≤ y ∨ y ≤ ↑a✝
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case h₁
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉₊

pp: case h₂
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉₊

Tactic:
<;>

Goal state after:
case h₁
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉₊

case h₂
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉₊