Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_right (IMOSLLean4/Extra/Infinitesimal/FloorRing.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |ε * r| < 1
Tactic:
apply (hε (k * ⌈|r|⌉.natAbs)).trans_le'
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |ε * r| ≤ (k * ⌈|r|⌉.natAbs) • |ε|

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |ε * r| ≤ (k * ⌈|r|⌉.natAbs) • |ε|
Tactic:
rw [abs_mul, mul_nsmul', nsmul_eq_mul' |ε|]
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|ε| * |r|) ≤ k • (|ε| * ↑⌈|r|⌉.natAbs)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|ε| * |r|) ≤ k • (|ε| * ↑⌈|r|⌉.natAbs)
Tactic:
refine nsmul_le_nsmul_right (mul_le_mul_of_nonneg_left ?_ (abs_nonneg ε)) k
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs
Tactic:
rw [← Int.cast_natCast ⌈|r|⌉.natAbs, ← Int.ceil_le]
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs
Tactic:
exact Int.le_natAbs
State after:
no goals